diff options
Diffstat (limited to 'test/regress')
-rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/regress/regress1/strings/indexof_re_red.smt2 | 7 |
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) |