blob: 47a3bf8b1d53b85f6ec79be4cc08815219cbb319 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
(set-logic QF_UF)
(declare-sort U 0)
(declare-fun a () U)
(declare-fun b () U)
(declare-fun c () U)
(declare-fun f (U U) U)
(assert (not
(=> (and (= a b) (= a c))
(= (f a c) (f b a)))))
(check-sat)
(exit)
|