diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-17 11:17:02 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-17 09:17:02 -0800 |
commit | b19c08997e15d2e42f61f1936fd60c5e34081d68 (patch) | |
tree | ee91b86dcc64a2e8c5106f173974151245b641c6 /src/theory/arith | |
parent | 27e1a5835139d5107010475cb951a1aa1350e7f4 (diff) |
Fix soundness bug in reduction of integer div/mod (#3766)
This was introduced 7 years ago in https://github.com/CVC4/CVC4/commit/9098391fe334d829ec4101f190b8f1fa21c30752.
This impacted any case of integer div/mod of the form `(mod c t)` or `(div c t)` where c is a constant and `t` is not.
Fixes #3765.
Also improves `--dump=t-lemmas` trace to result in smt-lib compatible output, which was required for debugging this.
Diffstat (limited to 'src/theory/arith')
-rw-r--r-- | src/theory/arith/theory_arith_private.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index 76d8dbc01..0ddded6bf 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -1603,7 +1603,7 @@ Node TheoryArithPrivate::axiomIteForTotalIntDivision(Node int_div_like){ Polynomial rp = Polynomial::parsePolynomial(r); Polynomial qp = Polynomial::parsePolynomial(q); - Node abs_d = (n.isConstant()) ? + Node abs_d = (d.isConstant()) ? d.getHead().getConstant().abs().getNode() : mkIntSkolem("abs"); Node eq = Comparison::mkComparison(EQUAL, n, d * qp + rp).getNode(); |