mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 09:55:19 +00:00
Code Activity

fix #6984

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-11-14 07:40:32 -08:00
parent 3c2e97ddb6
commit 4406011881
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/qe/qsat.cpp
View file

@ -551,6 +551,7 @@ namespace qe {
void init() { void init() {
m_solver = mk_smt2_solver(m, m_params, symbol::null); m_solver = mk_smt2_solver(m, m_params, symbol::null);
m_last_assert = nullptr;
} }
void collect_statistics(statistics & st) const { void collect_statistics(statistics & st) const {
if (m_solver) if (m_solver)
@ -633,7 +634,7 @@ namespace qe {
\brief check alternating satisfiability. \brief check alternating satisfiability.
Even levels are existential, odd levels are universal. Even levels are existential, odd levels are universal.
*/ */
lbool check_sat() { lbool check_sat() {
while (true) { while (true) {
++m_stats.m_num_rounds; ++m_stats.m_num_rounds;
IF_VERBOSE(1, verbose_stream() << "(check-qsat level: " << m_level << " round: " << m_stats.m_num_rounds << ")\n";); IF_VERBOSE(1, verbose_stream() << "(check-qsat level: " << m_level << " round: " << m_stats.m_num_rounds << ")\n";);