mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-14 19:24:44 +00:00
Code Activity

revert fix to #2417

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-07-24 11:24:01 -07:00
parent 3a90de1cbe
commit 809b0ebca7
3 changed files with 9 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/rewriter/bv_rewriter.cpp
View file

@ -2084,8 +2084,10 @@ br_status bv_rewriter::mk_bv_comp(expr * arg1, expr * arg2, expr_ref & result) {
br_status bv_rewriter::mk_bv_add(unsigned num_args, expr * const * args, expr_ref & result) {
br_status st = mk_add_core(num_args, args, result);
if (st != BR_FAILED && st != BR_DONE)
if (st != BR_FAILED && st != BR_DONE) {
TRACE("bv", tout << result << "\n";);
return st;
}
#if 0
expr * x;
expr * y;

7
src/ast/rewriter/poly_rewriter_def.h
View file

@ -1017,8 +1017,11 @@ bool poly_rewriter<Config>::hoist_ite(expr_ref& e) {
bs.push_back(s);
}
}
adds[i] = mk_add_app(bs.size(), bs.c_ptr());
pinned.push_back(adds[i]);
expr* a2 = mk_add_app(bs.size(), bs.c_ptr());
if (a != a2) {
adds[i] = a2;
pinned.push_back(a2);
}
}
}
++i;