blob: 7c9de4c49cb47a0d1150b4605b0ef7fcb3be6bae (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
|
; COMMAND-LINE: --finite-model-find -q --decision=justification-old
; EXPECT: sat
(set-logic HO_ALL)
(declare-sort $$unsorted 0)
(declare-sort qML_mu 0)
(declare-sort qML_i 0)
(declare-fun scott_G (qML_mu qML_i) Bool)
(declare-fun scott_P ((-> qML_mu qML_i Bool) qML_i) Bool)
(assert
(=
scott_G
(lambda ((X qML_mu) (__flatten_var_0 qML_i))
(forall ((BOUND_VARIABLE_292 (-> qML_mu qML_i Bool)))
(or
(not (scott_P BOUND_VARIABLE_292 __flatten_var_0))
(BOUND_VARIABLE_292 X __flatten_var_0)
) ))))
(assert
(forall ((X_1 qML_i))
(scott_P
(lambda ((X qML_mu) (__flatten_var_0 qML_i))
(forall ((BOUND_VARIABLE_292 (-> qML_mu qML_i Bool)))
(or
(not (scott_P BOUND_VARIABLE_292 __flatten_var_0))
(BOUND_VARIABLE_292 X __flatten_var_0)) ))
X_1
)
))
(check-sat)
|
