mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-08 15:13:23 +00:00
Code Activity

fix #3682

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-02 12:30:25 -07:00
parent 700ad1f2b9
commit 2d01c64d2c
1 changed files with 9 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/tactic/smtlogics/qfufbv_tactic.cpp
View file

@ -70,8 +70,15 @@ public:
flas.reset(); flas.reset();
// report result // report result
goal_ref resg(alloc(goal, *g, true)); goal_ref resg(alloc(goal, *g, true));
if (o == l_false) resg->assert_expr(m.mk_false()); if (o == l_false)
if (o != l_undef) result.push_back(resg.get()); resg->assert_expr(m.mk_false());
if (o == l_undef) {
g->inc_depth();
result.push_back(g.get());
}
else {
result.push_back(resg.get());
}
// report model // report model
if (g->models_enabled() && o == l_true) { if (g->models_enabled() && o == l_true) {
model_ref abstr_model = imp.get_model(); model_ref abstr_model = imp.get_model();