diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-10 15:48:05 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-10 15:48:05 -0600 |
| commit | e0009c822488a2c39f8907e37333409c1191d47b (patch) | |
| tree | bfc4c40a5d8789769ab5d4827aa9562986e0f475 /test | |
| parent | cef8ceaf4cd81863171363fe54a97921361d1de9 (diff) | |
Do not mark extended functions as reduced based on decomposing contains (#5407)
Fixes #5381.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress2/strings/issue5381.smt2 | 30 |
2 files changed, 31 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 58a43895e..9a0565d8e 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2174,6 +2174,7 @@ set(regress_2_tests regress2/strings/cmu-prereg-fmf.smt2 regress2/strings/cmu-repl-len-nterm.smt2 regress2/strings/issue3203.smt2 + regress2/strings/issue5381.smt2 regress2/strings/issue918.smt2 regress2/strings/non_termination_regular_expression6.smt2 regress2/strings/range-perf.smt2 diff --git a/test/regress/regress2/strings/issue5381.smt2 b/test/regress/regress2/strings/issue5381.smt2 new file mode 100644 index 000000000..6efd22a6e --- /dev/null +++ b/test/regress/regress2/strings/issue5381.smt2 @@ -0,0 +1,30 @@ +; COMMAND-LINE: --strings-fmf --strings-exp +; EXPECT: sat +(set-logic QF_SLIA) +(set-info :status sat) +; required for solving the benchmark, although the original benchmark only has an error when this is disabled +(set-option :strings-fmf true) +(declare-fun a () String) +(assert (not (= (ite (str.contains (str.++ (str.replace (str.substr + (str.substr (str.substr a 1 (- (str.len a) 1)) 0 (- (str.len + (str.substr a 1 (- (str.len a) 1))) 0)) 0 (- (+ (str.indexof (str.++ + (str.replace (str.substr (str.substr a 1 (- (str.len a) 1)) 0 1) "A" + "") "") "D" 0) 1) 0)) "" "") (str.substr (str.substr (str.substr a 1 + (- (str.len a) 1)) 1 (str.len (str.substr a 1 (- (str.len a) 1)))) 0 + (str.len (str.substr (str.substr a 1 (- (str.len a) 1)) 0 (str.len + (str.substr a 1 (- (str.len a) 1))))))) "F") 1 0) 0))) +(assert (= (ite (str.contains (str.substr (str.substr (str.substr a 1 + (- (str.len a) 1)) (+ (str.indexof (str.substr a 1 (- (str.len a) + 1)) "A" 0) 1) (str.len (str.substr a 1 (- (str.len a) 1)))) 0 (- + (str.len (str.substr (str.substr a 1 (- (str.len a) 1)) 0 (str.len + (str.substr a 1 (- (str.len a) 1))))) (+ (str.indexof (str.substr + (str.substr a 1 (- (str.len a) 1)) 1 (str.len (str.substr a 1 (- + (str.len a) 1)))) "D" 0) 1))) "D") 1 0) 0)) +(assert (not (= (ite (str.contains (str.substr (str.substr a 1 (- + (str.len a) 1)) 0 (str.len (str.substr a 1 (- (str.len a) 1)))) "D") + 1 0) 0))) +(assert (<= (+ (str.indexof (str.substr (str.substr a 1 (- (str.len a) + 1)) (+ (str.indexof (str.substr a 1 (- (str.len a) 1)) "A" 0) 1) (- + (str.len (str.substr a 1 (- (str.len a) 1))) 0)) "D" 0) 1) 0)) +(check-sat) +(exit) |