diff options
Diffstat (limited to 'test/regress/regress1/strings/cmu-repl-len-nterm.smt2')
-rw-r--r-- | test/regress/regress1/strings/cmu-repl-len-nterm.smt2 | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/test/regress/regress1/strings/cmu-repl-len-nterm.smt2 b/test/regress/regress1/strings/cmu-repl-len-nterm.smt2 new file mode 100644 index 000000000..004db77ed --- /dev/null +++ b/test/regress/regress1/strings/cmu-repl-len-nterm.smt2 @@ -0,0 +1,12 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: sat +(set-logic ALL_SUPPORTED) +(set-info :status sat) + +(declare-fun url () String) + +(assert (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (not (not (= (ite (str.contains (str.++ (str.replace (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) 0 (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) 0)) "B" "b") (str.++ (str.replace (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1))) 0 (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1))) "B" 0) 1) 0)) "B" "b") (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1))) "B" 0) 1) (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1))) "B" 0) 1))))) "C") 1 0) 0)))) (not (not (= (ite (str.contains (str.substr (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1))) "B" 0) 1) (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1))) "B" 0) 1))) "B") 1 0) 0)))) (not (= (ite (str.contains (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1))) "B") 1 0) 0))) (not (= (ite (str.contains (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B") 1 0) 0))) (not (not (= (ite (str.contains (str.substr url 0 (- (str.indexof url ":" 0) 0)) "A") 1 0) 0)))) (not (not (= (ite (not (= (str.len (str.substr url (+ (str.indexof url ":" 0) 1) (- (str.len url) (+ (str.indexof url ":" 0) 1)))) 0)) 1 0) 0)))) (not (not (= (ite (= (str.substr url 0 (- (str.indexof url ":" 0) 0)) "http") 1 0) 0)))) (not (= (ite (> (str.indexof url ":" 0) 0) 1 0) 0))) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1)) 0)) (>= 0 0)) (>= (- (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1))) "B" 0) 1) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1)) 0)) (>= (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1))) "B" 0) 1) 0)) (>= (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1))) "B" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1)) 0)) (>= (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1))) "B" 0) 1) 0)) (>= (- (str.len (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1)))) (+ (str.indexof (str.substr (str.substr url 0 (- (str.indexof url ":" 0) 0)) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1))) "B" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1) 0)) (>= (- (str.len (str.substr url 0 (- (str.indexof url ":" 0) 0))) (+ (str.indexof (str.substr url 0 (- (str.indexof url ":" 0) 0)) "B" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0)) (>= (+ (str.indexof url ":" 0) 1) 0)) (>= (- (str.len url) (+ (str.indexof url ":" 0) 1)) 0)) (>= 0 0)) (>= (- (str.indexof url ":" 0) 0) 0))) + +(check-sat) + +;(get-value (url)) |