From 42f206171d0df032ea110743ee3c761edf571a26 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 27 Dec 2021 15:10:09 -0800 Subject: [PATCH] fix #5741 --- src/tactic/core/pb_preprocess_tactic.cpp | 2 +- src/tactic/goal.h | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/tactic/core/pb_preprocess_tactic.cpp b/src/tactic/core/pb_preprocess_tactic.cpp index ef3db804b..1d40a91c7 100644 --- a/src/tactic/core/pb_preprocess_tactic.cpp +++ b/src/tactic/core/pb_preprocess_tactic.cpp @@ -605,7 +605,7 @@ private: sub.insert(e, v); expr_ref tmp(m); m_r.set_substitution(&sub); - for (unsigned i = 0; i < positions.size(); ++i) { + for (unsigned i = 0; !g->inconsistent() && i < positions.size(); ++i) { unsigned idx = positions[i]; expr_ref f(m); proof_ref new_pr(m); diff --git a/src/tactic/goal.h b/src/tactic/goal.h index f7f927bb3..f32e4a66b 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 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; }