| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-02-17 | Fix soundness bug in reduction of integer div/mod (#3766) | Andrew Reynolds | |
| 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. | |||
 |
index : cvc5.git | |
| CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. | git repository hosting |
| summaryrefslogtreecommitdiff |
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback