blob: e3428de179cb59459ff02c141d963159af1c1da1 (
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
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
|
(set-logic BV)
(set-info :status sat)
(declare-fun W_S1_V1 () Bool)
(declare-fun W_S1_V2 () Bool)
(declare-fun W_S1_V4 () Bool)
(declare-fun R_S1_V1 () Bool)
(declare-fun R_E1_V1 () Bool)
(declare-fun R_E1_V3 () Bool)
(declare-fun R_E1_V2 () Bool)
(declare-fun R_E1_V4 () Bool)
(declare-fun DISJ_W_S1_R_E1 () Bool)
(declare-fun R_S1_V3 () Bool)
(declare-fun R_S1_V2 () Bool)
(declare-fun R_S1_V4 () Bool)
(declare-fun DISJ_W_S1_R_S1 () Bool)
(declare-fun W_S1_V3 () Bool)
(assert
(let
(($x324
(forall
((V4_0 (_ BitVec 32)) (V2_0 (_ BitVec 32))
(V3_0 (_ BitVec 32)) (V1_0 (_ BitVec 32))
(MW_S1_V4 Bool) (MW_S1_V2 Bool)
(MW_S1_V3 Bool) (MW_S1_V1 Bool)
(S1_V3_!14 (_ BitVec 32)) (S1_V3_!20 (_ BitVec 32))
(E1_!11 (_ BitVec 32)) (E1_!16 (_ BitVec 32))
(E1_!17 (_ BitVec 32)) (S1_V1_!15 (_ BitVec 32))
(S1_V1_!21 (_ BitVec 32)) (S1_V2_!13 (_ BitVec 32))
(S1_V2_!19 (_ BitVec 32)) (S1_V4_!12 (_ BitVec 32))
(S1_V4_!18 (_ BitVec 32)))
(let
(($x267
(and (= (ite MW_S1_V4 S1_V4_!12 V4_0) (ite MW_S1_V4 S1_V4_!18 V4_0))
(= E1_!16 (ite MW_S1_V1 S1_V1_!21 E1_!17))
(= (ite MW_S1_V3 S1_V3_!14 V3_0) (ite MW_S1_V3 S1_V3_!20 V3_0))
(= (ite MW_S1_V1 S1_V1_!15 E1_!11) (ite MW_S1_V1 S1_V1_!21 E1_!17)))))
(let
(($x297
(and (or (not R_E1_V4) (= (ite MW_S1_V4 S1_V4_!12 V4_0) V4_0))
(or (not R_E1_V2) (= (ite MW_S1_V2 S1_V2_!13 V2_0) V2_0))
(or (not R_E1_V3) (= (ite MW_S1_V3 S1_V3_!14 V3_0) V3_0))
(or (not R_E1_V1) (= (ite MW_S1_V1 S1_V1_!15 E1_!11) V1_0)))))
(let
(($x310
(and (or (not R_E1_V4) (= V4_0 (ite MW_S1_V4 S1_V4_!12 V4_0)))
(or (not R_E1_V2) (= V2_0 (ite MW_S1_V2 S1_V2_!13 V2_0)))
(or (not R_E1_V3) (= V3_0 (ite MW_S1_V3 S1_V3_!14 V3_0)))
(or (not R_E1_V1) (= V1_0 (ite MW_S1_V1 S1_V1_!15 E1_!11))))))
(let
(($x321
(and
(or (not (or (not R_S1_V1) (= E1_!17 E1_!11))) (= S1_V3_!20 S1_V3_!14))
(or (not $x310) (= E1_!11 E1_!16))
(= E1_!11 E1_!17) (or (not $x297) (= E1_!16 E1_!17))
(or (not (or (not R_S1_V1) (= E1_!17 E1_!11))) (= S1_V1_!21 S1_V1_!15))
(or (not (or (not R_S1_V1) (= E1_!17 E1_!11))) (= S1_V2_!19 S1_V2_!13))
(or (not (or (not R_S1_V1) (= E1_!17 E1_!11))) (= S1_V4_!18 S1_V4_!12))
(or (not MW_S1_V4) W_S1_V4)
(or (not MW_S1_V2) W_S1_V2)
(or (not MW_S1_V1) W_S1_V1))))
(or (not $x321) $x267))))))))
(let
(($x40
(or (and W_S1_V4 R_E1_V4)
(and W_S1_V2 R_E1_V2) R_E1_V3
(and W_S1_V1 R_E1_V1))))
(let (($x42 (= DISJ_W_S1_R_E1 (not $x40))))
(let
(($x37
(or (and W_S1_V4 R_S1_V4)
(and W_S1_V2 R_S1_V2) R_S1_V3
(and W_S1_V1 R_S1_V1))))
(let (($x39 (= DISJ_W_S1_R_S1 (not $x37)))) (and W_S1_V3 $x39 $x42 $x324)))))))
(check-sat)
(exit)
|
