test/regress/regress1/fmf/german73.smt2


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
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105

; COMMAND-LINE: --finite-model-find
; EXPECT: unsat
(set-logic ALL_SUPPORTED)
(set-info :status unsat)
(declare-datatypes ((UNIT 0)) (((Unit))))
(declare-datatypes ((BOOL 0)) (((Truth) (Falsity))))

; Decls     --------------
(declare-sort node$type 0)
(declare-sort data$type 0)
(declare-datatypes ((cache_state$type 0)) (((invalid) (shared) (exclusive))))
(declare-datatypes ((cache$type 0)) (((c_cache$type (c_state cache_state$type) (c_data data$type)))))
(declare-datatypes ((msg_cmd$type 0)) (((empty) (reqs) (reqe) (inv) (invack) (gnts) (gnte))))
(declare-datatypes ((msg$type 0)) (((c_msg$type (m_cmd msg_cmd$type) (m_data data$type)))))
(declare-fun dummy () data$type)

; Var Decls --------------
(declare-fun memdata$1 () data$type)
(declare-fun shrset$1 () (Array node$type BOOL))
(declare-fun recv_invack$i () node$type)
(declare-fun exgntd () BOOL)
(declare-fun invset () (Array node$type BOOL))
(declare-fun chan3$1 () (Array node$type msg$type))
(declare-fun shrset () (Array node$type BOOL))
(declare-fun exgntd$1 () BOOL)
(declare-fun chan2 () (Array node$type msg$type))
(declare-fun chan3 () (Array node$type msg$type))
(declare-fun curcmd () msg_cmd$type)

; Asserts   --------------
(assert (not (=> (and (forall ((n node$type))
                                                 (=> (= (select invset n)
                                                     Truth) (= (select
                                                               shrset
                                                               n) Truth)))
                                            (forall ((n node$type)) (=>
                                                                    (or
                                                                    (=
                                                                    (m_cmd
                                                                    (select
                                                                    chan2
                                                                    n))
                                                                    inv)
                                                                    (=
                                                                    (m_cmd
                                                                    (select
                                                                    chan3
                                                                    n))
                                                                    invack))
                                                                    (not
                                                                    (=
                                                                    (select
                                                                    invset
                                                                    n)
                                                                    Truth)))))
                                        (=> (= (m_cmd (select chan3 recv_invack$i))
                                            invack) (=> (not (= curcmd empty))
                                                    (=> (= chan3$1 (store
                                                                   chan3
                                                                   recv_invack$i
                                                                   (let (
                                                                   (vup_101
                                                                   (select
                                                                   chan3
                                                                   recv_invack$i)))
                                                                   (c_msg$type
                                                                   empty
                                                                   (m_data
                                                                   vup_101)))))
                                                    (=> (= shrset$1 (store
                                                                    shrset
                                                                    recv_invack$i
                                                                    Falsity))
                                                    (= (ite (= exgntd Truth)
                                                       (ite (=> (= exgntd$1
                                                                Falsity)
                                                            (=> (= memdata$1
                                                                (m_data
                                                                (select
                                                                chan3$1
                                                                recv_invack$i)))
                                                            (forall (
                                                                    (n node$type))
                                                            (=> (= (select
                                                                   invset
                                                                   n)
                                                                Truth)
                                                            (= (select
                                                               shrset$1
                                                               n) Truth)))))
                                                       Truth Falsity)
                                                       (ite (forall (
                                                                    (n node$type))
                                                            (=> (= (select
                                                                   invset
                                                                   n)
                                                                Truth)
                                                            (= (select
                                                               shrset$1
                                                               n) Truth)))
                                                       Truth Falsity))
                                                    Truth))))))))

(check-sat)
(exit)