From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 20 Nov 2018 16:48:41 +0000 (-0600)
Subject: Fix real2int regression. (#2716)
X-Git-Tag: cvc5-1.0.0~4362
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7a58c9853012e7ae5992d5062592d8a21738bd32;p=cvc5.git

Fix real2int regression. (#2716)
---

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/regress1/arith/real2int-test.smt2
deleted file mode 100644
index a769aa4de..000000000
--- a/test/regress/regress1/arith/real2int-test.smt2
+++ /dev/null
@@ -1,29 +0,0 @@
-; COMMAND-LINE: --solve-real-as-int --no-new-prop
-; EXPECT: sat
-(set-info :smt-lib-version 2.6)
-(set-logic QF_NRA)
-(set-info :source |
-These benchmarks used in the paper:
-
-  Dejan Jovanovic and Leonardo de Moura.  Solving Non-Linear Arithmetic.
-  In IJCAR 2012, published as LNCS volume 7364, pp. 339--354.
-
-The meti-tarski benchmarks are proof obligations extracted from the
-Meti-Tarski project, see:
-
-  B. Akbarpour and L. C. Paulson. MetiTarski: An automatic theorem prover
-  for real-valued special functions. Journal of Automated Reasoning,
-  44(3):175-205, 2010.
-
-Submitted by Dejan Jovanovic for SMT-LIB.
-
-
-|)
-(set-info :category "industrial")
-(set-info :status sat)
-(declare-fun skoX () Real)
-(declare-fun skoS3 () Real)
-(declare-fun skoSX () Real)
-(assert (and (not (<= (* skoX (+ (+ (* skoS3 (/ 471 100)) (* skoSX (/ 157 100))) (* skoX (* skoS3 (- 8))))) (+ (* skoS3 3) skoSX))) (and (not (<= skoX 0)) (and (not (<= skoSX 0)) (not (<= skoS3 0))))))
-(check-sat)
-(exit)
diff --git a/test/regress/regress2/arith/real2int-test.smt2 b/test/regress/regress2/arith/real2int-test.smt2
new file mode 100644
index 000000000..b27b6e2b3
--- /dev/null
+++ b/test/regress/regress2/arith/real2int-test.smt2
@@ -0,0 +1,29 @@
+; 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)
+(set-info :source |
+These benchmarks used in the paper:
+
+  Dejan Jovanovic and Leonardo de Moura.  Solving Non-Linear Arithmetic.
+  In IJCAR 2012, published as LNCS volume 7364, pp. 339--354.
+
+The meti-tarski benchmarks are proof obligations extracted from the
+Meti-Tarski project, see:
+
+  B. Akbarpour and L. C. Paulson. MetiTarski: An automatic theorem prover
+  for real-valued special functions. Journal of Automated Reasoning,
+  44(3):175-205, 2010.
+
+Submitted by Dejan Jovanovic for SMT-LIB.
+
+
+|)
+(set-info :category "industrial")
+(set-info :status sat)
+(declare-fun skoX () Real)
+(declare-fun skoS3 () Real)
+(declare-fun skoSX () Real)
+(assert (and (not (<= (* skoX (+ (+ (* skoS3 (/ 471 100)) (* skoSX (/ 157 100))) (* skoX (* skoS3 (- 8))))) (+ (* skoS3 3) skoSX))) (and (not (<= skoX 0)) (and (not (<= skoSX 0)) (not (<= skoS3 0))))))
+(check-sat)
+(exit)