From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 22 Dec 2020 20:07:19 +0000 (-0600)
Subject: Move slow regression to regress3 (#5715)
X-Git-Tag: cvc5-1.0.0~2410
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2f73122d32e3272b1a9727857b6ac02d2da871d3;p=cvc5.git

Move slow regression to regress3 (#5715)
---

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 2c480da3a..2a3cfd9ea 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1719,7 +1719,6 @@ set(regress_1_tests
   regress1/quantifiers/issue4243-prereg-inc.smt2
   regress1/quantifiers/issue4290-cegqi-r.smt2
   regress1/quantifiers/issue4433-nqe.smt2
-  regress1/quantifiers/issue4476-ext-rew.smt2
   regress1/quantifiers/issue4620-erq-witness-unsound.smt2
   regress1/quantifiers/issue4685-wrewrite.smt2
   regress1/quantifiers/issue4849-nqe.smt2
@@ -2384,6 +2383,7 @@ set(regress_3_tests
   regress3/interpol2.smt2
   regress3/inv_gen_n_c11.sy
   regress3/issue4170.smt2
+  regress3/issue4476-ext-rew.smt2
   regress3/issue4714.smt2
   regress3/lpsat-goal-9.smt2
   regress3/nia-max-square.sy
diff --git a/test/regress/regress1/quantifiers/issue4476-ext-rew.smt2 b/test/regress/regress1/quantifiers/issue4476-ext-rew.smt2
deleted file mode 100644
index 8f1d8285d..000000000
--- a/test/regress/regress1/quantifiers/issue4476-ext-rew.smt2
+++ /dev/null
@@ -1,7 +0,0 @@
-; COMMAND-LINE: --sygus-inst --no-check-models
-; EXPECT: sat
-(set-logic NRA)
-(set-info :status sat)
-(set-option :ext-rewrite-quant true)
-(assert (exists ((a Real) (b Real)) (forall ((c Real)) (= (/ b (/ 1 c)) 0))))
-(check-sat)
diff --git a/test/regress/regress3/issue4476-ext-rew.smt2 b/test/regress/regress3/issue4476-ext-rew.smt2
new file mode 100644
index 000000000..8f1d8285d
--- /dev/null
+++ b/test/regress/regress3/issue4476-ext-rew.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --sygus-inst --no-check-models
+; EXPECT: sat
+(set-logic NRA)
+(set-info :status sat)
+(set-option :ext-rewrite-quant true)
+(assert (exists ((a Real) (b Real)) (forall ((c Real)) (= (/ b (/ 1 c)) 0))))
+(check-sat)