From 440601188135f02abd6353423297cd6c8a529288 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 14 Nov 2023 07:40:32 -0800 Subject: [PATCH] fix #6984 --- src/qe/qsat.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp index 6472a83c254..daeb09b8a83 100644 --- a/src/qe/qsat.cpp +++ b/src/qe/qsat.cpp @@ -551,6 +551,7 @@ namespace qe { void init() { m_solver = mk_smt2_solver(m, m_params, symbol::null); + m_last_assert = nullptr; } void collect_statistics(statistics & st) const { if (m_solver) @@ -633,7 +634,7 @@ namespace qe { \brief check alternating satisfiability. Even levels are existential, odd levels are universal. */ - lbool check_sat() { + lbool check_sat() { while (true) { ++m_stats.m_num_rounds; IF_VERBOSE(1, verbose_stream() << "(check-qsat level: " << m_level << " round: " << m_stats.m_num_rounds << ")\n";);