diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-06-13 13:36:22 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-06-13 13:36:22 -0500 |
| commit | c4905e4aa2ec70929335497130f802254a0d4b4e (patch) | |
| tree | 777acc36953d9a2b504b248359b8b05e67dbb96f /test | |
| parent | a7c4cd3ecacb1e484a076edde0274c282bb43ffb (diff) | |
Fix simple regexp consume (#2066)
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/Makefile.tests | 1 | ||||
| -rw-r--r-- | test/regress/regress1/strings/issue2060.smt2 | 20 |
2 files changed, 21 insertions, 0 deletions
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests index fd4a7da39..41753720f 100644 --- a/test/regress/Makefile.tests +++ b/test/regress/Makefile.tests @@ -1444,6 +1444,7 @@ REG1_TESTS = \ regress1/strings/idof-triv.smt2 \ regress1/strings/ilc-l-nt.smt2 \ regress1/strings/issue1105.smt2 \ + regress1/strings/issue2060.smt2 \ regress1/strings/kaluza-fl.smt2 \ regress1/strings/loop002.smt2 \ regress1/strings/loop003.smt2 \ diff --git a/test/regress/regress1/strings/issue2060.smt2 b/test/regress/regress1/strings/issue2060.smt2 new file mode 100644 index 000000000..784fe1862 --- /dev/null +++ b/test/regress/regress1/strings/issue2060.smt2 @@ -0,0 +1,20 @@ +(set-logic QF_S) +(set-info :status sat) + +(declare-const action String) +(declare-const example_key String) + +(assert (str.in.re action (re.++ + (str.to.re "foobar:ab") + (re.* re.allchar) + ))) + +(declare-const action_1 String) +(declare-const action_2 String) + +(assert (and + (= action (str.++ action_1 example_key action_2)) + (= action_1 "foobar:a") + )) + +(check-sat) |