mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
Code Activity

fix #3659

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-01 11:31:12 -07:00
parent b3c863fb15
commit e160320e8a
1 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/smt/tactic/smt_tactic.cpp
View file

@ -19,6 +19,7 @@ Notes:
#include "util/debug.h"
#include "ast/rewriter/rewriter_types.h"
#include "ast/ast_util.h"
#include "ast/ast_ll_pp.h"
#include "smt/smt_kernel.h"
#include "smt/params/smt_params.h"
#include "smt/params/smt_params_helper.hpp"
@ -249,8 +250,11 @@ public:
lcore = m.mk_join(lcore, m.mk_leaf(d));
}
}
if (!pr && m.proofs_enabled()) pr = m.mk_asserted(m.mk_false()); // bail out
if (m.proofs_enabled() && !pr) pr = m.mk_asserted(m.mk_false()); // bail out
if (pr && m.get_fact(pr) != m.mk_false()) pr = m.mk_asserted(m.mk_false()); // could happen in clause_proof mode
in->assert_expr(m.mk_false(), pr, lcore);
result.push_back(in.get());
return;
}