Move slow nl regression to regress3 (#4276)

Should fix nightlies.

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 06dc2d87c7e780e5066c13f7708ca51ffe67e81d..01092cf6e27615ab8f74f81b9001c5f551506932 100644 (file)
--- 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 (file)
index cf6e3ab..0000000
--- 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 (file)
index 0000000..cf6e3ab
--- /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)