diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-10-06 13:26:03 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-10-06 13:26:03 +0200 |
| commit | 6343fbb0c9b238aeb1addca6449f95a01071c1ac (patch) | |
| tree | 60f872134b3697a88d639ffa5adf73c5db02c5d1 /test/regress/regress0/strings/norn-ab.smt2 | |
| parent | 645aaaa186269c26d96a60c8df3350a2de9b6acb (diff) | |
More improvements to strings rewriter for regexps, contains, indexof, replace and others. Enable non-recursive flat form inferences in strings theory solver. Refactor extf reductions. Use non-constant length terms when checking length equality. Add option --strings-eager-len.
Diffstat (limited to 'test/regress/regress0/strings/norn-ab.smt2')
| -rwxr-xr-x | test/regress/regress0/strings/norn-ab.smt2 | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/test/regress/regress0/strings/norn-ab.smt2 b/test/regress/regress0/strings/norn-ab.smt2 new file mode 100755 index 000000000..db7aac732 --- /dev/null +++ b/test/regress/regress0/strings/norn-ab.smt2 @@ -0,0 +1,25 @@ +(set-logic QF_SLIA)
+(set-info :status unsat)
+(set-option :strings-exp true)
+
+(declare-fun var_0 () String)
+(declare-fun var_1 () String)
+(declare-fun var_2 () String)
+(declare-fun var_3 () String)
+(declare-fun var_4 () String)
+(declare-fun var_5 () String)
+(declare-fun var_6 () String)
+(declare-fun var_7 () String)
+(declare-fun var_8 () String)
+(declare-fun var_9 () String)
+(declare-fun var_10 () String)
+(declare-fun var_11 () String)
+(declare-fun var_12 () String)
+
+(assert (str.in.re var_4 (re.++ (str.to.re "a") (re.* (str.to.re "b")))))
+(assert (str.in.re var_4 (re.++ (re.* (str.to.re "a")) (str.to.re "b"))))
+(assert (str.in.re var_4 (re.* (re.range "a" "u"))))
+(assert (str.in.re var_4 (re.++ (re.* (str.to.re "a")) (re.++ (str.to.re "b") (re.* (str.to.re "b"))))))
+(assert (not (str.in.re (str.++ "a" var_4 "b" ) (re.++ (re.* (str.to.re "a")) (re.++ (str.to.re "b") (re.* (str.to.re "b")))))))
+(assert (and (<= 0 (str.len var_4)) (not (not (exists ((v Int)) (= (* v 2 ) (+ (str.len var_4) 2 )))))))
+(check-sat)
\ No newline at end of file |