mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix #3641

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-31 23:29:08 -07:00
parent d9032890e4
commit c20b321e57
1 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/smt/theory_lra.cpp
View file

@ -1038,8 +1038,6 @@ public:
bool internalize_atom(app * atom, bool gate_ctx) { bool internalize_atom(app * atom, bool gate_ctx) {
SASSERT(!ctx().b_internalized(atom)); SASSERT(!ctx().b_internalized(atom));
bool_var bv = ctx().mk_bool_var(atom);
ctx().set_var_theory(bv, get_id());
expr* n1, *n2; expr* n1, *n2;
rational r; rational r;
lp_api::bound_kind k; lp_api::bound_kind k;
@ -1059,8 +1057,10 @@ public:
else { else {
TRACE("arith", tout << "Could not internalize " << mk_pp(atom, m) << "\n";); TRACE("arith", tout << "Could not internalize " << mk_pp(atom, m) << "\n";);
found_unsupported(atom); found_unsupported(atom);
return true; return false;
} }
bool_var bv = ctx().mk_bool_var(atom);
ctx().set_var_theory(bv, get_id());
if (is_int(v) && !r.is_int()) { if (is_int(v) && !r.is_int()) {
r = (k == lp_api::upper_t) ? floor(r) : ceil(r); r = (k == lp_api::upper_t) ? floor(r) : ceil(r);
} }
@ -1069,7 +1069,7 @@ public:
updt_unassigned_bounds(v, +1); updt_unassigned_bounds(v, +1);
m_bounds_trail.push_back(v); m_bounds_trail.push_back(v);
m_bool_var2bound.insert(bv, b); m_bool_var2bound.insert(bv, b);
TRACE("arith_verbose", tout << "Internalized " << mk_pp(atom, m) << "\n";); TRACE("arith_verbose", tout << "Internalized " << bv << ": " << mk_pp(atom, m) << "\n";);
mk_bound_axioms(*b); mk_bound_axioms(*b);
//add_use_lists(b); //add_use_lists(b);
return true; return true;