From 7a58c9853012e7ae5992d5062592d8a21738bd32 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 20 Nov 2018 10:48:41 -0600 Subject: [PATCH] Fix real2int regression. (#2716) --- test/regress/CMakeLists.txt | 2 +- test/regress/{regress1 => regress2}/arith/real2int-test.smt2 | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) rename test/regress/{regress1 => regress2}/arith/real2int-test.smt2 (93%) 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 similarity index 93% rename from test/regress/regress1/arith/real2int-test.smt2 rename to 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) -- 2.30.2