Home
last modified time | relevance | path

Searched refs:bvugt (Results 1 – 25 of 143) sorted by relevance

123456

/dports/math/rumur/rumur-2021.09.29/misc/
H A Dread-raw.smt2128 (assert (= u128_branch (bvugt aligned_width (bvmul (bvsub (_ bv8 64) (_ bv1 64)) (_ bv8 64)))))
141 (ite (bvugt low_size (_ bv16 64))
150 …(ite (bvugt low_size2 (_ bv0 64)) ((_ zero_extend 120) ((_ extract 7 0) h_base)) (_ bv…
257 (assert (= low_size4 (ite (bvugt low_size3 (_ bv8 64)) (_ bv8 64) low_size3)))
262 …(ite (bvugt low_size4 (_ bv0 64)) ((_ zero_extend 56) ((_ extract 7 0) h_base)) (_ bv0 6…
263 …(ite (bvugt low_size4 (_ bv1 64)) (bvshl ((_ zero_extend 56) ((_ extract 15 8) h_base)) (_ bv8 6…
264 …(ite (bvugt low_size4 (_ bv2 64)) (bvshl ((_ zero_extend 56) ((_ extract 23 16) h_base)) (_ bv16 6…
265 …(ite (bvugt low_size4 (_ bv3 64)) (bvshl ((_ zero_extend 56) ((_ extract 31 24) h_base)) (_ bv24 6…
266 …(ite (bvugt low_size4 (_ bv4 64)) (bvshl ((_ zero_extend 56) ((_ extract 39 32) h_base)) (_ bv32 6…
336 (or (not u128_branch) (bvugt h_width (_ bv64 64)) (= ((_ extract 63 0) spec) ret))
[all …]
H A Dwrite-raw.smt2151 (assert (= u128_branch (and defined__SIZEOF_INT128__ (bvugt aligned_width (bvmul (bvsub (_ bv8 64) …
165 (bvugt low_size (_ bv16 64))
352 (bvugt low_size3 (_ bv8 64))
361 …(bvor (ite (bvugt low_size4 (_ bv0 64)) (bvshl ((_ zero_extend 56) ((_ extract 7 0) h_base)) (_ …
362 …(ite (bvugt low_size4 (_ bv1 64)) (bvshl ((_ zero_extend 56) ((_ extract 15 8) h_base)) (_ bv8 6…
363 …(ite (bvugt low_size4 (_ bv2 64)) (bvshl ((_ zero_extend 56) ((_ extract 23 16) h_base)) (_ bv16 6…
364 …(ite (bvugt low_size4 (_ bv3 64)) (bvshl ((_ zero_extend 56) ((_ extract 31 24) h_base)) (_ bv24 6…
365 …(ite (bvugt low_size4 (_ bv4 64)) (bvshl ((_ zero_extend 56) ((_ extract 39 32) h_base)) (_ bv32 6…
533 (or u128_branch (bvugt h_width (_ bv64 64))
539 (or u128_branch (= h_offset (_ bv0 64)) (bvugt h_width (_ bv64 64))
[all …]
/dports/math/cvc4/CVC4-1.7/test/regress/regress0/bv/
H A Dfuzz15.smt367 (flet ($e362 (bvugt ?e250 ?e62))
411 (flet ($e406 (bvugt ?e289 ?e60))
525 (flet ($e520 (bvugt ?e134 ?e87))
570 (flet ($e565 (bvugt ?e91 ?e123))
583 (flet ($e578 (bvugt ?e221 ?e60))
589 (flet ($e584 (bvugt ?e62 ?e44))
625 (flet ($e620 (bvugt ?e203 ?e198))
629 (flet ($e624 (bvugt ?e317 ?e233))
856 (flet ($e851 (bvugt ?e51 ?e289))
924 (flet ($e919 (bvugt ?e22 ?e89))
[all …]
H A Dfuzz25.smt72 (flet ($e67 (bvugt ?e13 ?e65))
87 (flet ($e82 (bvugt ?e55 ?e44))
94 (flet ($e89 (bvugt ?e21 ?e13))
99 (flet ($e94 (bvugt ?e24 ?e37))
107 (flet ($e102 (bvugt ?e52 ?e50))
124 (flet ($e119 (bvugt v0 ?e29))
134 (flet ($e129 (bvugt ?e19 ?e50))
162 (flet ($e157 (bvugt ?e14 ?e28))
198 (flet ($e193 (bvugt ?e43 ?e11))
232 (flet ($e227 (bvugt ?e37 ?e9))
[all …]
H A Dfuzz17.smt605 (flet ($e600 (bvugt ?e52 ?e339))
645 (flet ($e640 (bvugt ?e373 ?e568))
675 (flet ($e670 (bvugt ?e108 ?e481))
728 (flet ($e723 (bvugt ?e378 ?e543))
797 (flet ($e792 (bvugt ?e388 ?e333))
891 (flet ($e886 (bvugt ?e68 ?e231))
959 (flet ($e954 (bvugt ?e428 ?e271))
965 (flet ($e960 (bvugt ?e357 ?e242))
995 (flet ($e990 (bvugt ?e206 ?e53))
1203 (flet ($e1198 (bvugt ?e432 ?e63))
[all …]
H A Dfuzz16.smt708 (flet ($e703 (bvugt ?e298 ?e378))
734 (flet ($e729 (bvugt ?e140 ?e149))
755 (flet ($e750 (bvugt ?e126 ?e657))
782 (flet ($e777 (bvugt ?e400 ?e429))
789 (flet ($e784 (bvugt ?e126 ?e313))
845 (flet ($e840 (bvugt ?e644 ?e96))
929 (flet ($e924 (bvugt ?e420 ?e665))
953 (flet ($e948 (bvugt ?e137 ?e374))
983 (flet ($e978 (bvugt ?e323 ?e469))
1003 (flet ($e998 (bvugt ?e267 ?e371))
[all …]
H A Dfuzz31.smt99 (flet ($e94 (bvugt v2 ?e45))
105 (flet ($e100 (bvugt ?e48 ?e35))
114 (flet ($e109 (bvugt ?e31 ?e32))
127 (flet ($e122 (bvugt ?e43 ?e55))
131 (flet ($e126 (bvugt ?e87 ?e61))
158 (flet ($e153 (bvugt v0 ?e48))
193 (flet ($e188 (bvugt ?e22 ?e24))
203 (flet ($e198 (bvugt ?e48 ?e42))
210 (flet ($e205 (bvugt ?e84 ?e34))
246 (flet ($e241 (bvugt ?e65 ?e17))
[all …]
H A Dfuzz20.smt61 (flet ($e56 (bvugt ?e41 ?e6))
63 (flet ($e58 (bvugt ?e5 ?e25))
66 (flet ($e61 (bvugt ?e35 ?e15))
67 (flet ($e62 (bvugt ?e47 ?e17))
70 (flet ($e65 (bvugt ?e6 ?e5))
91 (flet ($e86 (bvugt ?e23 ?e16))
95 (flet ($e90 (bvugt ?e42 ?e31))
120 (flet ($e115 (bvugt ?e48 ?e34))
122 (flet ($e117 (bvugt ?e12 v0))
125 (flet ($e120 (bvugt ?e42 ?e47))
[all …]
H A Dfuzz26.smt170 (flet ($e165 (bvugt ?e71 ?e4))
173 (flet ($e168 (bvugt ?e25 ?e96))
213 (flet ($e208 (bvugt ?e82 ?e42))
253 (flet ($e248 (bvugt ?e5 ?e116))
274 (flet ($e269 (bvugt ?e46 ?e31))
333 (flet ($e328 (bvugt ?e11 ?e48))
350 (flet ($e345 (bvugt ?e90 ?e32))
401 (flet ($e396 (bvugt v1 ?e71))
408 (flet ($e403 (bvugt ?e30 ?e78))
416 (flet ($e411 (bvugt v2 ?e126))
[all …]
H A Dfuzz28.smt109 (flet ($e104 (bvugt ?e73 ?e17))
128 (flet ($e123 (bvugt ?e73 v2))
133 (flet ($e128 (bvugt ?e56 v1))
136 (flet ($e131 (bvugt ?e73 ?e10))
142 (flet ($e137 (bvugt ?e45 ?e13))
143 (flet ($e138 (bvugt ?e51 ?e19))
174 (flet ($e169 (bvugt ?e70 ?e70))
188 (flet ($e183 (bvugt ?e72 ?e8))
195 (flet ($e190 (bvugt ?e35 v2))
229 (flet ($e224 (bvugt ?e44 ?e14))
[all …]
H A Dfuzz35.smt28 (let (?e23 (ite (bvugt v1 ?e5) bv1[1] bv0[1]))
33 (let (?e28 (ite (bvugt ?e9 ?e12) bv1[1] bv0[1]))
74 (flet ($e69 (bvugt ?e36 ?e24))
89 (flet ($e84 (bvugt ?e23 ?e53))
103 (flet ($e98 (bvugt ?e51 ?e42))
116 (flet ($e111 (bvugt ?e8 v3))
122 (flet ($e117 (bvugt ?e10 ?e7))
148 (flet ($e143 (bvugt ?e61 v2))
155 (flet ($e150 (bvugt ?e31 ?e54))
180 (flet ($e175 (bvugt ?e26 ?e11))
[all …]
H A Dfuzz21.smt18 (let (?e13 (ite (bvugt ?e7 v3) bv1[1] bv0[1]))
49 (let (?e44 (ite (bvugt v4 ?e9) bv1[1] bv0[1]))
141 (flet ($e136 (bvugt ?e51 ?e44))
172 (flet ($e167 (bvugt ?e96 ?e39))
175 (flet ($e170 (bvugt ?e88 ?e73))
209 (flet ($e204 (bvugt ?e54 ?e81))
233 (flet ($e228 (bvugt ?e56 ?e61))
236 (flet ($e231 (bvugt ?e37 ?e80))
244 (flet ($e239 (bvugt ?e38 v4))
287 (flet ($e282 (bvugt ?e96 ?e36))
[all …]
H A Dfuzz36.smt23 (let (?e18 (ite (bvugt ?e7 ?e5) bv1[1] bv0[1]))
43 (let (?e38 (ite (bvugt ?e17 ?e29) bv1[1] bv0[1]))
102 (flet ($e97 (bvugt ?e59 (zero_extend[3] ?e26)))
103 (flet ($e98 (bvugt ?e13 (zero_extend[2] ?e34)))
131 (flet ($e126 (bvugt ?e9 ?e53))
145 (flet ($e140 (bvugt ?e25 ?e60))
150 (flet ($e145 (bvugt ?e6 ?e7))
151 (flet ($e146 (bvugt ?e45 ?e37))
157 (flet ($e152 (bvugt ?e25 ?e66))
158 (flet ($e153 (bvugt ?e28 ?e19))
[all …]
H A Dincorrect1.smt12 (let (?e7 (ite (bvugt v0 ?e3) bv1[1] bv0[1]))
133 (flet ($e128 (bvugt ?e60 ?e64))
142 (flet ($e137 (bvugt ?e4 (sign_extend[1] v0)))
153 (flet ($e148 (bvugt ?e16 ?e3))
164 (flet ($e159 (bvugt ?e33 ?e9))
170 (flet ($e165 (bvugt ?e81 ?e52))
172 (flet ($e167 (bvugt ?e71 ?e27))
237 (flet ($e232 (bvugt ?e98 ?e18))
357 (flet ($e352 (bvugt ?e32 ?e83))
375 (flet ($e370 (bvugt ?e84 ?e27))
[all …]
H A Dinequality05.smt218 (bvugt v7 v1)
21 (bvugt v1 v0)
25 (bvugt v3 v6)
/dports/sysutils/triton/Triton-0.8.1/src/examples/pin/
H A Dcrackme_hash_collision.py72 astCtxt.bvugt(astCtxt.variable(SymVar_0), astCtxt.bv(96, CPUSIZE.QWORD_BIT)),
74 astCtxt.bvugt(astCtxt.variable(SymVar_1), astCtxt.bv(96, CPUSIZE.QWORD_BIT)),
76 astCtxt.bvugt(astCtxt.variable(SymVar_2), astCtxt.bv(96, CPUSIZE.QWORD_BIT)),
78 astCtxt.bvugt(astCtxt.variable(SymVar_3), astCtxt.bv(96, CPUSIZE.QWORD_BIT)),
80 astCtxt.bvugt(astCtxt.variable(SymVar_4), astCtxt.bv(96, CPUSIZE.QWORD_BIT)),
/dports/math/cvc4/CVC4-1.7/test/regress/regress1/bv/
H A Dbv-proof00.smt293 (flet ($e288 (bvugt ?e201 ?e122))
309 (flet ($e304 (bvugt ?e55 ?e158))
327 (flet ($e322 (bvugt ?e154 ?e239))
340 (flet ($e335 (bvugt ?e138 ?e218))
347 (flet ($e342 (bvugt ?e173 ?e72))
551 (flet ($e546 (bvugt ?e106 ?e18))
602 (flet ($e597 (bvugt ?e146 ?e39))
611 (flet ($e606 (bvugt ?e132 v1))
744 (flet ($e739 (bvugt ?e76 ?e31))
769 (flet ($e764 (bvugt ?e34 ?e29))
[all …]
H A Dfuzz34.smt701 (flet ($e696 (bvugt ?e147 ?e349))
705 (flet ($e700 (bvugt ?e74 ?e343))
714 (flet ($e709 (bvugt ?e240 ?e16))
723 (flet ($e718 (bvugt ?e6 ?e589))
749 (flet ($e744 (bvugt ?e100 ?e542))
782 (flet ($e777 (bvugt ?e57 ?e196))
915 (flet ($e910 (bvugt ?e69 ?e632))
974 (flet ($e969 (bvugt ?e82 ?e111))
1021 (flet ($e1016 (bvugt ?e338 ?e2))
1808 (flet ($e1803 (bvugt ?e73 ?e39))
[all …]
/dports/math/yices/yices-2.6.2/tests/regress/mantis/
H A D0006.smt263 (let ((e57 (bvugt e47 ((_ sign_extend 14) e34))))
68 (let ((e62 (bvugt ((_ sign_extend 3) e45) e46)))
71 (let ((e65 (bvugt ((_ zero_extend 14) e44) e39)))
80 (let ((e74 (bvugt ((_ zero_extend 9) e25) e24)))
85 (let ((e79 (bvugt e36 e26)))
87 (let ((e81 (bvugt e13 ((_ zero_extend 1) e9))))
101 (let ((e95 (bvugt e11 ((_ sign_extend 11) e6))))
102 (let ((e96 (bvugt e42 ((_ sign_extend 1) e34))))
126 (let ((e120 (bvugt e45 e30)))
138 (let ((e132 (bvugt e25 e10)))
[all …]
H A D0012.smt291 (let ((e85 (bvugt ((_ sign_extend 5) e4) e38)))
120 (let ((e114 (bvugt e24 e54)))
129 (let ((e123 (bvugt e35 e15)))
165 (let ((e159 (bvugt e29 e38)))
209 (let ((e203 (bvugt e38 e70)))
215 (let ((e209 (bvugt e22 e47)))
271 (let ((e265 (bvugt e51 e58)))
281 (let ((e275 (bvugt e65 e30)))
286 (let ((e280 (bvugt e82 e52)))
316 (let ((e310 (bvugt e57 e28)))
[all …]
H A D0007.smt2121 (let ((e115 (bvugt ((_ sign_extend 8) e88) e70)))
134 (let ((e128 (bvugt ((_ zero_extend 8) e35) e83)))
147 (let ((e141 (bvugt ((_ sign_extend 8) e24) e28)))
163 (let ((e157 (bvugt e92 e66)))
173 (let ((e167 (bvugt e5 e65)))
182 (let ((e176 (bvugt e95 e42)))
218 (let ((e212 (bvugt e102 e72)))
266 (let ((e260 (bvugt e65 e32)))
281 (let ((e275 (bvugt e41 e100)))
284 (let ((e278 (bvugt e21 e36)))
[all …]
H A D0023.smt236 (let ((e30 (bvugt e21 e19)))
40 (let ((e34 (bvugt ((_ sign_extend 7) e25) e23)))
42 (let ((e36 (bvugt ((_ zero_extend 1) e18) e26)))
44 (let ((e38 (bvugt e15 e17)))
47 (let ((e41 (bvugt e17 v3)))
53 (let ((e47 (bvugt e26 ((_ sign_extend 1) e7))))
69 (let ((e63 (bvugt ((_ zero_extend 1) e6) e22)))
80 (let ((e74 (bvugt e13 ((_ sign_extend 9) v0))))
81 (let ((e75 (bvugt e4 ((_ sign_extend 6) v0))))
/dports/math/cvc4/CVC4-1.7/test/regress/regress1/aufbv/
H A Dfuzz10.smt24 (let (?e19 (ite (bvugt ?e16 (zero_extend[3] ?e14)) bv1[1] bv0[1]))
34 (flet ($e29 (bvugt ?e24 ?e17))
37 (flet ($e32 (bvugt (sign_extend[13] ?e8) ?e25))
41 (flet ($e36 (bvugt ?e20 ?e27))
43 (flet ($e38 (bvugt ?e25 (zero_extend[13] ?e24)))
56 (flet ($e51 (bvugt ?e8 ?e12))
57 (flet ($e52 (bvugt ?e22 (zero_extend[3] ?e16)))
67 (flet ($e62 (bvugt ?e22 (sign_extend[13] ?e8)))
68 (flet ($e63 (bvugt (zero_extend[7] ?e24) ?e26))
69 (flet ($e64 (bvugt ?e9 (sign_extend[13] ?e18)))
[all …]
/dports/math/cvc4/CVC4-1.7/test/regress/regress0/aufbv/
H A Dfuzz12.smt38 (let (?e33 (ite (bvugt ?e6 ?e24) bv1[1] bv0[1]))
46 (flet ($e41 (bvugt ?e21 (sign_extend[6] ?e25)))
56 (flet ($e51 (bvugt (zero_extend[8] ?e23) ?e25))
57 (flet ($e52 (bvugt v1 (sign_extend[6] ?e26)))
60 (flet ($e55 (bvugt ?e7 (zero_extend[6] ?e14)))
70 (flet ($e65 (bvugt (zero_extend[14] ?e33) ?e7))
75 (flet ($e70 (bvugt ?e29 (zero_extend[13] ?e4)))
80 (flet ($e75 (bvugt v0 (zero_extend[6] ?e13)))
93 (flet ($e88 (bvugt ?e13 (sign_extend[6] ?e4)))
95 (flet ($e90 (bvugt ?e9 (sign_extend[6] ?e13)))
[all …]
/dports/math/stp/stp-2.3.3/tests/query-files/sample-smt-tests/
H A Dtmp.liyo9rgPx3.smt285 (let ((e1109460 (bvugt e1109423 e1109431)))
89 (let ((e1109464 (bvugt ((_ sign_extend 10) e1109436) e1109401)))
103 (let ((e1109478 (bvugt e1109434 e1109419)))
116 (let ((e1109491 (bvugt e1109404 e1109413)))
117 (let ((e1109492 (bvugt e1109407 e1109408)))
133 (let ((e1109508 (bvugt e1109431 e1109423)))
139 (let ((e1109514 (bvugt e1109427 e1109425)))
200 (let ((e1109575 (bvugt e1109390 e1109400)))
208 (let ((e1109583 (bvugt e1109407 e1109403)))
256 (let ((e1109631 (bvugt e1109410 e1109410)))
[all …]

123456