From 84ddd06c8f068628b62054d1b083f1f1e827fd69 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 22 Dec 2021 18:04:53 -0800 Subject: [PATCH] #5732 --- src/tactic/core/pb_preprocess_tactic.cpp | 4 +++- src/tactic/goal.h | 2 +- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/tactic/core/pb_preprocess_tactic.cpp b/src/tactic/core/pb_preprocess_tactic.cpp index ef3db804b..fdc8bd93d 100644 --- a/src/tactic/core/pb_preprocess_tactic.cpp +++ b/src/tactic/core/pb_preprocess_tactic.cpp @@ -196,6 +196,8 @@ public: // now check for subsumption. for (unsigned i = 0; i < m_ge.size(); ++i) { + if (g->inconsistent()) + break; expr_ref_vector args1(m), args2(m); vector coeffs1, coeffs2; @@ -209,7 +211,7 @@ public: if (!m_vars.contains(to_app(arg))) continue; rec const& r = m_vars.find(to_app(arg)); unsigned_vector const& pos = neg?r.neg:r.pos; - for (unsigned j = 0; j < pos.size(); ++j) { + for (unsigned j = 0; !g->inconsistent() && j < pos.size(); ++j) { unsigned k = pos[j]; if (k == m_ge[i]) continue; if (!to_ge(g->form(k), args2, coeffs2, k2)) continue; diff --git a/src/tactic/goal.h b/src/tactic/goal.h index f7f927bb3..01da2c466 100644 --- a/src/tactic/goal.h +++ b/src/tactic/goal.h @@ -119,7 +119,7 @@ public: unsigned num_exprs() const; - expr * form(unsigned i) const { return m().get(m_forms, i); } + expr * form(unsigned i) const { return m_inconsistent ? m().mk_false() : m().get(m_forms, i); } proof * pr(unsigned i) const { return m().size(m_proofs) > i ? static_cast(m().get(m_proofs, i)) : nullptr; } expr_dependency * dep(unsigned i) const { return unsat_core_enabled() ? m().get(m_dependencies, i) : nullptr; }