From f8dcaa8885ce44020effad7b427fd3c7432328ea Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 27 Mar 2020 10:23:00 -0700
Subject: [PATCH] 'na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/ast/ast.cpp | 2 +-
src/smt/smt_context_inv.cpp | 2 +-
src/tactic/core/ctx_simplify_tactic.cpp | 3 ++-
3 files changed, 4 insertions(+), 3 deletions(-)
diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index f76eca9a6..90fd64fd9 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -1800,7 +1800,7 @@ static void track_id(ast* n, unsigned id) {
if (n->get_id() != id) return;
++s_count;
std::cout << s_count << "\n";
-// SASSERT(s_count != 7);
+ //SASSERT(s_count != 23);
}
#endif
diff --git a/src/smt/smt_context_inv.cpp b/src/smt/smt_context_inv.cpp
index e26419829..51098bafb 100644
--- a/src/smt/smt_context_inv.cpp
+++ b/src/smt/smt_context_inv.cpp
@@ -264,7 +264,7 @@ namespace smt {
bool context::check_th_diseq_propagation() const {
TRACE("check_th_diseq_propagation", tout << "m_propagated_th_diseqs.size() " << m_propagated_th_diseqs.size() << "\n";);
int num = get_num_bool_vars();
- if (inconsistent()) {
+ if (inconsistent() || get_manager().canceled()) {
return true;
}
for (bool_var v = 0; v < num; v++) {
diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp
index 81a1364f9..eb4092cd4 100644
--- a/src/tactic/core/ctx_simplify_tactic.cpp
+++ b/src/tactic/core/ctx_simplify_tactic.cpp
@@ -585,7 +585,8 @@ struct ctx_simplify_tactic::imp {
for (unsigned i = 0; !g.inconsistent() && i < sz; ++i) {
expr * t = g.form(i);
process(t, r);
- proof* new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite(t, r));
+ proof_ref new_pr(m.mk_rewrite(t, r), m);
+ new_pr = m.mk_modus_ponens(g.pr(i), new_pr);
g.update(i, r, new_pr, g.dep(i));
}
}