mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 22:23:22 +00:00
Code Activity

fix #6734

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-05-26 09:48:58 +01:00
parent 11264c38d8
commit 5e1869d8eb
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/smt/smt_context.cpp
View file

@ -3024,6 +3024,7 @@ namespace smt {
SASSERT(is_well_sorted(m, e)); SASSERT(is_well_sorted(m, e));
TRACE("begin_assert_expr", tout << mk_pp(e, m) << " " << mk_pp(pr, m) << "\n";); TRACE("begin_assert_expr", tout << mk_pp(e, m) << " " << mk_pp(pr, m) << "\n";);
TRACE("begin_assert_expr_ll", tout << mk_ll_pp(e, m) << "\n";); TRACE("begin_assert_expr_ll", tout << mk_ll_pp(e, m) << "\n";);
if (!m_searching)
pop_to_base_lvl(); pop_to_base_lvl();
if (pr == nullptr) if (pr == nullptr)
m_asserted_formulas.assert_expr(e); m_asserted_formulas.assert_expr(e);