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 | |
| 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')
| -rw-r--r-- | src/theory/arith/theory_arith_private.cpp | 2 | ||||
| -rw-r--r-- | src/theory/theory_engine.cpp | 4 |
2 files changed, 3 insertions, 3 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(); diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 7549bd973..b43e55364 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1854,11 +1854,11 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, if(Dump.isOn("t-lemmas")) { Node n = node; - if (negated) { + if (!negated) { n = node.negate(); } Dump("t-lemmas") << CommentCommand("theory lemma: expect valid") - << QueryCommand(n.toExpr()); + << CheckSatCommand(n.toExpr()); } // Share with other portfolio threads |