diff options
Diffstat (limited to 'test/regress/regress1/strings/cmu-substr-rw.smt2')
| -rw-r--r-- | test/regress/regress1/strings/cmu-substr-rw.smt2 | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/test/regress/regress1/strings/cmu-substr-rw.smt2 b/test/regress/regress1/strings/cmu-substr-rw.smt2 new file mode 100644 index 000000000..20bf979dd --- /dev/null +++ b/test/regress/regress1/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) + |