diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-06-08 18:47:40 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-06-08 23:47:40 +0000 |
| commit | ccd52accc3bd19c5bc5203d091d1fc0f8d48f8a3 (patch) | |
| tree | f28b36f9194ccb0a43d37cc0e472f171f3645c15 /test | |
| parent | 0ec38bbddf9b9e37f4535a6c782f42e03f4593e0 (diff) | |
Fix for 2 dimensional dependent bounded quantifiers (#6710)
This updates 2-dim dependent bounded quantifiers to not map constants to terms when computing ranges, when the type of the variable is closed enumerable. This is require to fix an incorrect model (possible solution unsoundness) issue in the reduction of str.indexof_re.
Fixes the 1st, 4th and 5th benchmarks from #6653. Fixes #6635.
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/CMakeLists.txt | 4 | ||||
| -rw-r--r-- | test/regress/regress1/strings/issue6635-rre.smt2 | 6 | ||||
| -rw-r--r-- | test/regress/regress1/strings/issue6653-4-rre.smt2 | 6 | ||||
| -rw-r--r-- | test/regress/regress1/strings/issue6653-rre-small.smt2 | 6 | ||||
| -rw-r--r-- | test/regress/regress1/strings/issue6653-rre.smt2 | 8 |
5 files changed, 30 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index a5a687f9f..4ee8e513e 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -2126,7 +2126,11 @@ set(regress_1_tests regress1/strings/issue6337-replace-re.smt2 regress1/strings/issue6567-empty-re-range.smt2 regress1/strings/issue6604-2.smt2 + regress1/strings/issue6635-rre.smt2 regress1/strings/issue6653-2-update-c-len.smt2 + regress1/strings/issue6653-4-rre.smt2 + regress1/strings/issue6653-rre.smt2 + regress1/strings/issue6653-rre-small.smt2 regress1/strings/kaluza-fl.smt2 regress1/strings/loop002.smt2 regress1/strings/loop003.smt2 diff --git a/test/regress/regress1/strings/issue6635-rre.smt2 b/test/regress/regress1/strings/issue6635-rre.smt2 new file mode 100644 index 000000000..cbca77783 --- /dev/null +++ b/test/regress/regress1/strings/issue6635-rre.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --strings-exp --re-elim --re-elim-agg +; EXPECT: unsat +(set-logic ALL) +(declare-fun a () String) +(assert (str.in_re (str.replace_re a (re.++ (str.to_re "A") (re.union (str.to_re "") (str.to_re (str.from_code (str.len a))))) "AB") (re.+ (str.to_re "A")))) +(check-sat) diff --git a/test/regress/regress1/strings/issue6653-4-rre.smt2 b/test/regress/regress1/strings/issue6653-4-rre.smt2 new file mode 100644 index 000000000..8de99a334 --- /dev/null +++ b/test/regress/regress1/strings/issue6653-4-rre.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --strings-exp --re-elim --re-elim-agg +; EXPECT: sat +(set-logic ALL) +(declare-fun x () String) +(assert (str.in_re (str.replace_re x (str.to_re "A") x) (re.++ (re.comp (str.to_re "A")) (str.to_re "A") re.allchar))) +(check-sat) diff --git a/test/regress/regress1/strings/issue6653-rre-small.smt2 b/test/regress/regress1/strings/issue6653-rre-small.smt2 new file mode 100644 index 000000000..c4b6a497b --- /dev/null +++ b/test/regress/regress1/strings/issue6653-rre-small.smt2 @@ -0,0 +1,6 @@ +; COMMAND-LINE: --strings-exp --strings-fmf --re-elim --re-elim-agg +; EXPECT: sat +(set-logic ALL) +(declare-fun a () String) +(assert (str.in_re a (re.+ (str.to_re (str.replace_re a (str.to_re a) "A"))))) +(check-sat) diff --git a/test/regress/regress1/strings/issue6653-rre.smt2 b/test/regress/regress1/strings/issue6653-rre.smt2 new file mode 100644 index 000000000..66b7dd64e --- /dev/null +++ b/test/regress/regress1/strings/issue6653-rre.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --strings-exp --re-elim --re-elim-agg +; EXPECT: sat +(set-logic ALL) +(declare-fun a () String) +(declare-fun b () String) +(assert (str.in_re (str.replace_re b (str.to_re (str.replace_all a (str.++ b "a") b)) (str.++ b "a")) (re.+ (str.to_re "b")))) +(assert (str.in_re a (re.* (re.range "a" "b")))) +(check-sat) |