test/regress/regress0/bt-test-00.smt2


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21

; EXPECT: unsat
(set-logic QF_UF)
(set-info :smt-lib-version 2.6)
(set-info :category "crafted")
(set-info :status unsat)

(declare-fun f (Bool) Bool)
(declare-fun g (Bool) Bool)
(declare-fun h (Bool) Bool)

(declare-fun x () Bool)
(declare-fun y () Bool)
(declare-fun z () Bool)

(assert (not (= (f x) (f y))))
(assert (not (= (g y) (g z))))
(assert (not (= (h z) (h x))))

(check-sat)

(exit)