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 /AUTHORS | |
| 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 'AUTHORS')
0 files changed, 0 insertions, 0 deletions