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

fix unbounded, issue #252

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-10-21 14:38:47 -07:00
parent e2f2708a9c
commit ffa78b95ab
1 changed files with 5 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/smt/theory_arith_aux.h
View file

@ -1530,6 +1530,7 @@ namespace smt {
while (best_efforts < max_efforts && !ctx.get_cancel_flag()) {
theory_var x_j = null_theory_var;
theory_var x_i = null_theory_var;
unsigned has_bound = false;
max_gain.reset();
min_gain.reset();
++round;
@ -1538,7 +1539,7 @@ namespace smt {
typename vector<row_entry>::const_iterator it = r.begin_entries();
typename vector<row_entry>::const_iterator end = r.end_entries();
for (; it != end; ++it) {
if (it->is_dead()) continue;
if (it->is_dead()) continue;
theory_var curr_x_j = it->m_var;
theory_var curr_x_i = null_theory_var;
SASSERT(is_non_base(curr_x_j));
@ -1546,6 +1547,7 @@ namespace smt {
bool curr_inc = curr_coeff.is_pos() ? max : !max;
if ((curr_inc && at_upper(curr_x_j)) || (!curr_inc && at_lower(curr_x_j))) {
// variable cannot be used for max/min.
has_bound = true;
continue;
}
bool picked_var = pick_var_to_leave(curr_x_j, curr_inc, curr_a_ij,
@ -1593,10 +1595,10 @@ namespace smt {
TRACE("opt", tout << "after traversing row:\nx_i: v" << x_i << ", x_j: v" << x_j << ", gain: " << max_gain << "\n";
tout << "best efforts: " << best_efforts << " has shared: " << has_shared << "\n";);
if (x_j == null_theory_var && x_i == null_theory_var) {
if (!has_bound && x_i == null_theory_var && x_j == null_theory_var) {
has_shared = false;
best_efforts = 0;
result = UNBOUNDED;
result = UNBOUNDED;
break;
}