diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-11-20 10:48:41 -0600 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-11-20 08:48:41 -0800 |
| commit | 7a58c9853012e7ae5992d5062592d8a21738bd32 (patch) | |
| tree | 64ded7a611da637b9a7b8ef55e884526bd8b066d | |
| parent | 176b119d86fe34878a4c9d4d7ee8f982db311b39 (diff) | |
Fix real2int regression. (#2716)
| -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) |