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

fix proof for extended GCD rule

Browse source
This commit is contained in:
Ken McMillan 2015-05-22 10:28:19 -07:00
parent caa616f11b
commit 13a3bdd7a3
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/smt/theory_arith_int.h
View file

@ -777,8 +777,8 @@ namespace smt {
// u += ncoeff * lower_bound(v).get_rational(); // u += ncoeff * lower_bound(v).get_rational();
u.addmul(ncoeff, lower_bound(v).get_rational()); u.addmul(ncoeff, lower_bound(v).get_rational());
} }
lower(v)->push_justification(ante, numeral::zero(), coeffs_enabled()); lower(v)->push_justification(ante, it->m_coeff, coeffs_enabled());
upper(v)->push_justification(ante, numeral::zero(), coeffs_enabled()); upper(v)->push_justification(ante, it->m_coeff, coeffs_enabled());
} }
else if (gcds.is_zero()) { else if (gcds.is_zero()) {
gcds = abs_ncoeff; gcds = abs_ncoeff;