blob: 225faa1a54213cf5dd28cc302a4182475f0e7021 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
; EXPECT: unsat
(set-logic HO_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)
|