From 138f0d269c3a1bb8ce9612165b44e390d78eac6c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 14 Aug 2022 12:26:33 -0700 Subject: [PATCH] fix regression found by fuzzers fix #6271 --- src/qe/mbp/mbp_arith.cpp | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/qe/mbp/mbp_arith.cpp b/src/qe/mbp/mbp_arith.cpp index 11db720ef..713a63c14 100644 --- a/src/qe/mbp/mbp_arith.cpp +++ b/src/qe/mbp/mbp_arith.cpp @@ -220,10 +220,13 @@ namespace mbp { if (!a.is_numeral(val, r)) throw default_exception("mbp evaluation didn't produce an integer"); c += mul * r; - // t1 mod mul1 == r - vars coeffs; - rational c0 = add_def(t1, mul1, coeffs); - mbo.add_divides(coeffs, c0 - r, mul1); + + rational c0(-r), mul0(1); + obj_map ts0; + linearize(mbo, eval, mul0, t1, c0, fmls, ts0, tids); + vars coeffs; + extract_coefficients(mbo, eval, ts0, tids, coeffs); + mbo.add_divides(coeffs, c0, mul1); } else if (false && a.is_mod(t, t1, t2) && is_numeral(t2, mul1) && mul1 > 0) { // v = t1 mod mul1