diff options
| author | Ying Sheng <sqy1415@gmail.com> | 2019-12-16 11:42:36 -0800 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-12-16 11:42:36 -0800 |
| commit | 49f0f09c6ef1c04fcd5b088456cea9998cff3c91 (patch) | |
| tree | 0d5746c90c1e7ca3e336a8cfc7417b05c0eecbe8 /test/regress/CMakeLists.txt | |
| parent | c101a6b42d1f14bc750fb2328ddd83261148d7ae (diff) | |
Support ackermannization on uninterpreted sorts in BV (#3372)
Support ackermannization on uninterpreted sorts in BV. For uninterpreted sorts, we create a bit-vector sort to replace it. For an uninterpreted sort `S`, if the number of variables within sort `S` is `n`, the replacing bit-vector will have size (log n)+1.
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 c4dfd2593..f4937f8f3 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -170,6 +170,10 @@ set(regress_0_tests regress0/bv/ackermann2.smt2 regress0/bv/ackermann3.smt2 regress0/bv/ackermann4.smt2 + regress0/bv/ackermann5.smt2 + regress0/bv/ackermann6.smt2 + regress0/bv/ackermann7.smt2 + regress0/bv/ackermann8.smt2 regress0/bv/bool-model.smt2 regress0/bv/bool-to-bv-all.smt2 regress0/bv/bool-to-bv-ite.smt2 |