mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-26 07:43:41 +00:00
Code Activity

more checks for #4013

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-19 12:43:06 -07:00
parent fcc34a07b2
commit 44957894ea
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/tactic/core/nnf_tactic.cpp
View file

@ -81,7 +81,7 @@ public:
} }
sz = defs.size(); sz = defs.size();
for (unsigned i = 0; i < sz; i++) { for (unsigned i = 0; !g->inconsistent() && i < sz; i++) {
if (produce_proofs) if (produce_proofs)
g->assert_expr(defs.get(i), def_prs.get(i), nullptr); g->assert_expr(defs.get(i), def_prs.get(i), nullptr);
else else
@ -90,7 +90,7 @@ public:
g->inc_depth(); g->inc_depth();
result.push_back(g.get()); result.push_back(g.get());
unsigned num_extra_names = dnames.get_num_names(); 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"); generic_model_converter * fmc = alloc(generic_model_converter, m, "nnf");
g->add(fmc); g->add(fmc);
for (unsigned i = 0; i < num_extra_names; i++) for (unsigned i = 0; i < num_extra_names; i++)