Remove regress for real to int (#4071)

Missed this one when real to int was disabled for quantifiers. Fixes regress1.

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index c23ed07ee315cb82d8236b28ddbedfa9854e81df..a68c3144116b60bf70695754623466e4eab03c1d 100644 (file)
--- 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 (file)
index 94b1312..0000000
--- 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)