From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 13 Mar 2020 18:44:07 +0000 (-0500)
Subject: Remove regress for real to int (#4071)
X-Git-Tag: cvc5-1.0.0~3493
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5fe737f9513ef4c9c6f582d08bd8cd644a9e012c;p=cvc5.git

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 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)