diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-06-24 10:30:27 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-06-24 10:30:27 -0500 |
| commit | d3e83102fde7d5e43f132efa80c651a43af5afa3 (patch) | |
| tree | 0a275fb00d0df13bb965486d2484ba1ee2105bc3 /test/regress | |
| parent | 5d6664a43c8ea3400b0f38797c937568d8d0ca2a (diff) | |
Stratify unfolding of regular expressions based on polarity (#3067)
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress1/strings/regexp-strat-fix.smt2 | 8 |
2 files changed, 9 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index f3abe2c87..3c5d82fa8 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1580,6 +1580,7 @@ set(regress_1_tests regress1/strings/regexp001.smt2 regress1/strings/regexp002.smt2 regress1/strings/regexp003.smt2 + regress1/strings/regexp-strat-fix.smt2 regress1/strings/reloop.smt2 regress1/strings/repl-empty-sem.smt2 regress1/strings/repl-soundness-sem.smt2 diff --git a/test/regress/regress1/strings/regexp-strat-fix.smt2 b/test/regress/regress1/strings/regexp-strat-fix.smt2 new file mode 100644 index 000000000..9ff78c935 --- /dev/null +++ b/test/regress/regress1/strings/regexp-strat-fix.smt2 @@ -0,0 +1,8 @@ +(set-info :smt-lib-version 2.5) +(set-logic QF_S) +(set-info :status unsat) +(set-option :strings-exp true) +(declare-fun var0 () String) +(assert (str.in.re var0 (re.* (re.* (str.to.re "0"))))) +(assert (not (str.in.re var0 (re.union (re.+ (str.to.re "0")) (re.* (str.to.re "1")))))) +(check-sat) |