projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 27e1a58) | patch
Fix soundness bug in reduction of integer div/mod (#3766)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 17 Feb 2020 17:17:02 +0000 (11:17 -0600)
committerGitHub <noreply@github.com>
Mon, 17 Feb 2020 17:17:02 +0000 (09:17 -0800)
commitb19c08997e15d2e42f61f1936fd60c5e34081d68
treeee91b86dcc64a2e8c5106f173974151245b641c6tree
parent27e1a5835139d5107010475cb951a1aa1350e7f4commit | 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.
src/theory/arith/theory_arith_private.cpp diff | blob | history
src/theory/theory_engine.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/quantifiers/issue3765-quant-dd.smt2 [new file with mode: 0644] blob
test/regress/regress1/quantifiers/issue3765.smt2 [new file with mode: 0644] blob