Move slow string regression to regress3 (#2913)

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 55c777f80452a413a0cb154dcb032180f24b2e3d..c6ccab4643d2b96427b39fc2545904803410b7a2 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1749,7 +1749,6 @@ set(regress_2_tests
   regress2/strings/cmu-disagree-0707-dd.smt2
   regress2/strings/cmu-prereg-fmf.smt2
   regress2/strings/cmu-repl-len-nterm.smt2
-  regress2/strings/extf_d_perf.smt2
   regress2/strings/issue918.smt2
   regress2/strings/non_termination_regular_expression6.smt2
   regress2/strings/norn-dis-0707-3.smt2
@@ -1798,6 +1797,7 @@ set(regress_3_tests
   regress3/pp-regfile.smt
   regress3/qwh.35.405.shuffled-as.sat03-1651.smt
   regress3/sixfuncs.sy
+  regress3/strings/extf_d_perf.smt2
 )
 
 #-----------------------------------------------------------------------------#

diff --git a/test/regress/regress2/strings/extf_d_perf.smt2 b/test/regress/regress2/strings/extf_d_perf.smt2
deleted file mode 100644 (file)
index 7ad094d..0000000
--- a/test/regress/regress2/strings/extf_d_perf.smt2
+++ /dev/null
@@ -1,19 +0,0 @@
-; COMMAND-LINE: --strings-exp --strings-fmf
-; EXPECT: sat
-(set-logic ALL)
-(declare-fun _substvar_140_ () String)
-(declare-fun _substvar_195_ () Int)
-(declare-fun _substvar_201_ () Int)
-(assert (let ((_let_0 (str.substr _substvar_140_ 10 (+ 0 (str.len _substvar_140_))))) (let ((_let_3 (str.substr _let_0 0 (str.indexof _let_0 "/" 0)))) (let ((_let_4 (str.substr _let_3 0 7))) (let ((_let_5 (str.substr _let_3 8 (+ _substvar_201_ (str.len _let_3)))))
-  (and
-    (str.contains _substvar_140_ "://")
-    (str.contains _let_3 "@")
-    (str.contains _let_5 ",")
-    (not (= (str.len (str.substr _let_0 (+ 1 (str.indexof _let_0 "/" 0)) _substvar_195_)) 0))
-    (not (= (str.len _let_4) 0))
-    (not (str.contains _let_0 ".sock"))
-    (not (str.contains _let_4 "@"))
-    (not (= (str.len _let_5) 0))
-    (= "mongodb://" (str.substr _substvar_140_ 0 10))))))))
-(check-sat)
-

diff --git a/test/regress/regress3/strings/extf_d_perf.smt2 b/test/regress/regress3/strings/extf_d_perf.smt2
new file mode 100644 (file)
index 0000000..7ad094d
--- /dev/null
+++ b/test/regress/regress3/strings/extf_d_perf.smt2
@@ -0,0 +1,19 @@
+; COMMAND-LINE: --strings-exp --strings-fmf
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun _substvar_140_ () String)
+(declare-fun _substvar_195_ () Int)
+(declare-fun _substvar_201_ () Int)
+(assert (let ((_let_0 (str.substr _substvar_140_ 10 (+ 0 (str.len _substvar_140_))))) (let ((_let_3 (str.substr _let_0 0 (str.indexof _let_0 "/" 0)))) (let ((_let_4 (str.substr _let_3 0 7))) (let ((_let_5 (str.substr _let_3 8 (+ _substvar_201_ (str.len _let_3)))))
+  (and
+    (str.contains _substvar_140_ "://")
+    (str.contains _let_3 "@")
+    (str.contains _let_5 ",")
+    (not (= (str.len (str.substr _let_0 (+ 1 (str.indexof _let_0 "/" 0)) _substvar_195_)) 0))
+    (not (= (str.len _let_4) 0))
+    (not (str.contains _let_0 ".sock"))
+    (not (str.contains _let_4 "@"))
+    (not (= (str.len _let_5) 0))
+    (= "mongodb://" (str.substr _substvar_140_ 0 10))))))))
+(check-sat)
+