mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 03:07:07 +00:00
Code Activity

fix #3784

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-06 12:27:53 -07:00
parent bffe7a2215
commit 077a2cf6f7
1 changed files with 12 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
src/smt/arith_eq_solver.cpp
View file

@ -76,17 +76,16 @@ void arith_eq_solver::prop_mod_const(expr * e, unsigned depth, numeral const& k,
void arith_eq_solver::gcd_normalize(vector<numeral>& values) {
numeral g(0);
for (unsigned i = 0; !g.is_one() && i < values.size(); ++i) {
SASSERT(values[i].is_int());
if (!values[i].is_zero()) {
if (g.is_zero()) {
g = abs(values[i]);
}
else {
g = gcd(abs(values[i]), g);
}
}
for (auto const& n : values) {
SASSERT(n.is_int());
if (g.is_zero())
g = abs(n);
else
g = gcd(abs(n), g);
if (g.is_one())
break;
}
if (g.is_zero() || g.is_one()) {
return;
}
@ -197,6 +196,9 @@ bool arith_eq_solver::solve_integer_equation(
// Instead used the coefficient 'm' at position 'index'.
//
for (auto const& n : values)
if (!n.is_int())
return false;
gcd_normalize(values);
if (!gcd_test(values)) {
TRACE("arith_eq_solver", tout << "not sat\n";