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 regressions exposed in Internal

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-09-07 20:17:46 -07:00
parent d121d031e9
commit 73a8f9960f
1 changed files with 7 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/smt/theory_arith_aux.h
View file

@ -1310,17 +1310,17 @@ namespace smt {
inf_numeral& max_gain, // maximal possible gain on x_j
bool& has_shared, // determine if pivot involves shared variable
theory_var& x_i) { // base variable to pivot with x_j
context& ctx = get_context();
x_i = null_theory_var;
init_gains(x_j, inc, min_gain, max_gain);
has_shared |= ctx.is_shared(get_enode(x_j));
if (is_int(x_j) && !get_value(x_j).is_int()) {
return false;
}
x_i = null_theory_var;
context& ctx = get_context();
}
column & c = m_columns[x_j];
typename svector<col_entry>::iterator it = c.begin_entries();
typename svector<col_entry>::iterator end = c.end_entries();
init_gains(x_j, inc, min_gain, max_gain);
has_shared |= ctx.is_shared(get_enode(x_j));
bool empty_column = true;
for (; it != end; ++it) {
if (it->is_dead()) continue;
@ -1407,7 +1407,6 @@ namespace smt {
SASSERT(max_gain.is_minus_one() || !max_gain.is_neg());
SASSERT(min_gain.is_minus_one() || min_gain.is_one());
SASSERT(!is_int(x) || max_gain.is_int());
SASSERT(is_int(x) == min_gain.is_one());
}
@ -1556,7 +1555,7 @@ namespace smt {
SASSERT(!picked_var || safe_gain(curr_min_gain, curr_max_gain));
if (!picked_var && r.size() > 1) {
if (!picked_var && (r.size() > 1 || !safe_gain(curr_min_gain, curr_max_gain))) {
TRACE("opt", tout << "no variable picked\n";);
best_efforts++;
}