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

a bug fix in internalize_atom, by NB

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-02-07 16:30:49 -08:00
parent 6071e08822
commit 34137cfa0a
1 changed files with 7 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/smt/theory_lra.cpp
View file

@ -990,7 +990,7 @@ public:
return true;
}
else {
TRACE("arith", tout << "Could not internalize " << mk_pp(atom, m) << "\n";);
TRACE("arith", tout << "Could not internalize " << mk_pp(atom, m) << "\n";);
found_not_handled(atom);
return true;
}
@ -1780,6 +1780,12 @@ public:
for (auto& kv : coeffs) kv.m_value.neg();
}
for (auto const& kv : coeffs) {
theory_var w = kv.m_key;
expr* o = get_enode(w)->get_owner();
is_int &= a.is_int(o);
}
app_ref atom(m);
app_ref t = coeffs2app(coeffs, rational::zero(), is_int);
if (lower_bound) {