mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

fix assertion for integrality, lax noprogress bail out code

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-07-09 05:04:00 +02:00
parent 53f82e3239
commit 465eafbf45
2 changed files with 6 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/smt/theory_arith_aux.h
View file

@ -1449,6 +1449,8 @@ namespace smt {
/** /**
Move the variable x_i maximally towards its bound as long as Move the variable x_i maximally towards its bound as long as
bounds of other variables are not violated. bounds of other variables are not violated.
Returns false if an integer bound was truncated and no
progress was made.
*/ */
template<typename Ext> template<typename Ext>
@ -1492,7 +1494,9 @@ namespace smt {
} }
} }
bool truncated = false;
if (is_int(x_i)) { if (is_int(x_i)) {
truncated = !delta_abs.is_int();
delta_abs = floor(delta_abs); delta_abs = floor(delta_abs);
} }
@ -1505,7 +1509,7 @@ namespace smt {
TRACE("opt", tout << "Safe delta: " << delta << "\n";); TRACE("opt", tout << "Safe delta: " << delta << "\n";);
update_value(x_i, delta); update_value(x_i, delta);
return !delta.is_zero(); return !truncated || !delta.is_zero();
} }
/** /**

2
src/smt/theory_arith_inv.h
View file

@ -204,7 +204,7 @@ namespace smt {
bool theory_arith<Ext>::satisfy_integrality() const { bool theory_arith<Ext>::satisfy_integrality() const {
int num = get_num_vars(); int num = get_num_vars();
for (theory_var v = 0; v < num; v++) { for (theory_var v = 0; v < num; v++) {
if (!(is_int(v) && get_value(v).is_int())) { if (is_int(v) && !get_value(v).is_int()) {
TRACE("bound_bug", display_var(tout, v); display(tout);); TRACE("bound_bug", display_var(tout, v); display(tout););
return false; return false;
} }