test/regress/regress1/fmf/german169.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

; COMMAND-LINE: --finite-model-find
; EXPECT: sat
(set-logic ALL_SUPPORTED)
(set-info :status sat)
(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 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 auxnode () node$type)
(declare-fun curcmd () msg_cmd$type)

; Asserts   --------------
(assert (not (=> (and (and (forall ((n node$type))
                                                      (=> (= (m_cmd (select
                                                                    chan2
                                                                    n))
                                                          gnte) (= exgntd
                                                                Truth)))
                                                 (forall ((n node$type))
                                                 (=> (= exgntd Truth)
                                                 (= (select shrset n)
                                                 (ite (= n auxnode) Truth
                                                 Falsity))))) (forall
                                                              ((n node$type))
                                                              (=> (=
                                                                  (m_cmd
                                                                  (select
                                                                  chan3
                                                                  n))
                                                                  invack)
                                                              (= (m_cmd
                                                                 (select
                                                                 chan2
                                                                 n))
                                                              empty))))
                                        (=> (= (m_cmd (select chan3 recv_invack$i))
                                            invack) (=> (not (= curcmd empty))
                                                    (=> (= chan3$1 (store
                                                                   chan3
                                                                   recv_invack$i
                                                                   (let (
                                                                   (vup_228
                                                                   (select
                                                                   chan3
                                                                   recv_invack$i)))
                                                                   (c_msg$type
                                                                   empty
                                                                   (m_data
                                                                   vup_228)))))
                                                    (=> (= 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))
                                                            (=> (= (m_cmd
                                                                   (select
                                                                   chan2
                                                                   n))
                                                                gnte)
                                                            (= exgntd$1
                                                            Truth)))))
                                                       Truth Falsity)
                                                       (ite (forall (
                                                                    (n node$type))
                                                            (=> (= (m_cmd
                                                                   (select
                                                                   chan2
                                                                   n))
                                                                gnte)
                                                            (= exgntd
                                                            Truth)))
                                                       Truth Falsity))
                                                    Truth))))))))

(check-sat)
(exit)