diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-03-13 13:44:07 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-13 11:44:07 -0700 |
commit | 5fe737f9513ef4c9c6f582d08bd8cd644a9e012c (patch) | |
tree | fae96ec6eb223ad6a62bf00c4872635379e7c952 | |
parent | 9efc82b701f1ab3a395306662f6d4fa37b130218 (diff) |
Remove regress for real to int (#4071)
Missed this one when real to int was disabled for quantifiers. Fixes regress1.
-rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/regress/regress1/quantifiers/real-to-int-quant.smt2 | 6 |
2 files changed, 0 insertions, 7 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index c23ed07ee..a68c31441 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1529,7 +1529,6 @@ set(regress_1_tests regress1/quantifiers/qe.smt2 regress1/quantifiers/quant-wf-int-ind.smt2 regress1/quantifiers/quaternion_ds1_symm_0428.fof.smt2 - regress1/quantifiers/real-to-int-quant.smt2 regress1/quantifiers/recfact.cvc regress1/quantifiers/rel-trigger-unusable.smt2 regress1/quantifiers/repair-const-nterm.smt2 diff --git a/test/regress/regress1/quantifiers/real-to-int-quant.smt2 b/test/regress/regress1/quantifiers/real-to-int-quant.smt2 deleted file mode 100644 index 94b131268..000000000 --- a/test/regress/regress1/quantifiers/real-to-int-quant.smt2 +++ /dev/null @@ -1,6 +0,0 @@ -; COMMAND-LINE: --solve-real-as-int --quiet -; EXPECT: sat -(set-logic ALL) -(set-info :status sat) -(assert (forall ((x Real) (y Real)) (=> (< x y) (exists ((z Real)) (and (< x z) (< z (+ y 2)))))) ) -(check-sat) |