Home
last modified time | relevance | path

Searched refs:zero_extend (Results 1 – 25 of 1953) sorted by relevance

12345678910>>...79

/dports/math/cvc4/CVC4-1.7/test/regress/regress0/bv/
H A Dfuzz15.smt53 (let (?e48 (zero_extend[6] ?e29))
81 (let (?e76 (zero_extend[2] ?e35))
86 (let (?e81 (zero_extend[2] ?e57))
89 (let (?e84 (zero_extend[1] ?e58))
100 (let (?e95 (zero_extend[2] v14))
120 (let (?e115 (zero_extend[0] v18))
136 (let (?e131 (zero_extend[4] v15))
259 (let (?e254 (zero_extend[0] ?e159))
283 (let (?e278 (zero_extend[14] ?e98))
299 (let (?e294 (zero_extend[3] ?e88))
[all …]
H A Dfuzz17.smt135 (let (?e130 (zero_extend[0] ?e75))
191 (let (?e186 (zero_extend[0] ?e116))
194 (let (?e189 (zero_extend[14] ?e126))
207 (let (?e202 (zero_extend[12] ?e78))
233 (let (?e228 (zero_extend[11] ?e142))
286 (let (?e281 (zero_extend[0] ?e189))
347 (let (?e342 (zero_extend[0] ?e216))
423 (let (?e418 (zero_extend[6] ?e59))
467 (let (?e462 (zero_extend[0] ?e322))
475 (let (?e470 (zero_extend[1] ?e180))
[all …]
H A Dfuzz16.smt59 (let (?e54 (zero_extend[1] ?e50))
100 (let (?e95 (zero_extend[1] ?e71))
102 (let (?e97 (zero_extend[0] ?e72))
112 (let (?e107 (zero_extend[1] ?e36))
279 (let (?e274 (zero_extend[2] ?e163))
337 (let (?e332 (zero_extend[0] ?e83))
338 (let (?e333 (zero_extend[7] ?e102))
429 (let (?e424 (zero_extend[3] ?e81))
457 (let (?e452 (zero_extend[0] ?e52))
506 (let (?e501 (zero_extend[4] ?e40))
[all …]
H A Dfuzz26.smt30 (let (?e25 (bvand (zero_extend[3] ?e8) ?e15))
32 (let (?e27 (zero_extend[2] ?e8))
33 (let (?e28 (bvmul ?e18 (zero_extend[3] ?e16)))
58 (let (?e53 (bvsub (zero_extend[3] ?e30) ?e32))
60 (let (?e55 (bvxor (zero_extend[3] ?e46) ?e23))
71 (let (?e66 (zero_extend[0] ?e23))
86 (let (?e81 (bvor (zero_extend[1] ?e70) ?e7))
96 (let (?e91 (zero_extend[1] ?e54))
122 (let (?e117 (zero_extend[2] ?e79))
125 (let (?e120 (zero_extend[3] ?e76))
[all …]
H A Dincorrect1.smt9 (let (?e4 (zero_extend[1] ?e3))
11 (let (?e6 (bvor ?e5 (zero_extend[3] ?e2)))
15 (let (?e10 (bvmul ?e8 (zero_extend[7] ?e7)))
20 (let (?e15 (bvashr ?e4 (zero_extend[1] ?e6)))
21 (let (?e16 (bvsdiv (zero_extend[7] ?e12) ?e10))
26 (let (?e21 (zero_extend[12] ?e19))
30 (let (?e25 (zero_extend[1] ?e3))
37 (let (?e32 (bvsdiv (zero_extend[7] ?e20) ?e17))
51 (let (?e46 (bvnor ?e14 (zero_extend[8] ?e29)))
60 (let (?e55 (bvor ?e4 (zero_extend[8] ?e24)))
[all …]
H A Dfuzz09.smt26 (let (?e21 (bvsub (zero_extend[12] ?e7) v2))
27 (let (?e22 (bvmul ?e18 (zero_extend[7] v0)))
34 (let (?e29 (bvlshr ?e6 (zero_extend[6] v0)))
76 (flet ($e71 (= ?e6 (zero_extend[8] ?e47)))
77 (flet ($e72 (= ?e56 (zero_extend[6] v0)))
86 (flet ($e81 (= ?e52 (zero_extend[2] ?e9)))
89 (flet ($e84 (= (zero_extend[7] v0) ?e27))
93 (flet ($e88 (= (zero_extend[2] ?e5) ?e46))
103 (flet ($e98 (= ?e52 (zero_extend[9] ?e8)))
132 (flet ($e127 (= (zero_extend[9] ?e8) v3))
[all …]
H A Dfuzz05.smt10 (let (?e5 (bvshl (zero_extend[8] v1) v3))
11 (let (?e6 (bvcomp v2 (zero_extend[11] v1)))
14 (let (?e9 (bvadd v1 (zero_extend[1] ?e6)))
23 (let (?e18 (bvand (zero_extend[1] ?e6) ?e9))
28 (let (?e23 (bvxor (zero_extend[1] ?e19) v1))
32 (let (?e27 (zero_extend[1] ?e22))
59 (flet ($e54 (= (zero_extend[1] ?e44) ?e13))
61 (flet ($e56 (= ?e4 (zero_extend[9] ?e39)))
80 (flet ($e75 (= (zero_extend[9] ?e21) ?e5))
89 (flet ($e84 (= v2 (zero_extend[1] v0)))
[all …]
H A Dfuzz07.smt18 (let (?e13 (bvor (zero_extend[1] ?e10) ?e5))
20 (let (?e15 (bvand (zero_extend[1] ?e12) ?e6))
26 (let (?e21 (bvlshr ?e3 (zero_extend[1] ?e12)))
27 (let (?e22 (bvcomp (zero_extend[1] ?e10) ?e6))
47 (let (?e42 (bvxor (zero_extend[3] ?e41) ?e8))
48 (let (?e43 (bvmul ?e3 (zero_extend[1] ?e12)))
62 (let (?e57 (zero_extend[12] ?e5))
74 (let (?e69 (zero_extend[4] ?e64))
93 (let (?e88 (bvmul (zero_extend[3] ?e3) v0))
102 (flet ($e97 (= (zero_extend[7] ?e20) ?e75))
[all …]
/dports/math/rumur/rumur-2021.09.29/misc/
H A Dwrite-raw.smt2134 (assert (bvult v (bvshl (_ bv1 128) ((_ zero_extend 64) h_width))))
196 (bvshl v ((_ zero_extend 64) h_offset))
232 …hl (_ bv1 128) ((_ zero_extend 64) high_bits)) (_ bv1 128)) (bvsub (bvmul ((_ zero_extend 64) low_…
334 (bvor ((_ zero_extend 8) ((_ extract 127 0) h_base2))
498 (bvor ((_ zero_extend 72) ((_ extract 63 0) h_base4))
518 …d h_base3 (bvsub (bvshl (_ bv1 136) ((_ zero_extend 72) (bvadd h_width h_offset))) (_ bv1 136))) (…
519 …(bvand ((_ zero_extend 8) v) (bvsub (bvshl (_ bv1 136) ((_ zero_extend 72) h_width)) (_ bv1 136)))…
528 (= (bvlshr h_base ((_ zero_extend 72) (bvadd h_width h_offset)))
534 …d h_base5 (bvsub (bvshl (_ bv1 136) ((_ zero_extend 72) (bvadd h_width h_offset))) (_ bv1 136))) (…
535 …(bvand ((_ zero_extend 8) v) (bvsub (bvshl (_ bv1 136) ((_ zero_extend 72) h_width)) (_ bv1 136)))…
[all …]
/dports/math/cvc4/CVC4-1.7/test/regress/regress0/aufbv/
H A Dfuzz02.smt31 (let (?e26 (bvashr ?e15 (zero_extend[6] ?e23)))
44 (let (?e39 (select a8 (zero_extend[1] ?e26)))
48 (let (?e43 (select ?e42 (zero_extend[1] ?e26)))
50 (let (?e45 (select a5 (zero_extend[4] ?e32)))
58 (let (?e53 (bvmul (zero_extend[10] ?e34) ?e37))
59 (let (?e54 (bvsub ?e21 (zero_extend[3] ?e15)))
61 (let (?e56 (bvsub (zero_extend[8] ?e17) ?e37))
107 (flet ($e102 (= ?e53 (zero_extend[12] ?e57)))
175 (flet ($e170 (= (zero_extend[5] ?e16) ?e67))
200 (flet ($e195 (= ?e43 (zero_extend[9] ?e17)))
[all …]
H A Dfuzz03.smt23 (let (?e18 (zero_extend[0] ?e13))
26 (let (?e21 (bvnor (zero_extend[8] ?e10) ?e17))
27 (let (?e22 (bvxnor v0 (zero_extend[2] ?e20)))
30 (let (?e25 (store a8 (zero_extend[2] ?e11) ?e17))
37 (let (?e32 (select a3 (zero_extend[4] ?e15)))
48 (let (?e43 (select ?e40 (zero_extend[2] ?e17)))
54 (let (?e49 (select ?e25 (zero_extend[2] ?e34)))
72 (let (?e67 (bvashr (zero_extend[7] v1) ?e34))
106 (flet ($e101 (= ?e43 (zero_extend[11] ?e93)))
188 (flet ($e183 (= (zero_extend[3] ?e91) ?e44))
[all …]
H A Dfuzz01.smt23 (let (?e18 (bvlshr (zero_extend[7] ?e17) v2))
26 (let (?e21 (bvnor (zero_extend[8] v1) v2))
39 (let (?e34 (select a3 (zero_extend[2] ?e23)))
40 (let (?e35 (select ?e30 (zero_extend[2] ?e20)))
43 (let (?e38 (select ?e26 (zero_extend[7] ?e31)))
47 (let (?e42 (select a3 (zero_extend[2] ?e23)))
55 (let (?e50 (bvxor (zero_extend[8] ?e34) ?e46))
59 (let (?e54 (bvor ?e32 (zero_extend[12] ?e53)))
73 (let (?e68 (zero_extend[7] ?e59))
95 (let (?e90 (bvadd (zero_extend[5] v2) ?e15))
[all …]
H A Dfuzz09.smt13 (let (?e8 (bvsrem (zero_extend[8] ?e6) v4))
16 (let (?e11 (store a5 (zero_extend[2] v2) (zero_extend[15] ?e10)))
19 (let (?e14 (select ?e12 (zero_extend[9] v0)))
32 (let (?e27 (bvsdiv (zero_extend[5] ?e7) ?e21))
40 (flet ($e35 (bvult v1 (zero_extend[5] ?e24)))
41 (flet ($e36 (= (zero_extend[15] ?e24) ?e15))
42 (flet ($e37 (bvule (zero_extend[6] v4) ?e14))
44 (flet ($e39 (bvsle ?e8 (zero_extend[8] ?e6)))
81 (flet ($e76 (bvult (zero_extend[1] v4) v2))
91 (flet ($e86 (= ?e8 (zero_extend[8] ?e6)))
[all …]
H A Dfuzz08.smt14 (let (?e9 (select a3 (zero_extend[4] ?e6)))
22 (let (?e17 (zero_extend[0] ?e7))
23 (let (?e18 (zero_extend[13] ?e9))
24 (let (?e19 (bvsrem (zero_extend[6] ?e10) v2))
32 (flet ($e27 (bvsgt (zero_extend[1] ?e4) ?e11))
34 (flet ($e29 (= v0 (zero_extend[11] ?e23)))
40 (flet ($e35 (bvslt (zero_extend[1] ?e4) ?e10))
63 (flet ($e58 (bvsgt v0 (zero_extend[3] v2)))
72 (flet ($e67 (= (zero_extend[2] ?e8) ?e16))
75 (flet ($e70 (bvslt (zero_extend[5] v2) v1))
[all …]
H A Dfuzz00.smt29 (let (?e24 (zero_extend[1] ?e12))
32 (flet ($e27 (= ?e7 (zero_extend[14] ?e17)))
36 (flet ($e31 (= ?e3 (zero_extend[7] ?e23)))
45 (flet ($e40 (= (zero_extend[8] ?e22) ?e3))
49 (flet ($e44 (= (zero_extend[10] ?e19) v1))
52 (flet ($e47 (= (zero_extend[6] ?e3) ?e6))
53 (flet ($e48 (= ?e7 (zero_extend[6] ?e3)))
57 (flet ($e52 (= v1 (zero_extend[2] ?e3)))
60 (flet ($e55 (= ?e6 (zero_extend[4] v1)))
69 (flet ($e64 (= ?e3 (zero_extend[7] v0)))
[all …]
/dports/math/cvc4/CVC4-1.7/test/regress/regress0/decision/
H A Daufbv-fuzz01.smt26 (let (?e18 (bvlshr (zero_extend[7] ?e17) v2))
29 (let (?e21 (bvnor (zero_extend[8] v1) v2))
42 (let (?e34 (select a3 (zero_extend[2] ?e23)))
43 (let (?e35 (select ?e30 (zero_extend[2] ?e20)))
46 (let (?e38 (select ?e26 (zero_extend[7] ?e31)))
50 (let (?e42 (select a3 (zero_extend[2] ?e23)))
58 (let (?e50 (bvxor (zero_extend[8] ?e34) ?e46))
62 (let (?e54 (bvor ?e32 (zero_extend[12] ?e53)))
76 (let (?e68 (zero_extend[7] ?e59))
98 (let (?e90 (bvadd (zero_extend[5] v2) ?e15))
[all …]
/dports/math/stp/stp-2.3.3/tests/query-files/sample-smt-tests/
H A Dtmp.FKuQABT1Bf.smt218 (let ((e964956 ((_ zero_extend 9) e964952)))
20 (let ((e964958 (bvashr v964949 ((_ zero_extend 2) e964957))))
23 (let ((e964961 (bvlshr v964948 ((_ zero_extend 5) e964955))))
24 (let ((e964962 (bvudiv ((_ zero_extend 7) v964949) e964953)))
34 (let ((e964972 (bvor ((_ zero_extend 1) e964967) e964962)))
74 (let ((e965012 (= e964986 ((_ zero_extend 6) e964978))))
95 (let ((e965033 (= ((_ zero_extend 7) e964954) e964970)))
114 (let ((e965052 (= ((_ zero_extend 1) e964956) e964953)))
118 (let ((e965056 (= e964966 ((_ zero_extend 5) e964985))))
135 (let ((e965073 (= ((_ zero_extend 7) e964954) e964960)))
[all …]
/dports/math/yices/yices-2.6.2/tests/regress/mantis/
H A D0007.smt217 (let ((e11 (bvlshr e5 ((_ zero_extend 15) e10))))
20 (let ((e14 ((_ zero_extend 1) e8)))
32 (let ((e26 (bvudiv ((_ zero_extend 1) e18) e5)))
38 (let ((e32 (bvnor e11 ((_ zero_extend 7) e28))))
39 (let ((e33 ((_ zero_extend 2) e8)))
40 (let ((e34 (bvurem ((_ zero_extend 8) e9) e28)))
44 (let ((e38 ((_ zero_extend 0) e17)))
113 (let ((e107 (= e34 ((_ zero_extend 8) e9))))
128 (let ((e122 (= ((_ zero_extend 6) e29) e74)))
221 (let ((e215 (= e71 ((_ zero_extend 4) v4))))
[all …]
H A D0035.smt216 (let ((e7 (f0 ((_ sign_extend 26) v1) ((_ zero_extend 48) e4) ((_ zero_extend 36) v1))))
20 (let ((e11 (bvsdiv ((_ zero_extend 94) e5) e9)))
22 (let ((e13 (bvudiv ((_ zero_extend 53) e5) v1)))
108 (let ((e99 ((_ zero_extend 13) e31)))
119 (let ((e110 (p0 ((_ zero_extend 44) e16) ((_ zero_extend 100) e95) ((_ zero_extend 65) e103))))
122 (let ((e113 (p0 ((_ zero_extend 44) e90) ((_ zero_extend 100) e16) ((_ sign_extend 65) e14))))
146 (let ((e137 (p0 ((_ extract 90 46) v3) ((_ zero_extend 36) e87) ((_ zero_extend 65) e51))))
185 (let ((e176 (p0 ((_ zero_extend 44) e8) ((_ zero_extend 100) e16) ((_ extract 65 0) e80))))
251 (let ((e242 (p0 ((_ extract 49 5) e58) ((_ zero_extend 100) e59) ((_ zero_extend 1) e87))))
281 (let ((e272 (p0 ((_ zero_extend 44) e39) ((_ extract 100 0) e98) ((_ zero_extend 65) e59))))
[all …]
H A D0032.smt213 (let ((e7 ((_ zero_extend 49) v2)))
16 (let ((e10 (bvsrem ((_ zero_extend 42) e9) e6)))
21 (let ((e15 ((_ zero_extend 20) e5)))
33 (let ((e27 (bvashr ((_ zero_extend 91) e17) e7)))
35 (let ((e29 (bvcomp v1 ((_ zero_extend 38) e18))))
38 (let ((e32 (bvudiv ((_ zero_extend 42) e8) e30)))
40 (let ((e34 (bvxor ((_ zero_extend 3) e7) e4)))
48 (let ((e42 ((_ zero_extend 62) e24)))
57 (let ((e51 (bvsub v2 ((_ zero_extend 41) e28))))
58 (let ((e52 ((_ zero_extend 19) e15)))
[all …]
/dports/math/cvc4/CVC4-1.7/test/regress/regress1/bv/
H A Dfuzz34.smt10 (let (?e5 (zero_extend[0] v0))
14 (let (?e9 (bvmul ?e5 (zero_extend[3] ?e6)))
65 (let (?e60 (zero_extend[0] ?e29))
108 (let (?e103 (zero_extend[2] ?e31))
137 (let (?e132 (zero_extend[0] ?e16))
145 (let (?e140 (zero_extend[2] ?e17))
257 (let (?e252 (zero_extend[0] ?e24))
269 (let (?e264 (zero_extend[0] ?e144))
285 (let (?e280 (zero_extend[0] ?e74))
313 (let (?e308 (zero_extend[3] ?e229))
[all …]
/dports/lang/gcc11-devel/gcc-11-20211009/gcc/config/pru/
H A Dalu-zext.md54 (zero_extend:EQD
56 (zero_extend:EQD
68 (zero_extend:EQD
70 (zero_extend:EQD
83 [(zero_extend:EQD
85 (zero_extend:EQD
116 (zero_extend:EQD
126 (zero_extend:EQD
137 (zero_extend:EQD
139 (zero_extend:EQD
[all …]
/dports/lang/gcc12-devel/gcc-12-20211205/gcc/config/pru/
H A Dalu-zext.md54 (zero_extend:EQD
56 (zero_extend:EQD
68 (zero_extend:EQD
70 (zero_extend:EQD
83 [(zero_extend:EQD
85 (zero_extend:EQD
116 (zero_extend:EQD
126 (zero_extend:EQD
137 (zero_extend:EQD
139 (zero_extend:EQD
[all …]
/dports/misc/cxx_atomics_pic/gcc-11.2.0/gcc/config/pru/
H A Dalu-zext.md54 (zero_extend:EQD
56 (zero_extend:EQD
68 (zero_extend:EQD
70 (zero_extend:EQD
83 [(zero_extend:EQD
85 (zero_extend:EQD
116 (zero_extend:EQD
126 (zero_extend:EQD
137 (zero_extend:EQD
139 (zero_extend:EQD
[all …]
/dports/lang/gcc11/gcc-11.2.0/gcc/config/pru/
H A Dalu-zext.md54 (zero_extend:EQD
56 (zero_extend:EQD
68 (zero_extend:EQD
70 (zero_extend:EQD
83 [(zero_extend:EQD
85 (zero_extend:EQD
116 (zero_extend:EQD
126 (zero_extend:EQD
137 (zero_extend:EQD
139 (zero_extend:EQD
[all …]

12345678910>>...79