mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-16 19:06:17 +00:00
Code Activity

fix regression found by fuzzers fix #6271

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-08-14 12:26:33 -07:00
parent 1d87592b13
commit 138f0d269c
1 changed files with 7 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/qe/mbp/mbp_arith.cpp
View file

@ -220,10 +220,13 @@ namespace mbp {
if (!a.is_numeral(val, r)) if (!a.is_numeral(val, r))
throw default_exception("mbp evaluation didn't produce an integer"); throw default_exception("mbp evaluation didn't produce an integer");
c += mul * r; c += mul * r;
// t1 mod mul1 == r
vars coeffs; rational c0(-r), mul0(1);
rational c0 = add_def(t1, mul1, coeffs); obj_map<expr, rational> ts0;
mbo.add_divides(coeffs, c0 - r, mul1); 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) { else if (false && a.is_mod(t, t1, t2) && is_numeral(t2, mul1) && mul1 > 0) {
// v = t1 mod mul1 // v = t1 mod mul1