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/uf/cnf-and-neg.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/uf/cnf-and-neg.smt2')
| -rwxr-xr-x | test/regress/regress0/uf/cnf-and-neg.smt2 | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/test/regress/regress0/uf/cnf-and-neg.smt2 b/test/regress/regress0/uf/cnf-and-neg.smt2 index 711740f67..470a88809 100755 --- a/test/regress/regress0/uf/cnf-and-neg.smt2 +++ b/test/regress/regress0/uf/cnf-and-neg.smt2 @@ -1,11 +1,11 @@ -(set-logic QF_UF)
-(set-info :status unsat)
-(declare-sort I 0)
-(declare-fun a () I)
-(declare-fun b () I)
-(declare-fun c () I)
-(declare-fun f (I) I)
-(assert (not (= (f a) (f b))))
-(assert (not (= (f a) (f c))))
-(assert (not (and (not (= a b)) (not (= a c)))))
-(check-sat)
+(set-logic QF_UF) +(set-info :status unsat) +(declare-sort I 0) +(declare-fun a () I) +(declare-fun b () I) +(declare-fun c () I) +(declare-fun f (I) I) +(assert (not (= (f a) (f b)))) +(assert (not (= (f a) (f c)))) +(assert (not (and (not (= a b)) (not (= a c))))) +(check-sat) |