diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-06-09 13:31:45 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-06-09 20:31:45 +0000 |
| commit | 6017579ab78cbc1390274290736ef311208a251b (patch) | |
| tree | 70714952802ac299ae4cb3e15b35a86aeae80c9c /test/regress/CMakeLists.txt | |
| parent | 73a3f516e3179141a71d3201e908bebf3061ead0 (diff) | |
Make `--solve-int-as-bv=X` robust to rewriting (#6722)
After commit 327a24508ed1d02a3fa233e680ffd0b30aa685a9, the int-to-bv
preprocessing pass is getting rewritten terms. As a result, the terms
can contain negative constants (instead of `(- c)`, i.e., `UMINUS` of a
positive constant) and `NONLINEAR_MULT`. The commit adds support for
those cases, does some minor cleanup, and adds regressions. The
regressions should allow us to detect if/when the preprocessing pass
breaks in the future.
Diffstat (limited to 'test/regress/CMakeLists.txt')
| -rw-r--r-- | test/regress/CMakeLists.txt | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 19c689b87..b94e06e47 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -645,6 +645,10 @@ set(regress_0_tests regress0/incorrect1.smtv1.smt2 regress0/ineq_basic.smtv1.smt2 regress0/ineq_slack.smtv1.smt2 + regress0/int-to-bv/basic.smt2 + regress0/int-to-bv/neg-consts.smt2 + regress0/int-to-bv/not-enough-bits.smt2 + regress0/int-to-bv/overflow.smt2 regress0/issue1063-overloading-dt-cons.smt2 regress0/issue1063-overloading-dt-fun.smt2 regress0/issue1063-overloading-dt-sel.smt2 |