diff options
Diffstat (limited to 'test/regress/regress0/strings')
56 files changed, 2 insertions, 969 deletions
diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index 7f7511e74..23b13aea2 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -19,85 +19,31 @@ MAKEFLAGS = -k # If a test shouldn't be run in e.g. competition mode, # put it below in "TESTS +=" TESTS = \ - at001.smt2 \ bug001.smt2 \ bug002.smt2 \ escchar.smt2 \ escchar_25.smt2 \ - str001.smt2 \ - str002.smt2 \ str003.smt2 \ str004.smt2 \ str005.smt2 \ - str006.smt2 \ - str007.smt2 \ - fmf002.smt2 \ type001.smt2 \ - type003.smt2 \ model001.smt2 \ - substr001.smt2 \ - regexp001.smt2 \ - regexp002.smt2 \ - regexp003.smt2 \ leadingzero001.smt2 \ loop001.smt2 \ - loop002.smt2 \ - loop003.smt2 \ - loop004.smt2 \ - loop005.smt2 \ - loop006.smt2 \ - loop007.smt2 \ - loop008.smt2 \ - loop009.smt2 \ - reloop.smt2 \ unsound-0908.smt2 \ - ilc-like.smt2 \ - ilc-l-nt.smt2 \ - artemis-0512-nonterm.smt2 \ + ilc-like.smt2 \ indexof-sym-simp.smt2 \ bug613.smt2 \ - idof-triv.smt2 \ - chapman150408.smt2 \ - pierre150331.smt2 \ - norn-360.smt2 \ norn-simp-rew.smt2 \ - norn-simp-rew-sat.smt2 \ - idof-nconst-index.smt2 \ - idof-neg-index.smt2 \ bug612.smt2 \ - bug615.smt2 \ - kaluza-fl.smt2 \ idof-rewrites.smt2 \ - bug682.smt2 \ - bug686dd.smt2 \ - idof-handg.smt2 \ - fmf001.smt2 \ - crash-1019.smt2 \ norn-31.smt2 \ strings-native-simple.cvc \ - cmu-2db2-extf-reg.smt2 \ - norn-nel-bug-052116.smt2 \ - cmu-disagree-0707-dd.smt2 \ - nf-ff-contains-abs.smt2 \ - csp-prefix-exp-bug.smt2 \ - cmu-substr-rw.smt2 \ - gm-inc-071516-2.smt2 \ - cmu-inc-nlpp-071516.smt2 \ - strings-index-empty.smt2 \ - bug768.smt2 \ - username_checker_min.smt2 \ - repl-empty-sem.smt2 \ - bug799-min.smt2 \ strings-charat.cvc \ - issue1105.smt2 \ issue1189.smt2 \ rewrites-v2.smt2 \ substr-rewrites.smt2 \ - norn-ab.smt2 \ - type002.smt2 \ - strip-endpt-sound.smt2 \ - repl-rewrites2.smt2 \ - repl-soundness-sem.smt2 + repl-rewrites2.smt2 FAILING_TESTS = @@ -106,9 +52,6 @@ EXTRA_DIST = $(TESTS) # and make sure to distribute it EXTRA_DIST += -#norn-dis-0707-3.smt2 - - # synonyms for "check" .PHONY: regress regress0 test regress regress0 test: check diff --git a/test/regress/regress0/strings/artemis-0512-nonterm.smt2 b/test/regress/regress0/strings/artemis-0512-nonterm.smt2 deleted file mode 100644 index 4b1cad8f6..000000000 --- a/test/regress/regress0/strings/artemis-0512-nonterm.smt2 +++ /dev/null @@ -1,26 +0,0 @@ -(set-logic QF_S) -(set-option :strings-exp true) -(set-info :status unsat) - -(declare-const Y String) -(assert - (or - (= Y "01") - (= Y "02") - (= Y "03") - (= Y "04") - (= Y "05") - (= Y "06") - (= Y "07") - (= Y "08") - (= Y "09") - (= Y "10") - (= Y "11") - (= Y "12") - ) -) - -(assert (= (<= (str.to.int Y) 31) false)) - -(check-sat) - diff --git a/test/regress/regress0/strings/at001.smt2 b/test/regress/regress0/strings/at001.smt2 deleted file mode 100644 index 2ecbcc993..000000000 --- a/test/regress/regress0/strings/at001.smt2 +++ /dev/null @@ -1,12 +0,0 @@ -(set-logic QF_S) -(set-info :status sat) - -(declare-fun x () String) -(declare-fun i () Int) - -(assert (= (str.at x i) "b")) -(assert (and (>= i 4) (< i (str.len x)))) -(assert (< (str.len x) 7)) -(assert (> (str.len x) 2)) - -(check-sat) diff --git a/test/regress/regress0/strings/bug615.smt2 b/test/regress/regress0/strings/bug615.smt2 deleted file mode 100644 index 86cc592fb..000000000 --- a/test/regress/regress0/strings/bug615.smt2 +++ /dev/null @@ -1,26 +0,0 @@ -(set-logic QF_S) -(set-option :strings-exp true) -(set-info :status sat) - -(declare-fun s () String) -;(assert (= s "</script><script>alert(1);</script><script>")) - -(declare-fun joined () String) -(assert (= joined (str.++ "<script>console.log('" s "');</script>"))) -(assert (str.contains joined "<script>alert(1);</script>")) - -; (<script>[^<]*</script>)+ -(assert (str.in.re joined - (re.+ (re.++ - (str.to.re "<script>") - (re.* - (re.union - (re.range " " ";") - (re.range "=" "~") - ) - ) - (str.to.re "</script>") - )) - )) - -(check-sat) diff --git a/test/regress/regress0/strings/bug682.smt2 b/test/regress/regress0/strings/bug682.smt2 deleted file mode 100644 index 6617b6b97..000000000 --- a/test/regress/regress0/strings/bug682.smt2 +++ /dev/null @@ -1,19 +0,0 @@ -; COMMAND-LINE: --incremental --strings-exp -(set-logic QF_S) - -(declare-fun a () String) -(define-fun replace3 ((x String) (y String) (z String)) String (str.replace x y z) ) - -(push 1) -(assert (= (replace3 a "5" "3") "333")) -(assert (str.contains a "5")) -; EXPECT: sat -(check-sat) -(pop 1) - -(push 1) -(assert (= (replace3 a "5" "3") "333")) -(assert (str.contains a "5")) -; EXPECT: sat -(check-sat) -(pop 1) diff --git a/test/regress/regress0/strings/bug686dd.smt2 b/test/regress/regress0/strings/bug686dd.smt2 deleted file mode 100644 index 7c923654d..000000000 --- a/test/regress/regress0/strings/bug686dd.smt2 +++ /dev/null @@ -1,13 +0,0 @@ -(set-logic UFDTSLIA) -(set-info :status sat) - -(declare-datatypes ((T 0)) ( ((TC (TCb String))) ) ) - -(declare-fun root5 () String) -(declare-fun root6 () T) - -(assert (and -(str.in.re root5 (re.loop (re.range "0" "9") 4 4) ) -(str.in.re (TCb root6) (re.loop (re.range "0" "9") 4 4) ) -) ) -(check-sat) diff --git a/test/regress/regress0/strings/bug768.smt2 b/test/regress/regress0/strings/bug768.smt2 deleted file mode 100644 index be3f24200..000000000 --- a/test/regress/regress0/strings/bug768.smt2 +++ /dev/null @@ -1,10 +0,0 @@ -(set-logic QF_S) -(set-info :status sat) -(declare-fun f0 () String) -(declare-fun c0 () String) -(declare-fun f1 () String) -(declare-fun f2 () String) - -(assert (= (str.++ f0 f1 f0 c0 f1 c0 f2 f2) "f(,f(c,c))")) - -(check-sat) diff --git a/test/regress/regress0/strings/bug799-min.smt2 b/test/regress/regress0/strings/bug799-min.smt2 deleted file mode 100644 index 06acffc97..000000000 --- a/test/regress/regress0/strings/bug799-min.smt2 +++ /dev/null @@ -1,18 +0,0 @@ -; COMMAND-LINE: --incremental --strings-exp -; EXPECT: sat -(set-logic ALL) -(set-info :status sat) - -(declare-fun u () String) -(declare-fun s () String) - -(assert (= (str.len u) 9)) -(assert (= (str.at u 1) s)) -(assert (= (str.at u 2) "4")) -(assert (= (str.at u 7) "5")) -(assert (= (str.at u 8) "6")) - -(push 1) -(assert (str.in.re s (re.range "0" "3"))) - -(check-sat) diff --git a/test/regress/regress0/strings/chapman150408.smt2 b/test/regress/regress0/strings/chapman150408.smt2 deleted file mode 100644 index f03718556..000000000 --- a/test/regress/regress0/strings/chapman150408.smt2 +++ /dev/null @@ -1,10 +0,0 @@ -(set-logic SLIA) -(set-info :status sat) -(set-option :strings-exp true) -(set-option :rewrite-divk true) -(declare-fun string () String) -(assert (and - (and (not (not (not (= (ite (> (str.indexof string ";" 0) 0) 1 0) - 0)))) (not (= (ite (not (= (str.len string) 0)) 1 0) 0))) (not - (not (= (ite (str.contains string "]") 1 0) 0))))) -(check-sat) diff --git a/test/regress/regress0/strings/cmu-2db2-extf-reg.smt2 b/test/regress/regress0/strings/cmu-2db2-extf-reg.smt2 deleted file mode 100644 index b513494b8..000000000 --- a/test/regress/regress0/strings/cmu-2db2-extf-reg.smt2 +++ /dev/null @@ -1,9 +0,0 @@ -(set-logic ALL_SUPPORTED) -(set-info :status sat) -(set-option :strings-exp true) - -(declare-fun s () String) - -(assert (and (not (not (= (ite (= (str.indexof s "bar" 1) (- 1)) 1 0) 0))) (not (not (= (ite (= (str.indexof s "bar" 1) 3) 1 0) 0))))) - -(check-sat) diff --git a/test/regress/regress0/strings/cmu-disagree-0707-dd.smt2 b/test/regress/regress0/strings/cmu-disagree-0707-dd.smt2 deleted file mode 100644 index c44dfa396..000000000 --- a/test/regress/regress0/strings/cmu-disagree-0707-dd.smt2 +++ /dev/null @@ -1,22 +0,0 @@ -(set-logic ALL_SUPPORTED) -(set-info :status sat) -(set-option :strings-exp true) - -(declare-fun url () String) - -(assert -(and -(and -(and -(and - -(= (str.len (str.substr (str.substr url (str.indexof url "#" 2) (- (str.len url) (str.indexof url "#" 2))) (+ (str.indexof (str.substr url (str.indexof url "#" 2) (- (str.len url) (str.indexof url "#" 2))) "#" 0) 1) (- (str.len (str.substr url (str.indexof url "#" 2) (- (str.len url) (str.indexof url "#" 2)))) (+ (str.indexof (str.substr url (str.indexof url "#" 2) (- (str.len url) (str.indexof url "#" 2))) "#" 0) 1)))) 0) - -(not (= (str.substr url 0 (- (str.indexof url ":" 0) 0)) "http"))) -(> (str.indexof url ":" 0) 0)) -(>= (- (str.indexof url "#" 2) 2) 0)) -(>= (str.indexof url ":" 0) 0)) -) - -(check-sat) - diff --git a/test/regress/regress0/strings/cmu-inc-nlpp-071516.smt2 b/test/regress/regress0/strings/cmu-inc-nlpp-071516.smt2 deleted file mode 100644 index 1208ca169..000000000 --- a/test/regress/regress0/strings/cmu-inc-nlpp-071516.smt2 +++ /dev/null @@ -1,9 +0,0 @@ -(set-logic ALL_SUPPORTED) -(set-info :status unsat) -(set-option :strings-exp true) - -(declare-fun url () String) - -(assert (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (not (= (ite (> (str.indexof url ":" 0) 0) 1 0) 0))) (not (= (ite (str.contains url "javascript:alert(1);") 1 0) 0))) (not (not (= (ite (= (str.len url) 0) 1 0) 0)))) (not (not (= (ite (= (str.at url 0) " ") 1 0) 0)))) (not (not (= (ite (= (str.at url 0) "\t") 1 0) 0)))) (not (not (= (ite (= (str.at url 0) "\n") 1 0) 0)))) (not (not (= (ite (= (str.at url 0) "\r") 1 0) 0)))) (not (not (= (ite (= (str.at url 0) "\v") 1 0) 0)))) (not (not (= (ite (= (str.at url 0) "\f") 1 0) 0)))) (not (not (= (ite (= (str.at url (- (str.len url) 1)) " ") 1 0) 0)))) (not (not (= (ite (= (str.at url (- (str.len url) 1)) "\t") 1 0) 0)))) (not (not (= (ite (= (str.at url (- (str.len url) 1)) "\n") 1 0) 0)))) (not (not (= (ite (= (str.at url (- (str.len url) 1)) "\r") 1 0) 0)))) (not (not (= (ite (= (str.at url (- (str.len url) 1)) "\v") 1 0) 0)))) (not (not (= (ite (= (str.at url (- (str.len url) 1)) "\f") 1 0) 0)))) (not (= (ite (str.prefixof "javascript:alert(1);" url) 1 0) 0)))) - -(check-sat) diff --git a/test/regress/regress0/strings/cmu-substr-rw.smt2 b/test/regress/regress0/strings/cmu-substr-rw.smt2 deleted file mode 100644 index 20bf979dd..000000000 --- a/test/regress/regress0/strings/cmu-substr-rw.smt2 +++ /dev/null @@ -1,12 +0,0 @@ -(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) - diff --git a/test/regress/regress0/strings/crash-1019.smt2 b/test/regress/regress0/strings/crash-1019.smt2 deleted file mode 100644 index 9f2e99b02..000000000 --- a/test/regress/regress0/strings/crash-1019.smt2 +++ /dev/null @@ -1,10 +0,0 @@ -(set-logic ALL_SUPPORTED) -(set-option :strings-exp true) -(set-option :rewrite-divk true) -(set-info :status unsat) - -(declare-fun s () 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 (not (not (not (= (ite (= (str.++ (str.replace (str.substr s 0 (- (+ (str.indexof s "o" 0) 1) 0)) "o" "a") (str.++ (str.replace (str.substr (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) 0 (- (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1) 0)) "o" "a") (str.substr (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1) (- (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1))))) "faa") 1 0) 0)))) (not (not (= (ite (str.contains (str.substr (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1) (- (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1))) "o") 1 0) 0)))) (not (= (ite (str.contains (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o") 1 0) 0))) (not (= (ite (str.contains s "o") 1 0) 0))) (>= 0 0)) (> (- (+ (str.indexof s "o" 0) 1) 0) 0)) (> (str.len s) 0)) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= 0 0)) (> (- (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1) 0) 0)) (> (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) 0)) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1) 0)) (> (- (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1)) 0)) (> (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1) 0)) (> (- (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1)) 0)) (> (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1)))) - -(check-sat) diff --git a/test/regress/regress0/strings/csp-prefix-exp-bug.smt2 b/test/regress/regress0/strings/csp-prefix-exp-bug.smt2 deleted file mode 100644 index c2fb4175c..000000000 --- a/test/regress/regress0/strings/csp-prefix-exp-bug.smt2 +++ /dev/null @@ -1,10 +0,0 @@ -(set-logic QF_S) -(set-info :status sat) - -(declare-fun x () String) -(declare-fun y () String) -(declare-fun z () String) - -(assert (= (str.len x) 1)) -(assert (= (str.++ x y "b" z) "aaaba")) -(check-sat) diff --git a/test/regress/regress0/strings/fmf001.smt2 b/test/regress/regress0/strings/fmf001.smt2 deleted file mode 100644 index 6081c8e06..000000000 --- a/test/regress/regress0/strings/fmf001.smt2 +++ /dev/null @@ -1,20 +0,0 @@ -(set-logic QF_S) -(set-option :strings-exp true) -(set-option :strings-fmf true) -(set-info :status sat) - -(declare-fun x () String) -(declare-fun y () String) - -(assert (str.in.re x - (re.* (re.++ (re.* (str.to.re "a") ) (str.to.re "b") )) - )) - -(assert (str.in.re y - (re.* (re.++ (re.* (str.to.re "a") ) (str.to.re "b") )) - )) - -(assert (not (= x y))) -(assert (= (str.len x) (str.len y))) - -(check-sat) diff --git a/test/regress/regress0/strings/fmf002.smt2 b/test/regress/regress0/strings/fmf002.smt2 deleted file mode 100644 index d52dae2d2..000000000 --- a/test/regress/regress0/strings/fmf002.smt2 +++ /dev/null @@ -1,17 +0,0 @@ -(set-logic QF_S) -(set-option :strings-exp true) -(set-option :strings-fmf true) -(set-info :status sat) - -(declare-fun x () String) -(declare-fun y () String) -(declare-fun z () String) - -(assert (str.in.re x - (re.+ (re.range "a" "c")) - )) - -(assert (= x (str.++ y "c" z "b"))) -(assert (> (str.len z) 1)) - -(check-sat) diff --git a/test/regress/regress0/strings/gm-inc-071516-2.smt2 b/test/regress/regress0/strings/gm-inc-071516-2.smt2 deleted file mode 100644 index 1650190f8..000000000 --- a/test/regress/regress0/strings/gm-inc-071516-2.smt2 +++ /dev/null @@ -1,10 +0,0 @@ -(set-logic ALL_SUPPORTED) -(set-info :status unsat) -(set-option :strings-exp true) - -(declare-fun value2 () String) -(declare-fun key2 () String) - -(assert (and (and (and (and (and (and (not (not (= (ite (str.contains value2 "=") 1 0) 0))) (not (not (= (ite (= (str.len value2) 0) 1 0) 0)))) (not (= (ite (not (= (str.indexof value2 "=" 0) (- 1))) 1 0) 0))) (not (not (= (ite (str.contains value2 ",") 1 0) 0)))) (not (not (= (ite (= (str.len value2) 0) 1 0) 0)))) (not (= (ite (= key2 "cache-control") 1 0) 0))) (not (= (ite (= key2 "cache-control") 1 0) 0)))) - -(check-sat) diff --git a/test/regress/regress0/strings/idof-handg.smt2 b/test/regress/regress0/strings/idof-handg.smt2 deleted file mode 100644 index 40aff3168..000000000 --- a/test/regress/regress0/strings/idof-handg.smt2 +++ /dev/null @@ -1,7 +0,0 @@ -(set-logic ALL_SUPPORTED) -(set-option :strings-exp true) -(set-info :status sat) -(declare-fun s () String) -(assert (str.contains s "Hello and goodbye!")) -(assert (> (str.indexof s "goodbye" 0) (str.indexof s "Hello" 0))) -(check-sat)
\ No newline at end of file diff --git a/test/regress/regress0/strings/idof-nconst-index.smt2 b/test/regress/regress0/strings/idof-nconst-index.smt2 deleted file mode 100644 index eba492220..000000000 --- a/test/regress/regress0/strings/idof-nconst-index.smt2 +++ /dev/null @@ -1,9 +0,0 @@ -(set-logic ALL_SUPPORTED) -(set-option :strings-exp true) -(set-info :status sat) -(declare-fun s () String) -(assert (str.contains s "Hello and goodbye!")) -(declare-fun x () Int) -(assert (<= (str.len s) x)) -(assert (not (= (str.indexof s "goodbye" (- x 30)) (- 1)))) -(check-sat) diff --git a/test/regress/regress0/strings/idof-neg-index.smt2 b/test/regress/regress0/strings/idof-neg-index.smt2 deleted file mode 100644 index c24fcc00a..000000000 --- a/test/regress/regress0/strings/idof-neg-index.smt2 +++ /dev/null @@ -1,8 +0,0 @@ -(set-logic ALL_SUPPORTED) -(set-option :strings-exp true) -(set-info :status unsat) -(declare-fun s () String) -(declare-fun x () Int) -(assert (< x 0)) -(assert (>= (str.indexof s "goodbye" x) 0)) -(check-sat) diff --git a/test/regress/regress0/strings/idof-triv.smt2 b/test/regress/regress0/strings/idof-triv.smt2 deleted file mode 100644 index 314adedf8..000000000 --- a/test/regress/regress0/strings/idof-triv.smt2 +++ /dev/null @@ -1,7 +0,0 @@ -(set-logic ALL_SUPPORTED) -(set-info :status sat) -(set-option :strings-exp true) -(declare-fun string () String) -;(assert (= string "::")) -(assert (> (str.indexof string ":" 0) 0)) -(check-sat) diff --git a/test/regress/regress0/strings/ilc-l-nt.smt2 b/test/regress/regress0/strings/ilc-l-nt.smt2 deleted file mode 100644 index 9e1cc2bc5..000000000 --- a/test/regress/regress0/strings/ilc-l-nt.smt2 +++ /dev/null @@ -1,14 +0,0 @@ -(set-logic ALL_SUPPORTED) -(set-info :status unsat) -(set-option :strings-exp true) - -(declare-fun s () String) -(assert (or (= s "Id like cookies.") (= s "Id not like cookies."))) - -(declare-fun target () String) -(assert (or (= target "l") (= target "m"))) - -(declare-fun location () Int) -(assert (= (* 2 location) (str.indexof s target 0))) - -(check-sat)
\ No newline at end of file diff --git a/test/regress/regress0/strings/issue1105.smt2 b/test/regress/regress0/strings/issue1105.smt2 deleted file mode 100644 index 81e7672da..000000000 --- a/test/regress/regress0/strings/issue1105.smt2 +++ /dev/null @@ -1,10 +0,0 @@ -(set-logic ALL) -(set-option :strings-exp true) -(set-info :status sat) -(declare-datatype Val ( - (Str (str String)) - (Num (num Int)))) - -(declare-const var0 Val) -(assert (=> (is-Str var0) (distinct (str.to.int (str var0)) (- 1)))) -(check-sat) diff --git a/test/regress/regress0/strings/kaluza-fl.smt2 b/test/regress/regress0/strings/kaluza-fl.smt2 deleted file mode 100644 index 04775d61c..000000000 --- a/test/regress/regress0/strings/kaluza-fl.smt2 +++ /dev/null @@ -1,97 +0,0 @@ -(set-logic QF_S) -(set-info :status sat) - -(declare-fun I0_15 () Int) -(declare-fun I0_18 () Int) -(declare-fun I0_2 () Int) -(declare-fun I0_4 () Int) -(declare-fun I0_6 () Int) -(declare-fun PCTEMP_LHS_1 () Int) -(declare-fun PCTEMP_LHS_2 () Int) -(declare-fun PCTEMP_LHS_3 () Int) -(declare-fun PCTEMP_LHS_4 () Int) -(declare-fun PCTEMP_LHS_5 () Int) -(declare-fun T0_15 () String) -(declare-fun T0_18 () String) -(declare-fun T0_2 () String) -(declare-fun T0_4 () String) -(declare-fun T0_6 () String) -(declare-fun T1_15 () String) -(declare-fun T1_18 () String) -(declare-fun T1_2 () String) -(declare-fun T1_4 () String) -(declare-fun T1_6 () String) -(declare-fun T2_15 () String) -(declare-fun T2_18 () String) -(declare-fun T2_2 () String) -(declare-fun T2_4 () String) -(declare-fun T2_6 () String) -(declare-fun T3_15 () String) -(declare-fun T3_18 () String) -(declare-fun T3_2 () String) -(declare-fun T3_4 () String) -(declare-fun T3_6 () String) -(declare-fun T4_15 () String) -(declare-fun T4_18 () String) -(declare-fun T4_2 () String) -(declare-fun T4_4 () String) -(declare-fun T4_6 () String) -(declare-fun T5_15 () String) -(declare-fun T5_18 () String) -(declare-fun T5_2 () String) -(declare-fun T5_4 () String) -(declare-fun T5_6 () String) -(declare-fun T_4 () Bool) -(declare-fun T_5 () Bool) -(declare-fun T_6 () Bool) -(declare-fun T_7 () Bool) -(declare-fun T_8 () Bool) -(declare-fun T_9 () Bool) -(declare-fun T_SELECT_1 () Bool) -(declare-fun T_SELECT_2 () Bool) -(declare-fun T_SELECT_3 () Bool) -(declare-fun T_SELECT_4 () Bool) -(declare-fun T_SELECT_5 () Bool) -(declare-fun T_a () Bool) -(declare-fun T_c () Bool) -(declare-fun T_e () Bool) -(declare-fun var_0xINPUT_12454 () String) - -(assert (= T_SELECT_1 (not (= PCTEMP_LHS_1 (- 1))))) -(assert (ite T_SELECT_1 - (and (= PCTEMP_LHS_1 (+ I0_2 0))(= var_0xINPUT_12454 (str.++ T0_2 T1_2))(= I0_2 (str.len T4_2))(= 0 (str.len T0_2))(= T1_2 (str.++ T2_2 T3_2))(= T2_2 (str.++ T4_2 T5_2))(= T5_2 "__utma=169413169.")(not (str.in.re T4_2 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "a") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "."))))) - (and (= PCTEMP_LHS_1 (- 1))(= var_0xINPUT_12454 (str.++ T0_2 T1_2))(= 0 (str.len T0_2))(not (str.in.re T1_2 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "a") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "."))))))) -(assert (= T_SELECT_2 (not (= PCTEMP_LHS_2 (- 1))))) -(assert (ite T_SELECT_2 - (and (= PCTEMP_LHS_2 (+ I0_4 0))(= var_0xINPUT_12454 (str.++ T0_4 T1_4))(= I0_4 (str.len T4_4))(= 0 (str.len T0_4))(= T1_4 (str.++ T2_4 T3_4))(= T2_4 (str.++ T4_4 T5_4))(= T5_4 "__utmb=169413169")(not (str.in.re T4_4 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "b") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9"))))) - (and (= PCTEMP_LHS_2 (- 1))(= var_0xINPUT_12454 (str.++ T0_4 T1_4))(= 0 (str.len T0_4))(not (str.in.re T1_4 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "b") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9"))))))) -(assert (= T_SELECT_3 (not (= PCTEMP_LHS_3 (- 1))))) -(assert (ite T_SELECT_3 - (and (= PCTEMP_LHS_3 (+ I0_6 0))(= var_0xINPUT_12454 (str.++ T0_6 T1_6))(= I0_6 (str.len T4_6))(= 0 (str.len T0_6))(= T1_6 (str.++ T2_6 T3_6))(= T2_6 (str.++ T4_6 T5_6))(= T5_6 "__utmc=169413169")(not (str.in.re T4_6 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "c") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9"))))) - (and (= PCTEMP_LHS_3 (- 1))(= var_0xINPUT_12454 (str.++ T0_6 T1_6))(= 0 (str.len T0_6))(not (str.in.re T1_6 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "c") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9"))))))) -(assert (= T_4 (<= 0 PCTEMP_LHS_1))) -(assert T_4) -(assert (= T_5 (<= 0 PCTEMP_LHS_2))) -(assert T_5) -(assert (= T_6 (<= 0 PCTEMP_LHS_3))) -(assert T_6) -(assert (= T_7 (= "" var_0xINPUT_12454))) -(assert (= T_8 (not T_7))) -(assert T_8) -(assert (= T_9 (= var_0xINPUT_12454 ""))) -(assert (= T_a (not T_9))) -(assert T_a) -(assert (= T_SELECT_4 (not (= PCTEMP_LHS_4 (- 1))))) -(assert (ite T_SELECT_4 - (and (= PCTEMP_LHS_4 (+ I0_15 0))(= var_0xINPUT_12454 (str.++ T0_15 T1_15))(= I0_15 (str.len T4_15))(= 0 (str.len T0_15))(= T1_15 (str.++ T2_15 T3_15))(= T2_15 (str.++ T4_15 T5_15))(= T5_15 "__utmb=169413169")(not (str.in.re T4_15 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "b") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9"))))) - (and (= PCTEMP_LHS_4 (- 1))(= var_0xINPUT_12454 (str.++ T0_15 T1_15))(= 0 (str.len T0_15))(not (str.in.re T1_15 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "b") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9"))))))) -(assert (= T_c (< (- 1) PCTEMP_LHS_4))) -(assert T_c) -(assert (= T_SELECT_5 (not (= PCTEMP_LHS_5 (- 1))))) -(assert (ite T_SELECT_5 - (and (= PCTEMP_LHS_5 (+ I0_18 PCTEMP_LHS_4))(= var_0xINPUT_12454 (str.++ T0_18 T1_18))(= I0_18 (str.len T4_18))(= PCTEMP_LHS_4 (str.len T0_18))(= T1_18 (str.++ T2_18 T3_18))(= T2_18 (str.++ T4_18 T5_18))(= T5_18 ";")(not (str.in.re T4_18 (str.to.re ";")))) - (and (= PCTEMP_LHS_5 (- 1))(= var_0xINPUT_12454 (str.++ T0_18 T1_18))(= PCTEMP_LHS_4 (str.len T0_18))(not (str.in.re T1_18 (str.to.re ";")))))) -(assert (= T_e (< PCTEMP_LHS_5 0))) -(assert T_e) - -(check-sat) diff --git a/test/regress/regress0/strings/loop002.smt2 b/test/regress/regress0/strings/loop002.smt2 deleted file mode 100644 index 90492189f..000000000 --- a/test/regress/regress0/strings/loop002.smt2 +++ /dev/null @@ -1,10 +0,0 @@ -(set-logic QF_S) -(set-info :status sat) - -(declare-fun x () String) -(declare-fun y () String) -(declare-fun z () String) - -(assert (= (str.++ x "ba") (str.++ "ab" x))) - -(check-sat) diff --git a/test/regress/regress0/strings/loop003.smt2 b/test/regress/regress0/strings/loop003.smt2 deleted file mode 100644 index 1247170c9..000000000 --- a/test/regress/regress0/strings/loop003.smt2 +++ /dev/null @@ -1,13 +0,0 @@ -(set-logic QF_S) -(set-info :status sat) - -(declare-fun x () String) -(declare-fun y () String) -(declare-fun z () String) -(declare-fun w () String) -(declare-fun w1 () String) -(declare-fun w2 () String) - -(assert (= (str.++ x "aaaae") (str.++ "eaaaa" x))) - -(check-sat) diff --git a/test/regress/regress0/strings/loop004.smt2 b/test/regress/regress0/strings/loop004.smt2 deleted file mode 100644 index 8d2ff8096..000000000 --- a/test/regress/regress0/strings/loop004.smt2 +++ /dev/null @@ -1,13 +0,0 @@ -(set-logic QF_S) -(set-info :status sat) - -(declare-fun x () String) -(declare-fun y () String) -(declare-fun z () String) -(declare-fun w () String) -(declare-fun w1 () String) -(declare-fun w2 () String) - -(assert (= (str.++ x y z) (str.++ y z x))) - -(check-sat) diff --git a/test/regress/regress0/strings/loop005.smt2 b/test/regress/regress0/strings/loop005.smt2 deleted file mode 100644 index 039409ea6..000000000 --- a/test/regress/regress0/strings/loop005.smt2 +++ /dev/null @@ -1,18 +0,0 @@ -(set-logic QF_S) -(set-info :status sat) - -(declare-fun x () String) -(declare-fun y () String) -(declare-fun z () String) -(declare-fun w () String) - -;(assert (= (str.++ x y z) (str.++ x z y))) -;(assert (= (str.++ x w z) (str.++ x z w))) - -(assert (= (str.++ y z) (str.++ z y))) -(assert (= (str.++ w z) (str.++ z w))) - -(assert (not (= y w))) -(assert (> (str.len z) 0)) - -(check-sat) diff --git a/test/regress/regress0/strings/loop006.smt2 b/test/regress/regress0/strings/loop006.smt2 deleted file mode 100644 index 288a5f60c..000000000 --- a/test/regress/regress0/strings/loop006.smt2 +++ /dev/null @@ -1,15 +0,0 @@ -(set-logic QF_S) -(set-info :status sat) - -(declare-fun x () String) -(declare-fun y () String) -(declare-fun z () String) -(declare-fun w () String) -(declare-fun w1 () String) -(declare-fun w2 () String) - -;(assert (= (str.++ x y) (str.++ y x))) - -(assert (not (= (str.++ x y) (str.++ y x)))) - -(check-sat) diff --git a/test/regress/regress0/strings/loop007.smt2 b/test/regress/regress0/strings/loop007.smt2 deleted file mode 100644 index a97d97d54..000000000 --- a/test/regress/regress0/strings/loop007.smt2 +++ /dev/null @@ -1,12 +0,0 @@ -(set-logic QF_S) -(set-option :strings-exp true) -(set-info :status sat) - -(declare-fun x () String) -(declare-fun y () String) - -(assert (= (str.++ x y "aa") (str.++ "aa" y x))) -(assert (= (str.len x) (* 2 (str.len y)))) -(assert (> (str.len x) 0)) - -(check-sat) diff --git a/test/regress/regress0/strings/loop008.smt2 b/test/regress/regress0/strings/loop008.smt2 deleted file mode 100644 index f84ba442b..000000000 --- a/test/regress/regress0/strings/loop008.smt2 +++ /dev/null @@ -1,10 +0,0 @@ -(set-logic QF_S) -(set-option :strings-exp true) -(set-info :status sat) - -(declare-fun x () String) - -(assert (= (str.++ x "ab") (str.++ "ba" x))) -(assert (> (str.len x) 5)) - -(check-sat) diff --git a/test/regress/regress0/strings/loop009.smt2 b/test/regress/regress0/strings/loop009.smt2 deleted file mode 100644 index 30fc6cebc..000000000 --- a/test/regress/regress0/strings/loop009.smt2 +++ /dev/null @@ -1,10 +0,0 @@ -(set-logic QF_S) -(set-option :strings-exp true) -(set-info :status sat) - -(declare-fun x () String) - -(assert (= (str.++ x "aa") (str.++ "aa" x))) -(assert (= (str.len x) 7)) - -(check-sat) diff --git a/test/regress/regress0/strings/nf-ff-contains-abs.smt2 b/test/regress/regress0/strings/nf-ff-contains-abs.smt2 deleted file mode 100644 index eb6792666..000000000 --- a/test/regress/regress0/strings/nf-ff-contains-abs.smt2 +++ /dev/null @@ -1,15 +0,0 @@ -(set-logic QF_S) -(set-info :status unsat) -(declare-fun a () String) -(declare-fun b () String) -(declare-fun c () String) -(declare-fun d () String) -(declare-fun e () String) -(declare-fun f () String) -(declare-fun g () String) -(assert (= (str.++ "abc" a "def" b "gg" c) (str.++ e g f))) -(assert (or (= a "a") (= a "aaa"))) -(assert (or (= b "b") (= b "bbb"))) -(assert (or (= c "c") (= c "ccc"))) -(assert (or (= g (str.++ ";" d)) (= g (str.++ d ";")))) -(check-sat) diff --git a/test/regress/regress0/strings/norn-360.smt2 b/test/regress/regress0/strings/norn-360.smt2 deleted file mode 100644 index 573dcbe01..000000000 --- a/test/regress/regress0/strings/norn-360.smt2 +++ /dev/null @@ -1,25 +0,0 @@ -(set-logic QF_SLIA) -(set-option :strings-exp true) -(set-info :status sat) - -(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 (str.++ var_3 "z" var_4 ) (re.++ (re.* (re.union (re.union (str.to.re "z") (str.to.re "b")) (re.++ (str.to.re "a") (re.union (re.union (str.to.re "z") (str.to.re "b")) (str.to.re "a"))))) (str.to.re "a")))) -(assert (str.in.re (str.++ var_3 "z" var_4 ) (re.++ (re.* (re.union (re.union (str.to.re "z") (str.to.re "b")) (re.++ (str.to.re "a") (re.union (str.to.re "z") (str.to.re "a"))))) (str.to.re "a")))) -(assert (str.in.re (str.++ var_3 "z" var_4 ) (re.++ (re.* (re.union (str.to.re "z") (re.++ (re.union (str.to.re "b") (str.to.re "a")) (re.union (str.to.re "z") (str.to.re "b"))))) (re.union (str.to.re "b") (str.to.re "a"))))) -(assert (str.in.re var_4 (re.* (re.range "a" "u")))) -(assert (str.in.re var_3 (re.* (re.range "a" "u")))) -(assert (<= 0 (str.len var_4))) -(check-sat)
\ No newline at end of file diff --git a/test/regress/regress0/strings/norn-ab.smt2 b/test/regress/regress0/strings/norn-ab.smt2 deleted file mode 100644 index 48d889847..000000000 --- a/test/regress/regress0/strings/norn-ab.smt2 +++ /dev/null @@ -1,25 +0,0 @@ -(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 diff --git a/test/regress/regress0/strings/norn-dis-0707-3.smt2 b/test/regress/regress0/strings/norn-dis-0707-3.smt2 deleted file mode 100644 index bc0f877ad..000000000 --- a/test/regress/regress0/strings/norn-dis-0707-3.smt2 +++ /dev/null @@ -1,26 +0,0 @@ -(set-logic QF_S) -(set-info :status sat) -(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 (str.++ var_8 "z" var_9 ) (re.++ (re.* (re.union (str.to.re "a") (re.++ (str.to.re "b") (re.++ (re.* (re.union (str.to.re "b") (str.to.re "a"))) (str.to.re "z"))))) (re.++ (str.to.re "b") (re.* (re.union (str.to.re "b") (str.to.re "a"))))))) -(assert (str.in.re (str.++ var_8 "z" var_9 ) (re.++ (re.* (re.union (re.union (str.to.re "z") (str.to.re "a")) (re.++ (str.to.re "b") (re.++ (re.* (str.to.re "b")) (re.union (str.to.re "z") (str.to.re "a")))))) (re.++ (str.to.re "b") (re.* (str.to.re "b")))))) -(assert (str.in.re (str.++ var_8 "z" var_9 ) (re.++ (re.* (re.union (str.to.re "a") (re.++ (str.to.re "b") (re.++ (re.* (re.union (str.to.re "z") (str.to.re "a"))) (str.to.re "b"))))) (re.++ (str.to.re "b") (re.* (re.union (str.to.re "z") (str.to.re "a"))))))) -(assert (str.in.re (str.++ var_8 "z" var_9 ) (re.* (re.++ (re.union (str.to.re "b") (str.to.re "a")) (re.++ (re.* (str.to.re "a")) (re.union (str.to.re "z") (str.to.re "b"))))))) -(assert (str.in.re var_9 (re.* (re.range "a" "u")))) -(assert (str.in.re var_8 (re.* (re.range "a" "u")))) -(assert (not (str.in.re (str.++ "b" var_8 "z" "b" var_9 ) (re.++ (re.* (re.++ (str.to.re "b") (str.to.re "z"))) (str.to.re "b"))))) -(check-sat) diff --git a/test/regress/regress0/strings/norn-nel-bug-052116.smt2 b/test/regress/regress0/strings/norn-nel-bug-052116.smt2 deleted file mode 100644 index f0c2534a1..000000000 --- a/test/regress/regress0/strings/norn-nel-bug-052116.smt2 +++ /dev/null @@ -1,23 +0,0 @@ -(set-logic QF_S) -(set-info :status sat) -(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.* (re.range "a" "u")))) -(assert (str.in.re var_4 (re.++ (re.* (re.union (str.to.re "a") (re.++ (str.to.re "b") (str.to.re "a")))) (str.to.re "b")))) -(assert (str.in.re (str.++ "a" var_4 "b" ) (re.* (re.range "a" "u")))) -(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"))))))) -(check-sat) diff --git a/test/regress/regress0/strings/norn-simp-rew-sat.smt2 b/test/regress/regress0/strings/norn-simp-rew-sat.smt2 deleted file mode 100644 index 01a102bf9..000000000 --- a/test/regress/regress0/strings/norn-simp-rew-sat.smt2 +++ /dev/null @@ -1,25 +0,0 @@ -(set-logic QF_SLIA) -(set-option :strings-exp true) -(set-info :status sat) - -(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 (str.++ var_3 "z" var_4 ) (re.++ (re.* (re.union (re.union (str.to.re "z") (str.to.re "a")) (re.++ (str.to.re "b") (re.++ (re.* (str.to.re "b")) (re.union (str.to.re "z") (str.to.re "a")))))) (re.++ (str.to.re "b") (re.* (str.to.re "b")))))) -(assert (str.in.re var_4 (re.* (re.range "a" "u")))) -(assert (str.in.re var_4 (re.* (str.to.re "b")))) -(assert (str.in.re var_3 (re.* (re.range "a" "u")))) -(assert (str.in.re var_3 (re.* (str.to.re "a")))) -(assert (<= 0 (str.len var_4))) -(check-sat)
\ No newline at end of file diff --git a/test/regress/regress0/strings/pierre150331.smt2 b/test/regress/regress0/strings/pierre150331.smt2 deleted file mode 100644 index 88d5ec10c..000000000 --- a/test/regress/regress0/strings/pierre150331.smt2 +++ /dev/null @@ -1,13 +0,0 @@ -(set-logic SLIA)
-(set-info :status sat)
-(set-info :smt-lib-version 2.5)
-(set-option :strings-exp true)
-(define-fun stringEval ((?s String)) Bool (str.in.re ?s
-(re.union
-(str.to.re "H")
-(re.++ (re.loop (str.to.re "{") 2 2 ) (re.loop (re.union re.nostr (re.range " " "]") (re.range "" "^") ) 2 4 ) ) ) ) )
-(declare-fun s0() String)
-(declare-fun s1() String)
-(declare-fun s2() String)
-(assert (and true (stringEval s0) (stringEval s1) (distinct s0 s1) (stringEval s2) (distinct s0 s2) (distinct s1 s2) ) )
-(check-sat)
\ No newline at end of file diff --git a/test/regress/regress0/strings/regexp001.smt2 b/test/regress/regress0/strings/regexp001.smt2 deleted file mode 100644 index 62c142d1d..000000000 --- a/test/regress/regress0/strings/regexp001.smt2 +++ /dev/null @@ -1,13 +0,0 @@ -(set-logic QF_S) -(set-info :status sat) -(set-option :strings-exp true) - -(declare-fun x () String) - -(assert (str.in.re x - (re.* (re.++ (re.* (str.to.re "a") ) (str.to.re "b") )) - )) - -(assert (= (str.len x) 3)) - -(check-sat) diff --git a/test/regress/regress0/strings/regexp002.smt2 b/test/regress/regress0/strings/regexp002.smt2 deleted file mode 100644 index a8bd2187a..000000000 --- a/test/regress/regress0/strings/regexp002.smt2 +++ /dev/null @@ -1,24 +0,0 @@ -(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) - -(assert (str.in.re x - (re.* (re.++ (re.* (str.to.re "a") ) (str.to.re "b") )) - )) - -(assert (str.in.re y - (re.* (re.++ (re.* (str.to.re "a") ) (str.to.re "b") )) - )) - -(assert (not (= x y))) -(assert (= (str.len x) (str.len y))) -(assert (= (str.len y) 3)) - -(check-sat) diff --git a/test/regress/regress0/strings/regexp003.smt2 b/test/regress/regress0/strings/regexp003.smt2 deleted file mode 100644 index 7696838fe..000000000 --- a/test/regress/regress0/strings/regexp003.smt2 +++ /dev/null @@ -1,13 +0,0 @@ -(set-logic QF_S) -(set-info :status sat) -(set-option :strings-exp true) - -(declare-const s String) - -(assert (str.in.re s (re.inter - (re.++ (str.to.re "a") (re.* (str.to.re "b")) - (re.inter (str.to.re "c") (re.* (str.to.re "c")))) - (re.++ (str.to.re "a") (re.* (str.to.re "b")) (re.* (str.to.re "c"))) - ))) - -(check-sat) diff --git a/test/regress/regress0/strings/reloop.smt2 b/test/regress/regress0/strings/reloop.smt2 deleted file mode 100644 index 9915504ae..000000000 --- a/test/regress/regress0/strings/reloop.smt2 +++ /dev/null @@ -1,18 +0,0 @@ -(set-logic QF_S) -(set-option :strings-exp true) -(set-info :status sat) - -(declare-fun x () String) -(declare-fun y () String) -(declare-fun z () String) -(declare-fun w () String) - -(assert (str.in.re x (re.loop (str.to.re "a") 5))) -(assert (str.in.re y (re.loop (str.to.re "b") 2 5))) -(assert (str.in.re z (re.loop (str.to.re "c") 5))) -(assert (> (str.len z) 7)) -(assert (str.in.re w (re.loop (str.to.re "b") 2 7))) -(assert (> (str.len w) 2)) -(assert (< (str.len w) 5)) - -(check-sat) diff --git a/test/regress/regress0/strings/repl-empty-sem.smt2 b/test/regress/regress0/strings/repl-empty-sem.smt2 deleted file mode 100644 index 61f70bc23..000000000 --- a/test/regress/regress0/strings/repl-empty-sem.smt2 +++ /dev/null @@ -1,11 +0,0 @@ -; COMMAND-LINE: --strings-exp -; EXPECT: unsat -(set-logic ALL) -(set-info :status unsat) -(declare-fun x () String) -(declare-fun z () String) -(assert (= (str.len z) 0)) -(assert (= (str.replace "ab" z "c") x)) -(declare-fun y () String) -(assert (= x (str.++ "c" y))) -(check-sat) diff --git a/test/regress/regress0/strings/repl-soundness-sem.smt2 b/test/regress/regress0/strings/repl-soundness-sem.smt2 deleted file mode 100644 index d56d7945f..000000000 --- a/test/regress/regress0/strings/repl-soundness-sem.smt2 +++ /dev/null @@ -1,12 +0,0 @@ -; COMMAND-LINE: --strings-exp -; EXPECT: sat -(set-logic ALL) -(set-info :status sat) -(declare-fun x () String) -(declare-fun y () String) -(assert (and -(= (str.replace x x "abc") "") -(= (str.replace (str.++ x y) x "abc") (str.++ x y)) -(= (str.replace (str.++ x y) (str.substr x 0 2) "abc") y) -)) -(check-sat) diff --git a/test/regress/regress0/strings/str001.smt2 b/test/regress/regress0/strings/str001.smt2 deleted file mode 100644 index bb2b701d8..000000000 --- a/test/regress/regress0/strings/str001.smt2 +++ /dev/null @@ -1,16 +0,0 @@ -(set-logic QF_S) -(set-info :status unsat) - -(declare-fun xx () String) -(declare-fun yy () String) -(declare-fun zz () String) -(declare-fun ww () String) -(declare-fun pp () String) -(declare-fun qq () String) - -(assert (= (str.++ xx yy zz) (str.++ ww qq))) -(assert (= ww (str.++ xx pp))) -(assert (= yy pp)) -(assert (not (= zz qq))) - -(check-sat) diff --git a/test/regress/regress0/strings/str002.smt2 b/test/regress/regress0/strings/str002.smt2 deleted file mode 100644 index 62512ef79..000000000 --- a/test/regress/regress0/strings/str002.smt2 +++ /dev/null @@ -1,18 +0,0 @@ -(set-logic QF_S) -(set-info :status unsat) - -(declare-fun xx () String) -(declare-fun yy () String) -(declare-fun zz () String) -(declare-fun ww () String) -(declare-fun pp () String) -(declare-fun qq () String) - -; assoc -(assert (or (= xx (str.++ yy "aa")) (= zz (str.++ yy "aa")) -)) -(assert (and (not (= (str.++ xx "bb") (str.++ yy "aa" "bb"))) - (not (= (str.++ zz "bb") (str.++ yy "aa" "bb"))) -)) - -(check-sat) diff --git a/test/regress/regress0/strings/str006.smt2 b/test/regress/regress0/strings/str006.smt2 deleted file mode 100644 index 2bdf9b1b5..000000000 --- a/test/regress/regress0/strings/str006.smt2 +++ /dev/null @@ -1,14 +0,0 @@ -(set-logic QF_S) -(set-info :status sat) - -(declare-fun x () String) -(declare-fun y () String) -(declare-fun z () String) - -;plandowski p469 1 -(assert (= (str.++ x "ab" y) (str.++ y "ba" z))) -(assert (= z (str.++ x y))) -(assert (not (= (str.++ x "a") (str.++ "a" x)))) - -(check-sat) - diff --git a/test/regress/regress0/strings/str007.smt2 b/test/regress/regress0/strings/str007.smt2 deleted file mode 100644 index a7173701a..000000000 --- a/test/regress/regress0/strings/str007.smt2 +++ /dev/null @@ -1,13 +0,0 @@ -(set-logic QF_S) -(set-info :status unsat) - -(declare-fun x () String) -(declare-fun y () String) - - -(assert (or (= x y) (= x y))) - -(assert (= (str.++ x "ba") (str.++ "ab" x))) -(assert (= (str.++ y "ab") (str.++ "ab" y))) - -(check-sat) diff --git a/test/regress/regress0/strings/strings-index-empty.smt2 b/test/regress/regress0/strings/strings-index-empty.smt2 deleted file mode 100644 index a726d9cab..000000000 --- a/test/regress/regress0/strings/strings-index-empty.smt2 +++ /dev/null @@ -1,11 +0,0 @@ -; COMMAND-LINE: --simplification=none --strings-exp --no-strings-lazy-pp -; EXPECT: sat -(set-logic SLIA) -(set-info :status sat) -(declare-fun x () String) -(declare-fun f () String) -(declare-fun y () Int) -(assert (= (str.len f) 0)) -; command line options ensure reduction is invoked for indexof, f is "", should return -1 -(assert (= (str.indexof x f 4) y)) -(check-sat) diff --git a/test/regress/regress0/strings/strip-endpt-sound.smt2 b/test/regress/regress0/strings/strip-endpt-sound.smt2 deleted file mode 100644 index 0c1dd123c..000000000 --- a/test/regress/regress0/strings/strip-endpt-sound.smt2 +++ /dev/null @@ -1,29 +0,0 @@ -; COMMAND-LINE: --strings-exp -; EXPECT: sat -(set-logic QF_S) -(declare-fun x () String) -(declare-fun y () String) - -(assert (str.contains "c(ab)" (str.++ x ")"))) -(assert (str.contains "c(ab)" (str.++ "c(" y))) - -(declare-fun z () String) -(declare-fun w () String) - -(assert (str.contains "c(ab))" (str.++ z "))"))) -(assert (str.contains z "b")) - -(assert (str.contains "c(ab))" (str.++ w "b)"))) -(assert (str.contains w "a")) - - -(declare-fun p () String) -(declare-fun q () String) - -(assert (str.contains "c(aab))" (str.++ "a" p))) -(assert (str.contains p "a")) - -(assert (str.contains "c(abb))" (str.++ q "b"))) -(assert (str.contains q "b")) - -(check-sat) diff --git a/test/regress/regress0/strings/substr001.smt2 b/test/regress/regress0/strings/substr001.smt2 deleted file mode 100644 index 78f3ffee7..000000000 --- a/test/regress/regress0/strings/substr001.smt2 +++ /dev/null @@ -1,16 +0,0 @@ -(set-logic QF_S) -(set-info :status sat) - -(declare-fun x () String) -(declare-fun i1 () Int) -(declare-fun i2 () Int) -(declare-fun i3 () Int) -(declare-fun i4 () Int) - -(assert (and (>= i1 0) (>= i2 0) (< (+ i1 i2) (str.len x)))) -(assert (and (>= i3 0) (>= i4 0) (< (+ i3 i4) (str.len x)))) -(assert (= "efg" (str.substr x i1 i2) ) ) -(assert (= "bef" (str.substr x i3 i4) ) ) -(assert (> (str.len x) 5)) - -(check-sat) diff --git a/test/regress/regress0/strings/type002.smt2 b/test/regress/regress0/strings/type002.smt2 deleted file mode 100644 index 0df0f20b0..000000000 --- a/test/regress/regress0/strings/type002.smt2 +++ /dev/null @@ -1,18 +0,0 @@ -(set-logic QF_S) -(set-info :status sat) -(set-option :strings-exp true) - -(declare-fun x () String) -(declare-fun y () String) -(declare-fun z () String) -(declare-fun i () Int) - -(assert (>= i 420)) -(assert (= x (int.to.str i))) -(assert (= x (str.++ y "0" z))) -(assert (not (= y ""))) -(assert (not (= z ""))) - - - -(check-sat) diff --git a/test/regress/regress0/strings/type003.smt2 b/test/regress/regress0/strings/type003.smt2 deleted file mode 100644 index c2d4792cc..000000000 --- a/test/regress/regress0/strings/type003.smt2 +++ /dev/null @@ -1,12 +0,0 @@ -(set-logic QF_S) -(set-info :status sat) -(set-option :strings-exp true) - -(declare-fun i () Int) -(declare-fun s () String) - -(assert (< 67 (str.to.int s))) -(assert (= (str.len s) 2)) -(assert (not (= s "68"))) - -(check-sat) diff --git a/test/regress/regress0/strings/username_checker_min.smt2 b/test/regress/regress0/strings/username_checker_min.smt2 deleted file mode 100644 index 2f1c35844..000000000 --- a/test/regress/regress0/strings/username_checker_min.smt2 +++ /dev/null @@ -1,14 +0,0 @@ -(set-logic QF_S) -(set-option :strings-exp true) -(set-info :status unsat) - -(declare-const buff String) -(declare-const pass_mem String) -(assert (= (str.len buff) 4)) -(assert (= (str.len pass_mem) 1)) - -(assert (str.in.re (str.++ buff pass_mem) (re.+ (str.to.re "A")))) - -(assert (str.contains buff "<")) - -(check-sat) |