mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 05:48:44 +00:00
Code Activity

fix #3789

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-06 13:57:38 -07:00
parent 5acf4b5968
commit 16be6b9162
2 changed files with 13 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
src/qe/qe_arith_plugin.cpp
View file

@ -1013,6 +1013,14 @@ namespace qe {
return false; return false;
} }
bool has_non_zero = false;
for (unsigned i = 1; !has_non_zero && i < values.size(); ++i) {
has_non_zero |= !values[i].is_zero();
}
if (!has_non_zero) {
return false;
}
TRACE("qe", tout << "is linear: " << mk_pp(p, m) << "\n";); TRACE("qe", tout << "is linear: " << mk_pp(p, m) << "\n";);
SASSERT(values.size() == num_vars + 1); SASSERT(values.size() == num_vars + 1);
SASSERT(num_vars > 0); SASSERT(num_vars > 0);
@ -1035,7 +1043,7 @@ namespace qe {
if (is_aux) { if (is_aux) {
// An auxiliary variable was introduced in lieu of 'x'. // An auxiliary variable was introduced in lieu of 'x'.
// it has coefficient 'm' = values[index]. // it has coefficient 'm' = values[index].
SASSERT(values[index] >= rational(3)); SASSERT(values[index] >= numeral(3));
z = m.mk_fresh_const("x", s); z = m.mk_fresh_const("x", s);
add_var(z); add_var(z);
p1 = m_arith.mk_mul(m_arith.mk_numeral(values[index], s), z); p1 = m_arith.mk_mul(m_arith.mk_numeral(values[index], s), z);
@ -1115,9 +1123,8 @@ namespace qe {
p = todo.back(); p = todo.back();
todo.pop_back(); todo.pop_back();
if (m_arith.is_add(p)) { if (m_arith.is_add(p)) {
for (unsigned i = 0; i < to_app(p)->get_num_args(); ++i) { for (expr* arg : *to_app(p))
todo.push_back(to_app(p)->get_arg(i)); todo.push_back(arg);
}
} }
else if (m_arith.is_mul(p, e1, e2) && else if (m_arith.is_mul(p, e1, e2) &&
m_arith.is_numeral(e1, k) && m_arith.is_numeral(e1, k) &&

8
src/smt/arith_eq_solver.cpp
View file

@ -161,10 +161,7 @@ bool arith_eq_solver::solve_integer_equation(
bool& is_fresh bool& is_fresh
) )
{ {
TRACE("arith_eq_solver", TRACE("arith_eq_solver", print_row(tout << "solving: ", values); );
tout << "solving: ";
print_row(tout, values);
);
// //
// perform one step of the omega test equality elimination. // perform one step of the omega test equality elimination.
// //
@ -201,8 +198,7 @@ bool arith_eq_solver::solve_integer_equation(
return false; return false;
gcd_normalize(values); gcd_normalize(values);
if (!gcd_test(values)) { if (!gcd_test(values)) {
TRACE("arith_eq_solver", tout << "not sat\n"; TRACE("arith_eq_solver", print_row(tout << "not sat\n", values););
print_row(tout, values););
return false; return false;
} }
index = find_abs_min(values); index = find_abs_min(values);