blob: 0485f9a6f04a1a84575ccd907bb06b971adf07dc (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
; COMMAND-LINE: --uf-ho
; EXPECT: unsat
(set-logic UFLIA)
(set-info :status unsat)
(declare-fun f (Int Int Int) Int)
(declare-fun h (Int Int Int) Int)
(declare-fun g (Int Int) Int)
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(assert (or (= (f a) g) (= (h a) g)))
(assert (= (f a b d) c))
(assert (= (h a b d) c))
(assert (forall ((x Int) (y Int)) (not (= (g x y) c))))
(check-sat)
|
