diff options
author | Tim King <taking@google.com> | 2015-11-05 14:18:03 -0800 |
---|---|---|
committer | Tim King <taking@google.com> | 2015-11-05 14:18:03 -0800 |
commit | 859ae93590062ba7fef5577c6577068f0b74c239 (patch) | |
tree | 81d2d257c28414d10a261c242c1801f3eaadce78 /test/regress/regress0/strings/norn-simp-rew.smt2 | |
parent | b455f5cde8b84b7951d309604b75a76afd8b8bfa (diff) |
Fixes some initialization and desctruction problems in quantifiers. Also restricts the desctructors of some components to not throw exceptions for pickier compiliers. Also changes some formatting of regression scripts.
Diffstat (limited to 'test/regress/regress0/strings/norn-simp-rew.smt2')
-rwxr-xr-x | test/regress/regress0/strings/norn-simp-rew.smt2 | 56 |
1 files changed, 28 insertions, 28 deletions
diff --git a/test/regress/regress0/strings/norn-simp-rew.smt2 b/test/regress/regress0/strings/norn-simp-rew.smt2 index d0cd69cb0..45f7ede94 100755 --- a/test/regress/regress0/strings/norn-simp-rew.smt2 +++ b/test/regress/regress0/strings/norn-simp-rew.smt2 @@ -1,29 +1,29 @@ -(set-logic QF_SLIA)
-(set-option :strings-exp true)
-(set-info :status unsat)
-
-(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_7 "z" var_8 ) (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_7 "z" var_8 ) (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_7 "z" var_8 ) (re.++ (re.* (re.++ (str.to.re "b") (re.++ (re.* (re.union (str.to.re "z") (str.to.re "b"))) (str.to.re "a")))) (re.++ (str.to.re "b") (re.* (re.union (str.to.re "z") (str.to.re "b")))))))
-(assert (str.in.re (str.++ var_7 "z" var_8 ) (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 (str.++ var_7 "z" var_8 ) (re.* (re.++ (str.to.re "b") (re.++ (re.* (str.to.re "z")) (str.to.re "b"))))))
-(assert (str.in.re (str.++ var_7 "z" var_8 ) (re.++ (re.* (re.++ (str.to.re "b") (str.to.re "z"))) (str.to.re "b"))))
-(assert (str.in.re (str.++ "a" var_8 ) (re.* (re.range "a" "u"))))
-(assert (str.in.re var_8 (re.* (re.range "a" "u"))))
-(assert (str.in.re var_7 (re.* (re.range "a" "u"))))
-(assert (not (str.in.re (str.++ "b" var_7 ) (re.* (re.range "a" "u")))))
+(set-logic QF_SLIA) +(set-option :strings-exp true) +(set-info :status unsat) + +(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_7 "z" var_8 ) (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_7 "z" var_8 ) (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_7 "z" var_8 ) (re.++ (re.* (re.++ (str.to.re "b") (re.++ (re.* (re.union (str.to.re "z") (str.to.re "b"))) (str.to.re "a")))) (re.++ (str.to.re "b") (re.* (re.union (str.to.re "z") (str.to.re "b"))))))) +(assert (str.in.re (str.++ var_7 "z" var_8 ) (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 (str.++ var_7 "z" var_8 ) (re.* (re.++ (str.to.re "b") (re.++ (re.* (str.to.re "z")) (str.to.re "b")))))) +(assert (str.in.re (str.++ var_7 "z" var_8 ) (re.++ (re.* (re.++ (str.to.re "b") (str.to.re "z"))) (str.to.re "b")))) +(assert (str.in.re (str.++ "a" var_8 ) (re.* (re.range "a" "u")))) +(assert (str.in.re var_8 (re.* (re.range "a" "u")))) +(assert (str.in.re var_7 (re.* (re.range "a" "u")))) +(assert (not (str.in.re (str.++ "b" var_7 ) (re.* (re.range "a" "u"))))) (check-sat)
\ No newline at end of file |