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

Fix bug #1079, integrality testing seems to have been wrong

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-06-20 14:18:43 -07:00
parent 78e8e8b893
commit 0fa6274a65
2 changed files with 7 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/smt/smt_internalizer.cpp
View file

@ -1034,8 +1034,10 @@ namespace smt {
lbool val = get_assignment(curr); lbool val = get_assignment(curr);
switch(val) { switch(val) {
case l_false: case l_false:
TRACE("simplify_aux_clause_literals", display_literal(tout << get_assign_level(curr) << " " << get_scope_level() << " ", curr); tout << "\n"; );
simp_lits.push_back(~curr); simp_lits.push_back(~curr);
break; // ignore literal break; // ignore literal
// fall through
case l_undef: case l_undef:
if (curr == ~prev) if (curr == ~prev)
return false; // clause is equivalent to true return false; // clause is equivalent to true

7
src/smt/theory_arith_aux.h
View file

@ -1412,7 +1412,7 @@ namespace smt {
<< "max gain: " << max_gain << "\n";); << "max gain: " << max_gain << "\n";);
SASSERT(max_gain.is_minus_one() || !max_gain.is_neg()); SASSERT(max_gain.is_minu
SASSERT(min_gain.is_minus_one() || min_gain.is_one()); SASSERT(min_gain.is_minus_one() || min_gain.is_one());
SASSERT(is_int(x) == min_gain.is_one()); SASSERT(is_int(x) == min_gain.is_one());
@ -1458,7 +1458,7 @@ namespace smt {
normalize_gain(min_gain.get_rational(), max_gain); normalize_gain(min_gain.get_rational(), max_gain);
} }
if (is_int(x_i) && !max_gain.is_rational()) { if (is_int(x_i) && !max_gain.is_int()) {
max_gain = inf_numeral(floor(max_gain)); max_gain = inf_numeral(floor(max_gain));
normalize_gain(min_gain.get_rational(), max_gain); normalize_gain(min_gain.get_rational(), max_gain);
} }
@ -1483,7 +1483,7 @@ namespace smt {
} }
} }
TRACE("opt", TRACE("opt",
tout << "v" << x_i << " a_ij " << a_ij << " " tout << "v" << x_i << (is_int(x_i)?" int":" real") << " a_ij " << a_ij << " "
<< "min gain: " << min_gain << " " << "min gain: " << min_gain << " "
<< "max gain: " << max_gain << " tighter: " << "max gain: " << max_gain << " tighter: "
<< (is_tighter?"true":"false") << "\n";); << (is_tighter?"true":"false") << "\n";);
@ -1696,6 +1696,7 @@ namespace smt {
if (lower(x_j)) tout << "lower x_j: " << lower_bound(x_j) << " "; if (lower(x_j)) tout << "lower x_j: " << lower_bound(x_j) << " ";
tout << "value x_j: " << get_value(x_j) << "\n"; tout << "value x_j: " << get_value(x_j) << "\n";
); );
pivot<true>(x_i, x_j, a_ij, false); pivot<true>(x_i, x_j, a_ij, false);
SASSERT(is_non_base(x_i)); SASSERT(is_non_base(x_i));