-
Notifications
You must be signed in to change notification settings - Fork 0
/
test.z3
104 lines (103 loc) · 5.69 KB
/
test.z3
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
(define-fun F () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000000)
(define-fun T () (_ BitVec 256) #x0000000000000000000000000000000000000000000000000000000000000001)
(declare-const v_46 (_ BitVec 256))
(declare-const v_44 (_ BitVec 256))
(declare-const v_45 (_ BitVec 256))
(declare-const v_43 (_ BitVec 256))
(declare-const v_42 (_ BitVec 256))
(declare-const v_41 (_ BitVec 256))
(declare-const v_32 (_ BitVec 256))
(declare-const v_11 (_ BitVec 256))
(declare-const v_10 (_ BitVec 256))
(declare-const v_40 (_ BitVec 256))
(declare-const v_39 (_ BitVec 256))
(declare-const v_38 (_ BitVec 256))
(declare-const v_37 (_ BitVec 256))
(declare-const v_36 (_ BitVec 256))
(declare-const v_31 (_ BitVec 256))
(declare-const v_30 (_ BitVec 256))
(declare-const v_15 (_ BitVec 256))
(declare-const v_35 (_ BitVec 256))
(declare-const v_34 (_ BitVec 256))
(declare-const v_33 (_ BitVec 256))
(declare-const v_5 (_ BitVec 256))
(declare-const v_4 (_ BitVec 256))
(declare-const v_3 (_ BitVec 256))
(declare-const v_2 (_ BitVec 256))
(declare-const v_73 (_ BitVec 256))
(declare-const v_72 (_ BitVec 256))
(declare-const v_71 (_ BitVec 256))
(declare-const v_70 (_ BitVec 256))
(declare-const v_69 (_ BitVec 256))
(declare-const v_68 (_ BitVec 256))
(declare-const v_66 (_ BitVec 256))
(declare-const v_57 (_ BitVec 256))
(declare-const v_56 (_ BitVec 256))
(declare-const v_29 (_ BitVec 256))
(declare-const v_28 (_ BitVec 256))
(declare-const v_27 (_ BitVec 256))
(declare-const v_26 (_ BitVec 256))
(declare-const v_25 (_ BitVec 256))
(declare-const v_24 (_ BitVec 256))
(declare-const v_23 (_ BitVec 256))
(declare-const v_22 (_ BitVec 256))
(declare-const v_21 (_ BitVec 256))
(declare-const v_20 (_ BitVec 256))
(declare-const v_19 (_ BitVec 256))
(declare-const v_18 (_ BitVec 256))
(declare-const v_16 (_ BitVec 256))
(declare-const v_17 (_ BitVec 256))
(assert (= v_17 (bvand #x000000000000000000000000ffffffffffffffffffffffffffffffffffffffff v_15)))
(assert (= v_16 (bvand #x000000000000000000000000ffffffffffffffffffffffffffffffffffffffff v_3)))
(assert (= v_18 (if (= v_17 v_16) T F)))
(assert (= v_19 (if (= v_18 F) T F)))
(assert (= v_20 (if (= v_19 F) T F)))
(assert (= v_21 (if (= v_20 F) T F)))
(assert (= v_22 (if (= v_21 F) T F)))
(assert (= v_23 (if (= v_22 F) T F)))
(assert (= v_24 (bvand #x000000000000000000000000ffffffffffffffffffffffffffffffffffffffff v_15)))
(assert (= v_25 (if (bvugt v_24 #x0000000000000000000000000000000000000000000000000004000000000000) T F)))
(assert (= v_26 (if (= v_25 F) T F)))
(assert (= v_27 (if (= v_26 F) T F)))
(assert (= v_28 (if (= v_27 F) T F)))
(assert (= v_29 (if (= v_28 F) T F)))
(assert (= v_56 (bvand #x000000000000000000000000ffffffffffffffffffffffffffffffffffffffff v_46)))
(assert (= v_57 (bvand #x000000000000000000000000ffffffffffffffffffffffffffffffffffffffff v_56)))
(assert (= v_66 (bvand #x000000000000000000000000ffffffffffffffffffffffffffffffffffffffff v_57)))
(assert (= v_68 (if (= v_66 #x0000000000000000000000000000000000000000000000000000000000000000) T F)))
(assert (= v_69 (if (= v_68 F) T F)))
(assert (= v_70 (if (= v_69 F) T F)))
(assert (= v_71 (if (= v_70 F) T F)))
(assert (= v_72 (if (= v_71 F) T F)))
(assert (= v_73 (if (= v_72 F) T F)))
(assert (= v_3 (bvand #x000000000000000000000000ffffffffffffffffffffffffffffffffffffffff v_2)))
(assert (= v_5 (bvand #x000000000000000000000000ffffffffffffffffffffffffffffffffffffffff v_4)))
(assert (= v_33 (bvshl #x0000000000000000000000000000000000000000000000000000000000000016 v_31)))
(assert (= v_34 (bvand v_33 #x00000000000000000000000000000000000000000000ffffffffffffffffffff)))
(assert (= v_35 (bvor v_34 #x5eb13676dec4ad4737583e64736f6c634300050a003200000000000000000000)))
(assert (= v_30 (bvand #x000000000000000000000000ffffffffffffffffffffffffffffffffffffffff v_15)))
(assert (= v_31 (bvand #x000000000000000000000000ffffffffffffffffffffffffffffffffffffffff v_30)))
(assert (= v_36 (bvshl #x000000000000000000000000000000000000000000000000000000000000000a v_31)))
(assert (= v_37 (bvand v_36 #xffffffffffffffffffffffffffffffffffffffffffff00000000000000000000)))
(assert (= v_38 (bvshl #x0000000000000000000000000000000000000000000000000000000000000016 v_32)))
(assert (= v_39 (bvand v_38 #x00000000000000000000000000000000000000000000ffffffffffffffffffff)))
(assert (= v_40 (bvor v_37 v_39)))
(assert (= v_11 (bvand #x000000000000000000000000ffffffffffffffffffffffffffffffffffffffff v_10)))
(assert (= v_32 (bvand #x000000000000000000000000ffffffffffffffffffffffffffffffffffffffff v_11)))
(assert (= v_41 (bvshl #x000000000000000000000000000000000000000000000000000000000000000a v_32)))
(assert (= v_42 (bvand v_41 #xffffffffffffffffffffffffffffffffffffffffffff00000000000000000000)))
(assert (= v_43 (bvand #xffffffffffffffffffff00000000000000000000000000000000000000000000 v_42)))
(assert (= v_45 (bvand #xffffffffffffffffffffff000000000000000000000000000000000000000000 #x0000000000000000000000000000000000000003760000000000000000000000)))
(assert (= T T))
(assert (= T (if (distinct v_3 v_5 v_11 v_46) T F)))
(assert (= T (if (= v_73 F) T F)))
(assert (= T (if (= #x0000000000000000000000000000000000000000000000000000000000000000 v_46) F T)))
(assert (= T (if (bvugt v_46 #x0000000000000000000000000000000000000000000000000200000000000000) T F)))
(assert (= T (if (bvugt v_44 #x0000000000000000000000000000000000000000000000000200000000000000) T F)))
(assert (= T (if (= v_29 F) F T)))
(assert (= T (if (= v_23 F) F T)))
(assert (= T (if (= #x0000000000000000000000000000000000000000000000000000000000000000 v_11) F T)))
(assert (= T (if (= #x0000000000000000000000000000000000000000000000000000000000000000 v_5) F T)))
(assert (= T (if (= #x0000000000000000000000000000000000000000000000000000000000000000 v_3) F T)))
(check-sat)
(get-model)