blob: 61d82d00cc1f00e9396f3f8040d6eedd17956a17 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
; COMMAND-LINE: --uf-ho --finite-model-find
; EXPECT: sat
(set-logic UF)
(set-info :status sat)
(declare-sort U 0)
(declare-fun P (U U) Bool)
(declare-fun Q (U U) Bool)
(declare-fun R (U U) Bool)
(declare-fun a () U)
(declare-fun b () U)
; can solve this using standard MBQI model for P = \ xy true
(assert (forall ((x U) (y U)) (or (P x y) (Q x y))))
(assert (forall ((x U) (y U)) (or (P x y) (R x y))))
(assert (not (= a b)))
(assert (= (Q a) (R b)))
(check-sat)
|
