blob: 375acc035b33f466c94ea081be9a47382450c728 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
(set-logic UFLIA)
(set-info :status unsat)
(declare-fun P (Int) Bool)
(declare-fun Q (Int) Bool)
(declare-fun R (Int) Bool)
(assert (forall ((x Int)) (=> (Q x) (R x))))
(assert (forall ((x Int)) (=> (P x) (not (R x)))))
(declare-fun f (Int) Int)
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(assert (or (= a b) (= a c)))
(assert (P (f a)))
(assert (Q (f b)))
(assert (Q (f c)))
(check-sat)
|
