diff options
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/CMakeLists.txt | 2 | ||||
-rw-r--r-- | test/regress/regress2/arith/real2int-test.smt2 (renamed from test/regress/regress1/arith/real2int-test.smt2) | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index a8eced69e..6736d712b 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1051,7 +1051,6 @@ set(regress_1_tests regress1/arith/mult.02.smt2 regress1/arith/pbrewrites-test.smt2 regress1/arith/problem__003.smt2 - regress1/arith/real2int-test.smt2 regress1/arrayinuf_error.smt2 regress1/aufbv/bug580.smt2 regress1/aufbv/fuzz10.smt @@ -1683,6 +1682,7 @@ set(regress_2_tests regress2/arith/pursuit-safety-11.smt regress2/arith/pursuit-safety-12.smt regress2/arith/qlock-4-10-9.base.cvc.smt2 + regress2/arith/real2int-test.smt2 regress2/arith/sc-7.base.cvc.smt regress2/arith/uart-8.base.cvc.smt regress2/auflia-fuzz06.smt diff --git a/test/regress/regress1/arith/real2int-test.smt2 b/test/regress/regress2/arith/real2int-test.smt2 index a769aa4de..b27b6e2b3 100644 --- a/test/regress/regress1/arith/real2int-test.smt2 +++ b/test/regress/regress2/arith/real2int-test.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --solve-real-as-int --no-new-prop +; COMMAND-LINE: --solve-real-as-int --no-new-prop --nl-ext-tplanes ; EXPECT: sat (set-info :smt-lib-version 2.6) (set-logic QF_NRA) |