From 13a3bdd7a3589c0a7e8b622acfba20e542c2f2b8 Mon Sep 17 00:00:00 2001 From: Ken McMillan Date: Fri, 22 May 2015 10:28:19 -0700 Subject: [PATCH] fix proof for extended GCD rule --- src/smt/theory_arith_int.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h index b600dd3c0..7c9e67da6 100644 --- a/src/smt/theory_arith_int.h +++ b/src/smt/theory_arith_int.h @@ -777,8 +777,8 @@ namespace smt { // u += ncoeff * lower_bound(v).get_rational(); u.addmul(ncoeff, lower_bound(v).get_rational()); } - lower(v)->push_justification(ante, numeral::zero(), coeffs_enabled()); - upper(v)->push_justification(ante, numeral::zero(), coeffs_enabled()); + lower(v)->push_justification(ante, it->m_coeff, coeffs_enabled()); + upper(v)->push_justification(ante, it->m_coeff, coeffs_enabled()); } else if (gcds.is_zero()) { gcds = abs_ncoeff;