summaryrefslogtreecommitdiff
path: root/test/regress
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress')
-rw-r--r--test/regress/CMakeLists.txt1
-rw-r--r--test/regress/regress1/strings/indexof_re_red.smt27
2 files changed, 1 insertions, 7 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index d3922ed5c..de3ce6f2b 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2526,6 +2526,7 @@ set(regress_3_tests
regress3/specsharp-WindowsCard.15.RTE.Terminate_System.Int32.smt2
regress3/strings-any-term.sy
regress3/strings/extf_d_perf.smt2
+ regress3/strings/indexof_re_red.smt2
regress3/strings/norn-dis-0707-3.smt2
regress3/strings/replace_re_all.smt2
regress3/unbdd_inv_gen_ex7.sy
diff --git a/test/regress/regress1/strings/indexof_re_red.smt2 b/test/regress/regress1/strings/indexof_re_red.smt2
index 34e80d8ea..f32a6723b 100644
--- a/test/regress/regress1/strings/indexof_re_red.smt2
+++ b/test/regress/regress1/strings/indexof_re_red.smt2
@@ -32,13 +32,6 @@
(pop)
(push)
-(assert (= i (str.indexof_re x (re.++ re.all (str.to_re "a") re.all) 0)))
-(assert (not (or (= i 0) (= i (- 1)))))
-(set-info :status unsat)
-(check-sat)
-(pop)
-
-(push)
(assert (= 2 (str.indexof_re x (str.to_re "a") 1)))
(set-info :status sat)
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback