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/ilc-l-nt.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/ilc-l-nt.smt2')
-rwxr-xr-x | test/regress/regress0/strings/ilc-l-nt.smt2 | 26 |
1 files changed, 13 insertions, 13 deletions
diff --git a/test/regress/regress0/strings/ilc-l-nt.smt2 b/test/regress/regress0/strings/ilc-l-nt.smt2 index 32dfc0b1b..9e1cc2bc5 100755 --- a/test/regress/regress0/strings/ilc-l-nt.smt2 +++ b/test/regress/regress0/strings/ilc-l-nt.smt2 @@ -1,14 +1,14 @@ -(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)))
-
+(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 |