diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-12-04 18:17:55 -0600 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2014-12-04 18:17:55 -0600 |
| commit | f8c5e78d97eb7ddc3a29392c9ca18c627279fa2b (patch) | |
| tree | 597fe7c703d3d2bc8fc05440d3529d348bb6a1c8 /test | |
| parent | 31175341b81e26f7373d75f65cddc69386f0ac86 (diff) | |
Relaxed the constant requirement for regular expression loop;
Added "ignoring negative membership" option (fragment checking is not provided,
and users must make sure the constraint is in the fragment;
otherwise, the solution may not be correct).
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/strings/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/strings/regexp002.smt2 | 4 |
2 files changed, 6 insertions, 1 deletions
diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index 865d05cd2..8a2674cee 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -37,6 +37,7 @@ TESTS = \ model001.smt2 \ substr001.smt2 \ regexp001.smt2 \ + regexp002.smt2 \ regexp003.smt2 \ leadingzero001.smt2 \ loop001.smt2 \ @@ -53,8 +54,8 @@ TESTS = \ FAILING_TESTS = EXTRA_DIST = $(TESTS) \ + artemis-0512-nonterm.smt2 \ fmf001.smt2 \ - regexp002.smt2 \ type002.smt2 # slow after changes on Nov 20 : artemis-0512-nonterm.smt2 diff --git a/test/regress/regress0/strings/regexp002.smt2 b/test/regress/regress0/strings/regexp002.smt2 index 18541af4e..8c29ccb38 100644 --- a/test/regress/regress0/strings/regexp002.smt2 +++ b/test/regress/regress0/strings/regexp002.smt2 @@ -1,6 +1,10 @@ (set-logic QF_S)
(set-info :status sat)
(set-option :strings-exp true)
+; this option requires user to check whether the constraint is in the fragment
+; currently we do not provide only positive membership constraint checking
+; if users use this option but the constraint is not in this fragment, the result will fail
+(set-option :strings-inm true)
(declare-fun x () String)
(declare-fun y () String)
|