From 39ffc4ece728efac8f4bfbc77adce7bb3e737507 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 5 Apr 2020 11:19:23 -0700 Subject: [PATCH] fix #3759 Signed-off-by: Nikolaj Bjorner --- src/muz/spacer/spacer_iuc_solver.cpp | 3 +-- src/tactic/goal.cpp | 4 ++-- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/src/muz/spacer/spacer_iuc_solver.cpp b/src/muz/spacer/spacer_iuc_solver.cpp index 114bc69b9..d0b1f769b 100644 --- a/src/muz/spacer/spacer_iuc_solver.cpp +++ b/src/muz/spacer/spacer_iuc_solver.cpp @@ -53,8 +53,7 @@ namespace spacer { m_proxies.push_back (res); // -- add the new proxy to proxy eliminator - proof_ref pr(m); - pr = m.mk_asserted (m.mk_true ()); + proof_ref pr(m.mk_rewrite(res, m.mk_true()), m); m_elim_proxies_sub.insert (res, m.mk_true (), pr); } diff --git a/src/tactic/goal.cpp b/src/tactic/goal.cpp index 28df07d02..348f54878 100644 --- a/src/tactic/goal.cpp +++ b/src/tactic/goal.cpp @@ -116,7 +116,7 @@ void goal::copy_to(goal & target) const { } void goal::push_back(expr * f, proof * pr, expr_dependency * d) { - SASSERT(!m().proofs_enabled() || pr); + SASSERT(!proofs_enabled() || pr); if (m().is_true(f)) return; if (m().is_false(f)) { @@ -254,7 +254,7 @@ void goal::assert_expr(expr * f, proof * pr, expr_dependency * d) { if (m_inconsistent) { return; } - SASSERT(!m().proofs_enabled() || pr); + SASSERT(!proofs_enabled() || pr); if (pr) { CTRACE("goal", f != m().get_fact(pr), tout << mk_pp(f, m()) << "\n" << mk_pp(pr, m()) << "\n";); SASSERT(f == m().get_fact(pr));