From 44957894eae6b75a5eaba484a49a1d79b191af06 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 19 Apr 2020 12:43:06 -0700 Subject: [PATCH] more checks for #4013 Signed-off-by: Nikolaj Bjorner --- src/tactic/core/nnf_tactic.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/tactic/core/nnf_tactic.cpp b/src/tactic/core/nnf_tactic.cpp index aa8f9d1f2..72ebb949d 100644 --- a/src/tactic/core/nnf_tactic.cpp +++ b/src/tactic/core/nnf_tactic.cpp @@ -81,7 +81,7 @@ public: } sz = defs.size(); - for (unsigned i = 0; i < sz; i++) { + for (unsigned i = 0; !g->inconsistent() && i < sz; i++) { if (produce_proofs) g->assert_expr(defs.get(i), def_prs.get(i), nullptr); else @@ -90,7 +90,7 @@ public: g->inc_depth(); result.push_back(g.get()); unsigned num_extra_names = dnames.get_num_names(); - if (num_extra_names > 0) { + if (num_extra_names > 0 && !g->inconsistent()) { generic_model_converter * fmc = alloc(generic_model_converter, m, "nnf"); g->add(fmc); for (unsigned i = 0; i < num_extra_names; i++)