blob: 345d8220e4b591bbaa269e6db71748264b1d61e7 (
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 --lang=smt2.5
; EXPECT: unsat
(set-logic ALL_SUPPORTED)
(set-info :status unsat)
(declare-sort g_ 0)
(declare-fun __nun_card_witness_0_ () g_)
(declare-sort f_ 0)
(declare-fun __nun_card_witness_1_ () f_)
(declare-sort e_ 0)
(declare-fun __nun_card_witness_2_ () e_)
(declare-datatypes ()
((prod1_ (Pair1_ (_select_Pair1__0 e_) (_select_Pair1__1 f_)))))
(declare-sort d_ 0)
(declare-fun __nun_card_witness_3_ () d_)
(declare-sort c_ 0)
(declare-fun __nun_card_witness_4_ () c_)
(declare-sort b_ 0)
(declare-fun __nun_card_witness_5_ () b_)
(declare-sort a_ 0)
(declare-fun __nun_card_witness_6_ () a_)
(declare-datatypes ()
((prod_ (Pair_ (_select_Pair__0 a_) (_select_Pair__1 b_)))))
(declare-fun f1_ (prod_ c_ d_ prod1_) g_)
(declare-fun g1_ (prod_) c_)
(declare-fun h_ (prod_ d_) prod1_)
(declare-fun nun_sk_0_ () prod_)
(declare-fun nun_sk_1_ (c_) d_)
(assert
(not
(exists ((v/72 c_))
(exists ((x/73 prod1_))
(= (f1_ nun_sk_0_ v/72 (nun_sk_1_ v/72) x/73)
(f1_ nun_sk_0_ (g1_ nun_sk_0_) (nun_sk_1_ v/72)
(h_ nun_sk_0_ (nun_sk_1_ v/72))))))))
(check-sat)
|
