mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 16:38:45 +00:00
Code Activity

fix #3155

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-05 18:26:34 +01:00
parent bd3024e837
commit d3bd3bd4fc
1 changed files with 5 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/tactic/arith/purify_arith_tactic.cpp
View file

@ -29,6 +29,7 @@ Revision History:
#include "ast/rewriter/th_rewriter.h" #include "ast/rewriter/th_rewriter.h"
#include "tactic/generic_model_converter.h" #include "tactic/generic_model_converter.h"
#include "ast/ast_smt2_pp.h" #include "ast/ast_smt2_pp.h"
#include "ast/ast_pp.h"
#include "ast/rewriter/expr_replacer.h" #include "ast/rewriter/expr_replacer.h"
/* /*
@ -250,9 +251,9 @@ struct purify_arith_proc {
void mk_def_proof(expr * k, expr * def, proof_ref & result_pr) { void mk_def_proof(expr * k, expr * def, proof_ref & result_pr) {
result_pr = nullptr; result_pr = nullptr;
if (produce_proofs()) { if (produce_proofs()) {
expr * eq = m().mk_eq(k, def); expr * eq = m().mk_eq(def, k);
proof * pr1 = m().mk_def_intro(eq); proof * pr1 = m().mk_def_intro(eq);
result_pr = m().mk_apply_def(k, def, pr1); result_pr = m().mk_apply_def(def, k, pr1);
} }
} }
@ -911,7 +912,7 @@ public:
try { try {
SASSERT(g->is_well_sorted()); SASSERT(g->is_well_sorted());
tactic_report report("purify-arith", *g); tactic_report report("purify-arith", *g);
TRACE("purify_arith", g->display(tout);); TRACE("goal", g->display(tout););
bool produce_proofs = g->proofs_enabled(); bool produce_proofs = g->proofs_enabled();
bool produce_models = g->models_enabled(); bool produce_models = g->models_enabled();
bool elim_root_objs = m_params.get_bool("elim_root_objects", true); bool elim_root_objs = m_params.get_bool("elim_root_objects", true);
@ -923,7 +924,7 @@ public:
g->add(mc.get()); g->add(mc.get());
g->inc_depth(); g->inc_depth();
result.push_back(g.get()); result.push_back(g.get());
TRACE("purify_arith", g->display(tout);); TRACE("goal", g->display(tout););
SASSERT(g->is_well_sorted()); SASSERT(g->is_well_sorted());
} }
catch (rewriter_exception & ex) { catch (rewriter_exception & ex) {