diff options
| author | Alex Ozdemir <aozdemir@hmc.edu> | 2020-02-03 22:42:27 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-02-03 22:42:27 -0800 |
| commit | d3e45c1fd1ef3f56f15ad08c783a3d5c54ea10c1 (patch) | |
| tree | bc604d6777250df74670b4f63c23d694594c31ec /test/regress/CMakeLists.txt | |
| parent | b2fad75b845de71d030705b3c3672009f1e4c2a4 (diff) | |
Regression tests for arithmetic proofs. (#3701)
* Add more arith proof regression tests
These tests are designed to test interesting cases of arithmetic proofs,
such as mixing integers and reals and tightening bounds.
Right now, they have the --no-check-proofs flag set, which prevents them
from testing the proof machinery. However, once we check that machinery
into master, we'll remove that flag, thus enabling the full effect of
the tests.
* A few comments explaining things.
* Add another tightening test
* Add new test to CMake
* No --no-check-models. There are no models anyway.
* Delete smt-lib-version, per Yoni
Diffstat (limited to 'test/regress/CMakeLists.txt')
| -rw-r--r-- | test/regress/CMakeLists.txt | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 20272de2b..35d604768 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -3,6 +3,12 @@ set(regress_0_tests regress0/arith/ackermann.real.smt2 + regress0/arith/arith-eq.smt2 + regress0/arith/arith-mixed.smt2 + regress0/arith/arith-tighten-1.smt2 + regress0/arith/arith-strict.smt2 + regress0/arith/arith-mixed-types-tighten.smt2 + regress0/arith/arith-mixed-types-no-tighten.smt2 regress0/arith/arith.01.cvc regress0/arith/arith.02.cvc regress0/arith/arith.03.cvc |