blob: cd3e1137e4344e97aa35af41c5d3ebf6f8ecab39 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
; COMMAND-LINE: --no-check-proofs
; EXPECT: unsat
(set-logic QF_UF)
(set-info :smt-lib-version 2.0)
(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)
|