diff options
Diffstat (limited to 'test/regress/regress0/uf')
| -rwxr-xr-x | test/regress/regress0/uf/cnf-and-neg.smt2 | 22 | ||||
| -rwxr-xr-x | test/regress/regress0/uf/cnf_abc.smt2 | 336 |
2 files changed, 179 insertions, 179 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) diff --git a/test/regress/regress0/uf/cnf_abc.smt2 b/test/regress/regress0/uf/cnf_abc.smt2 index 5d011f44c..46a4b7dbf 100755 --- a/test/regress/regress0/uf/cnf_abc.smt2 +++ b/test/regress/regress0/uf/cnf_abc.smt2 @@ -1,168 +1,168 @@ -(set-logic QF_UF)
-(set-info :status unsat)
-
-(declare-sort I 0)
-(declare-fun f (I I) I)
-(declare-fun a () I)
-(declare-fun b () I)
-(declare-fun c () I)
-
-
-
-(assert
- (or
- (= (f a a) a)
- (= (f a a) b)
- (= (f a a) c)
- ))
-
-(assert
- (or
- (= (f a b) a)
- (= (f a b) b)
- (= (f a b) c)
- ))
-
-(assert
- (or
- (= (f a c) a)
- (= (f a c) b)
- (= (f a c) c)
- ))
-
-(assert
- (or
- (= (f b a) a)
- (= (f b a) b)
- (= (f b a) c)
- ))
-
-(assert
- (or
- (= (f b b) a)
- (= (f b b) b)
- (= (f b b) c)
- ))
-
-(assert
- (or
- (= (f b c) a)
- (= (f b c) b)
- (= (f b c) c)
- ))
-
-
-(assert
- (or
- (= (f c a) a)
- (= (f c a) b)
- (= (f c a) c)
- ))
-
-(assert
- (or
- (= (f c b) a)
- (= (f c b) b)
- (= (f c b) c)
- ))
-
-(assert
- (or
- (= (f c c) a)
- (= (f c c) b)
- (= (f c c) c)
- ))
-
-
-
-(assert
- (or
- (= (f a a) a)
- (= (f b b) a)
- (= (f c c) a)
- ))
-
-(assert
- (or
- (= (f a a) b)
- (= (f b b) b)
- (= (f c c) b)
- ))
-
-(assert
- (or
- (= (f a a) c)
- (= (f b b) c)
- (= (f c c) c)
- ))
-
-
-
-(assert
- (or
- (= (f a a) a)
- (= (f b a) b)
- (= (f c a) c)
- ))
-
-(assert
- (or
- (= (f a b) a)
- (= (f b b) b)
- (= (f c b) c)
- ))
-
-(assert
- (or
- (= (f a c) a)
- (= (f b c) b)
- (= (f c c) c)
- ))
-
-
-
-
-(assert (not (= (f a a) a)))
-(assert (not (= (f b b) b)))
-(assert (not (= (f c c) c)))
-
-
-(assert
- (or
- (not (= (f a (f a a)) a))
- (not (= (f a (f a b)) b))
- (not (= (f a (f a c)) c))
- ))
-
-(assert
- (or
- (not (= (f b (f b a)) a))
- (not (= (f b (f b b)) b))
- (not (= (f b (f b c)) c))
- ))
-
-(assert
- (or
- (not (= (f c (f c a)) a))
- (not (= (f c (f c b)) b))
- (not (= (f c (f c c)) c))
- ))
-
-
-(assert (not (= (f a a) (f b a))))
-(assert (not (= (f a a) (f c a))))
-(assert (not (= (f b a) (f c a))))
-
-(assert (not (= (f a b) (f b b))))
-(assert (not (= (f a b) (f c b))))
-(assert (not (= (f b b) (f c b))))
-
-(assert (not (= (f a c) (f b c))))
-(assert (not (= (f a c) (f c c))))
-(assert (not (= (f b c) (f c c))))
-
-
-
-(check-sat)
-
-(exit)
+(set-logic QF_UF) +(set-info :status unsat) + +(declare-sort I 0) +(declare-fun f (I I) I) +(declare-fun a () I) +(declare-fun b () I) +(declare-fun c () I) + + + +(assert + (or + (= (f a a) a) + (= (f a a) b) + (= (f a a) c) + )) + +(assert + (or + (= (f a b) a) + (= (f a b) b) + (= (f a b) c) + )) + +(assert + (or + (= (f a c) a) + (= (f a c) b) + (= (f a c) c) + )) + +(assert + (or + (= (f b a) a) + (= (f b a) b) + (= (f b a) c) + )) + +(assert + (or + (= (f b b) a) + (= (f b b) b) + (= (f b b) c) + )) + +(assert + (or + (= (f b c) a) + (= (f b c) b) + (= (f b c) c) + )) + + +(assert + (or + (= (f c a) a) + (= (f c a) b) + (= (f c a) c) + )) + +(assert + (or + (= (f c b) a) + (= (f c b) b) + (= (f c b) c) + )) + +(assert + (or + (= (f c c) a) + (= (f c c) b) + (= (f c c) c) + )) + + + +(assert + (or + (= (f a a) a) + (= (f b b) a) + (= (f c c) a) + )) + +(assert + (or + (= (f a a) b) + (= (f b b) b) + (= (f c c) b) + )) + +(assert + (or + (= (f a a) c) + (= (f b b) c) + (= (f c c) c) + )) + + + +(assert + (or + (= (f a a) a) + (= (f b a) b) + (= (f c a) c) + )) + +(assert + (or + (= (f a b) a) + (= (f b b) b) + (= (f c b) c) + )) + +(assert + (or + (= (f a c) a) + (= (f b c) b) + (= (f c c) c) + )) + + + + +(assert (not (= (f a a) a))) +(assert (not (= (f b b) b))) +(assert (not (= (f c c) c))) + + +(assert + (or + (not (= (f a (f a a)) a)) + (not (= (f a (f a b)) b)) + (not (= (f a (f a c)) c)) + )) + +(assert + (or + (not (= (f b (f b a)) a)) + (not (= (f b (f b b)) b)) + (not (= (f b (f b c)) c)) + )) + +(assert + (or + (not (= (f c (f c a)) a)) + (not (= (f c (f c b)) b)) + (not (= (f c (f c c)) c)) + )) + + +(assert (not (= (f a a) (f b a)))) +(assert (not (= (f a a) (f c a)))) +(assert (not (= (f b a) (f c a)))) + +(assert (not (= (f a b) (f b b)))) +(assert (not (= (f a b) (f c b)))) +(assert (not (= (f b b) (f c b)))) + +(assert (not (= (f a c) (f b c)))) +(assert (not (= (f a c) (f c c)))) +(assert (not (= (f b c) (f c c)))) + + + +(check-sat) + +(exit) |