From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sun, 12 Apr 2020 16:01:24 +0000 (-0500)
Subject: Move slow nl regression to regress3 (#4276)
X-Git-Tag: cvc5-1.0.0~3384
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9cd5bbf8c659d2e260bad71a841f5153f358a58b;p=cvc5.git

Move slow nl regression to regress3 (#4276)

Should fix nightlies.
---

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 06dc2d87c..01092cf6e 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2021,7 +2021,6 @@ set(regress_2_tests
   regress2/instance_1444.smtv1.smt2
   regress2/javafe.ast.StandardPrettyPrint.319_no_forall.smt2
   regress2/javafe.ast.WhileStmt.447_no_forall.smt2
-  regress2/nl/siegel-nl-bases.smt2
   regress2/ooo.rf6.smt2
   regress2/ooo.tag10.smt2
   regress2/piVC_5581bd.smt2
@@ -2097,6 +2096,7 @@ set(regress_3_tests
   regress3/issue4170.smt2
   regress3/pp-regfile.smtv1.smt2
   regress3/qwh.35.405.shuffled-as.sat03-1651.smtv1.smt2
+  regress3/siegel-nl-bases.smt2
   regress3/sixfuncs.sy
   regress3/strings-any-term.sy
   regress3/strings/extf_d_perf.smt2
diff --git a/test/regress/regress2/nl/siegel-nl-bases.smt2 b/test/regress/regress2/nl/siegel-nl-bases.smt2
deleted file mode 100644
index cf6e3ab5e..000000000
--- a/test/regress/regress2/nl/siegel-nl-bases.smt2
+++ /dev/null
@@ -1,22 +0,0 @@
-; COMMAND-LINE: --nl-ext
-; EXPECT: unsat
-(set-logic QF_NIA)
-(declare-const n Int)
-(declare-const i1 Int)
-(declare-const i2 Int)
-(declare-const j1 Int)
-(declare-const j2 Int)
-(assert (>= n 0))
-(assert (not (= i1 i2)))
-(assert (<= 0 i1))
-(assert (<= i1 j1))
-(assert (< j1 n))
-(assert (<= 0 i2))
-(assert (<= i2 j2))
-(assert (< j2 n))
-(assert (or
-  (= (+ (* i1 n) j1) (+ (* i2 n) j2))
-  (= (+ (* i1 n) j1) (+ (* j2 n) i2))
-  (= (+ (* j1 n) i1) (+ (* i2 n) j2))
-  (= (+ (* j1 n) i1) (+ (* j2 n) i2))))
-(check-sat)
diff --git a/test/regress/regress3/siegel-nl-bases.smt2 b/test/regress/regress3/siegel-nl-bases.smt2
new file mode 100644
index 000000000..cf6e3ab5e
--- /dev/null
+++ b/test/regress/regress3/siegel-nl-bases.smt2
@@ -0,0 +1,22 @@
+; COMMAND-LINE: --nl-ext
+; EXPECT: unsat
+(set-logic QF_NIA)
+(declare-const n Int)
+(declare-const i1 Int)
+(declare-const i2 Int)
+(declare-const j1 Int)
+(declare-const j2 Int)
+(assert (>= n 0))
+(assert (not (= i1 i2)))
+(assert (<= 0 i1))
+(assert (<= i1 j1))
+(assert (< j1 n))
+(assert (<= 0 i2))
+(assert (<= i2 j2))
+(assert (< j2 n))
+(assert (or
+  (= (+ (* i1 n) j1) (+ (* i2 n) j2))
+  (= (+ (* i1 n) j1) (+ (* j2 n) i2))
+  (= (+ (* j1 n) i1) (+ (* i2 n) j2))
+  (= (+ (* j1 n) i1) (+ (* j2 n) i2))))
+(check-sat)