mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 05:48:44 +00:00
Code Activity

fix #6955

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-10-19 10:41:24 -07:00
parent 11ab583232
commit 8c00181815
1 changed files with 11 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

26
src/qe/qsat.cpp
View file

@ -568,25 +568,21 @@ namespace qe {
m_solver = nullptr; m_solver = nullptr;
} }
void assert_expr(expr *e) { void assert_expr(expr* e) {
if (!m.is_true(e)) if (!m.is_true(e))
m_solver->assert_expr(e); m_solver->assert_expr(e);
} }
void assert_blocking_fml(expr* e) { void assert_blocking_fml(expr* e) {
if (m.is_true(e)) return; if (m.is_true(e))
if (m_last_assert) { return;
if (e == m_last_assert) { if (m_last_assert && e == m_last_assert && !m.is_false(e)) {
verbose_stream() << "Asserting this expression twice in a row:\n " << m_last_assert << "\n"; IF_VERBOSE(0, verbose_stream() << "Asserting this expression twice in a row:\n " << m_last_assert << "\n");
SASSERT(false); UNREACHABLE();
std::exit(3);
} }
m_last_assert = e;
}
m_last_assert = e;
m_solver->assert_expr(e); m_solver->assert_expr(e);
} }
void get_core(expr_ref_vector& core) { void get_core(expr_ref_vector& core) {
core.reset(); core.reset();
m_solver->get_unsat_core(core); m_solver->get_unsat_core(core);