mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-09 07:33:24 +00:00
Code Activity

do not bound all free vars

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2018-09-10 13:43:29 -07:00
parent 8068c64cab
commit 813b906341
1 changed files with 1 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/smt/theory_lra.cpp
View file

@ -1461,7 +1461,7 @@ public:
return atom; return atom;
} }
bool all_variables_have_bounds() { bool make_sure_all_vars_have_bounds() {
if (!m_has_int) { if (!m_has_int) {
return true; return true;
} }
@ -1595,10 +1595,6 @@ public:
TRACE("arith", tout << "canceled\n";); TRACE("arith", tout << "canceled\n";);
return l_undef; return l_undef;
} }
if (!all_variables_have_bounds()) {
TRACE("arith", tout << "not all variables have bounds\n";);
return l_false;
}
if (!check_idiv_bounds()) { if (!check_idiv_bounds()) {
TRACE("arith", tout << "idiv bounds check\n";); TRACE("arith", tout << "idiv bounds check\n";);
return l_false; return l_false;