diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-07-21 10:56:09 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-07-21 10:56:09 -0500 |
commit | b5956e457da61e4d49cd35e0a73ba423230a25e0 (patch) | |
tree | 26fd0ce8f9bd511d967a2be2cbe9c6cd5dc21b08 /test/regress/regress0/strings/cmu-substr-rw.smt2 | |
parent | f827fb06c949d421fb32f6629c2c353ca7bd026e (diff) |
Fixes for strings, explanations for constant split propagations, substr under concat rewrite. Avoid duplicate re.range length lemmas.
Diffstat (limited to 'test/regress/regress0/strings/cmu-substr-rw.smt2')
-rw-r--r-- | test/regress/regress0/strings/cmu-substr-rw.smt2 | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/test/regress/regress0/strings/cmu-substr-rw.smt2 b/test/regress/regress0/strings/cmu-substr-rw.smt2 new file mode 100644 index 000000000..20bf979dd --- /dev/null +++ b/test/regress/regress0/strings/cmu-substr-rw.smt2 @@ -0,0 +1,12 @@ +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(set-option :strings-exp true) +;(set-option :produce-models true) +;(set-option :rewrite-divk true) + +(declare-fun uri () String) + +(assert (and (and (and (and (and (and (and (and (and (and (and (and (not (not (= (ite (= (str.len (str.substr (str.substr uri (+ (str.indexof uri "%" 0) 1) (- (str.len uri) (+ (str.indexof uri "%" 0) 1))) 0 (- 2 0))) 2) 1 0) 0))) (not (not (= (ite (str.contains (str.substr uri (+ (str.indexof uri "%" 0) 1) (- (str.len uri) (+ (str.indexof uri "%" 0) 1))) "%") 1 0) 0)))) (not (not (= (ite (= (str.len (str.substr uri (+ (str.indexof uri "%" 0) 1) (- (str.len uri) (+ (str.indexof uri "%" 0) 1)))) 0) 1 0) 0)))) (not (= (ite (str.contains uri "%") 1 0) 0))) (not (not (= (ite (= (str.len uri) 0) 1 0) 0)))) (>= (+ (str.indexof uri "%" 0) 1) 0)) (>= (- (str.len uri) (+ (str.indexof uri "%" 0) 1)) 0)) (>= 0 0)) (>= (- 2 0) 0)) (>= (+ (str.indexof uri "%" 0) 1) 0)) (>= (- (str.len uri) (+ (str.indexof uri "%" 0) 1)) 0)) (>= (+ (str.indexof uri "%" 0) 1) 0)) (>= (- (str.len uri) (+ (str.indexof uri "%" 0) 1)) 0))) + +(check-sat) + |