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 --lang=smt2.5
; EXPECT: sat
(set-logic ALL_SUPPORTED)
(set-info :status sat)
(declare-datatypes () ((UNIT (Unit))))
(declare-datatypes () ((BOOL (Truth) (Falsity))))

; Decls     --------------
(declare-sort node$type 0)
(declare-sort data$type 0)
(declare-datatypes () ((cache_state$type (invalid) (shared) (exclusive))))
(declare-datatypes () ((cache$type (c_cache$type (c_state cache_state$type) (c_data data$type)))))
(declare-datatypes () ((msg_cmd$type (empty) (reqs) (reqe) (inv) (invack) (gnts) (gnte))))
(declare-datatypes () ((msg$type (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)