diff options
| author | Tim King <taking@google.com> | 2017-01-05 15:07:33 -0800 |
|---|---|---|
| committer | Tim King <taking@google.com> | 2017-01-05 15:07:33 -0800 |
| commit | e05f7f5cea72649069fe2f6fd96d063dcad78da2 (patch) | |
| tree | 81d3a8e455f226cf008d2fc2bbd81bcf273030b4 /test/regress/regress0/bv | |
| parent | 5552e43454c3b45ae8c7b35a822ac4b39adca72f (diff) | |
Disabling a regression test that assumes CVC4 is configured with proofs on. Modifying the travis rules so there are instances with proofs disabled.
Diffstat (limited to 'test/regress/regress0/bv')
| -rw-r--r-- | test/regress/regress0/bv/Makefile.am | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am index 0c49af306..dc87e1077 100644 --- a/test/regress/regress0/bv/Makefile.am +++ b/test/regress/regress0/bv/Makefile.am @@ -100,8 +100,10 @@ SMT_TESTS = \ bv2nat-simp-range.smt2 \ bv-int-collapse1.smt2 \ bv-int-collapse2.smt2 \ - bv-int-collapse2-sat.smt2 \ - bench_38.delta.smt2 + bv-int-collapse2-sat.smt2 + +# This benchmark is currently disabled as it uses --check-proof +# bench_38.delta.smt2 # Regression tests for SMT2 inputs SMT2_TESTS = divtest.smt2 |