From 5fe737f9513ef4c9c6f582d08bd8cd644a9e012c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 13 Mar 2020 13:44:07 -0500 Subject: [PATCH] Remove regress for real to int (#4071) Missed this one when real to int was disabled for quantifiers. Fixes regress1. --- test/regress/CMakeLists.txt | 1 - test/regress/regress1/quantifiers/real-to-int-quant.smt2 | 6 ------ 2 files changed, 7 deletions(-) delete mode 100644 test/regress/regress1/quantifiers/real-to-int-quant.smt2 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) -- 2.30.2