| /dports/math/cvc4/CVC4-1.7/test/regress/regress0/bv/ |
| H A D | fuzz15.smt | 33 (let (?e28 (bvand (sign_extend[5] v12) v18))
36 (let (?e31 (bvand (sign_extend[2] v17) v2))
44 (let (?e39 (bvand v2 (sign_extend[9] ?e38)))
49 (let (?e44 (bvadd v3 (sign_extend[6] v11)))
50 (let (?e45 (sign_extend[5] v1))
77 (let (?e72 (sign_extend[0] ?e55))
88 (let (?e83 (sign_extend[0] v5))
230 (let (?e225 (sign_extend[4] ?e131))
309 (let (?e304 (sign_extend[0] ?e157))
326 (let (?e321 (sign_extend[13] ?e230))
[all …]
|
| H A D | fuzz17.smt | 36 (let (?e31 (sign_extend[5] v6))
44 (let (?e39 (sign_extend[0] v5))
45 (let (?e40 (sign_extend[0] v6))
93 (let (?e88 (sign_extend[0] ?e50))
98 (let (?e93 (sign_extend[0] ?e29))
105 (let (?e100 (sign_extend[0] ?e36))
157 (let (?e152 (sign_extend[8] ?e137))
173 (let (?e168 (sign_extend[0] ?e49))
239 (let (?e234 (sign_extend[1] ?e40))
248 (let (?e243 (sign_extend[0] v12))
[all …]
|
| H A D | fuzz16.smt | 54 (let (?e49 (sign_extend[1] v11))
84 (let (?e79 (sign_extend[0] ?e49))
165 (let (?e160 (sign_extend[3] ?e135))
232 (let (?e227 (sign_extend[0] ?e109))
248 (let (?e243 (sign_extend[0] ?e196))
264 (let (?e259 (sign_extend[0] ?e77))
291 (let (?e286 (sign_extend[0] ?e155))
333 (let (?e328 (sign_extend[3] v15))
364 (let (?e359 (sign_extend[6] v13))
417 (let (?e412 (sign_extend[8] ?e44))
[all …]
|
| H A D | fuzz09.smt | 13 (let (?e8 (bvnor (sign_extend[2] v1) v0))
14 (let (?e9 (sign_extend[1] v2))
18 (let (?e13 (bvsub (sign_extend[8] v1) v2))
21 (let (?e16 (bvnand (sign_extend[1] ?e5) v2))
22 (let (?e17 (bvor ?e9 (sign_extend[9] v1)))
23 (let (?e18 (bvxnor ?e9 (sign_extend[7] v0)))
52 (let (?e47 (sign_extend[4] ?e7))
57 (let (?e52 (sign_extend[15] ?e45))
64 (let (?e59 (sign_extend[0] ?e21))
73 (flet ($e68 (= ?e9 (sign_extend[8] ?e36)))
[all …]
|
| H A D | fuzz41.smt | 16 (let (?e11 (bvurem (sign_extend[10] ?e8) ?e6))
18 (let (?e13 (bvnor (sign_extend[2] ?e11) ?e7))
21 (let (?e16 (bvsmod (sign_extend[2] ?e12) ?e5))
26 (let (?e21 (bvsdiv (sign_extend[4] ?e15) ?e17))
35 (let (?e30 (sign_extend[0] ?e21))
45 (flet ($e40 (bvult ?e6 (sign_extend[3] ?e9)))
47 (flet ($e42 (bvult v2 (sign_extend[12] ?e8)))
72 (flet ($e67 (= (sign_extend[2] ?e25) ?e14))
84 (flet ($e79 (= (sign_extend[10] ?e26) ?e6))
87 (flet ($e82 (= (sign_extend[4] ?e35) ?e34))
[all …]
|
| H A D | fuzz21.smt | 27 (let (?e22 (bvxnor (sign_extend[3] ?e20) ?e7))
30 (let (?e25 (bvand (sign_extend[3] ?e18) v3))
33 (let (?e28 (bvshl ?e25 (sign_extend[3] ?e26)))
46 (let (?e41 (bvsub (sign_extend[3] ?e21) ?e27))
50 (let (?e45 (bvadd (sign_extend[3] ?e44) ?e41))
58 (let (?e53 (sign_extend[3] ?e34))
68 (let (?e63 (bvsub ?e33 (sign_extend[3] ?e37)))
91 (let (?e86 (sign_extend[0] ?e38))
144 (flet ($e139 (= (sign_extend[3] ?e12) v2))
158 (flet ($e153 (= (sign_extend[3] ?e49) ?e6))
[all …]
|
| H A D | fuzz31.smt | 24 (let (?e19 (bvcomp ?e17 (sign_extend[3] ?e9)))
25 (let (?e20 (bvxor (sign_extend[3] ?e13) ?e15))
40 (let (?e35 (sign_extend[0] ?e23))
44 (let (?e39 (bvnand (sign_extend[3] ?e9) ?e5))
45 (let (?e40 (bvlshr ?e23 (sign_extend[3] ?e10)))
47 (let (?e42 (bvshl (sign_extend[3] ?e12) ?e35))
50 (let (?e45 (bvmul ?e16 (sign_extend[3] ?e18)))
55 (let (?e50 (bvor (sign_extend[3] ?e44) ?e36))
77 (let (?e72 (bvor (sign_extend[3] ?e10) ?e39))
100 (flet ($e95 (= ?e30 (sign_extend[3] ?e12)))
[all …]
|
| H A D | fuzz32.smt | 28 (let (?e23 (sign_extend[1] ?e19))
42 (let (?e37 (bvnor (sign_extend[3] ?e29) v2))
47 (let (?e42 (bvashr (sign_extend[3] ?e29) ?e21))
63 (let (?e58 (bvcomp ?e51 (sign_extend[1] ?e23)))
71 (let (?e66 (bvshl ?e45 (sign_extend[2] ?e39)))
76 (let (?e71 (sign_extend[0] ?e24))
85 (let (?e80 (sign_extend[3] ?e32))
134 (let (?e129 (sign_extend[0] ?e38))
135 (let (?e130 (sign_extend[0] ?e17))
137 (let (?e132 (sign_extend[0] ?e96))
[all …]
|
| H A D | fuzz04.smt | 12 (let (?e7 (bvxor (sign_extend[4] v3) v1))
15 (let (?e10 (bvshl v1 (sign_extend[6] v0)))
30 (let (?e25 (sign_extend[7] ?e22))
31 (let (?e26 (bvnand (sign_extend[6] v0) v1))
42 (flet ($e37 (= (sign_extend[8] ?e24) ?e12))
43 (flet ($e38 (= (sign_extend[10] v3) v2))
45 (flet ($e40 (= ?e19 (sign_extend[6] ?e9)))
50 (flet ($e45 (= v2 (sign_extend[12] ?e31)))
57 (flet ($e52 (= (sign_extend[8] ?e18) ?e4))
66 (flet ($e61 (= v2 (sign_extend[12] ?e9)))
[all …]
|
| H A D | incorrect1.smt | 8 (let (?e3 (bvsrem (sign_extend[3] ?e2) v0))
14 (let (?e9 (bvadd ?e4 (sign_extend[4] ?e2)))
19 (let (?e14 (bvsmod (sign_extend[1] ?e13) ?e9))
33 (let (?e28 (bvudiv (sign_extend[7] ?e11) ?e6))
36 (let (?e31 (sign_extend[2] ?e15))
38 (let (?e33 (bvxor ?e9 (sign_extend[4] ?e2)))
41 (let (?e36 (sign_extend[9] ?e35))
42 (let (?e37 (bvadd ?e9 (sign_extend[8] ?e27)))
45 (let (?e40 (bvsmod (sign_extend[7] ?e27) v0))
78 (let (?e73 (sign_extend[1] ?e48))
[all …]
|
| H A D | fuzz26.smt | 15 (let (?e10 (sign_extend[3] ?e8))
27 (let (?e22 (bvadd v0 (sign_extend[3] ?e19)))
31 (let (?e26 (bvlshr v0 (sign_extend[3] ?e19)))
37 (let (?e32 (bvshl ?e10 (sign_extend[3] ?e21)))
48 (let (?e43 (sign_extend[1] ?e33))
49 (let (?e44 (bvnand (sign_extend[3] ?e19) v0))
62 (let (?e57 (sign_extend[0] ?e3))
100 (let (?e95 (sign_extend[1] ?e62))
124 (let (?e119 (sign_extend[3] ?e101))
172 (flet ($e167 (= (sign_extend[3] ?e80) ?e5))
[all …]
|
| /dports/math/cvc4/CVC4-1.7/test/regress/regress0/aufbv/ |
| H A D | fuzz14.smt | 12 (let (?e7 (bvxor (sign_extend[7] v1) ?e6))
14 (let (?e9 (sign_extend[2] ?e5))
20 (let (?e15 (store ?e11 (sign_extend[3] v1) (sign_extend[6] v3)))
22 (let (?e17 (bvcomp ?e8 (sign_extend[4] ?e7)))
28 (let (?e23 (bvnand v0 (sign_extend[1] ?e20)))
29 (flet ($e24 (bvsge v2 (sign_extend[7] ?e23)))
30 (flet ($e25 (bvsgt (sign_extend[6] v3) ?e13))
32 (flet ($e27 (= v1 (sign_extend[1] ?e17)))
34 (flet ($e29 (bvule (sign_extend[4] ?e7) ?e8))
43 (flet ($e38 (= (sign_extend[10] ?e5) v2))
[all …]
|
| H A D | fuzz02.smt | 29 (let (?e24 (sign_extend[4] v2))
63 (let (?e58 (bvcomp (sign_extend[9] ?e32) ?e13))
65 (let (?e60 (bvadd ?e37 (sign_extend[8] ?e17)))
77 (let (?e72 (bvcomp (sign_extend[3] v2) ?e65))
87 (let (?e82 (sign_extend[1] v1))
88 (let (?e83 (bvor (sign_extend[2] ?e33) v4))
103 (flet ($e98 (bvuge v0 (sign_extend[5] ?e33)))
135 (flet ($e130 (= (sign_extend[6] ?e32) ?e26))
155 (flet ($e150 (= (sign_extend[1] ?e37) v0))
174 (flet ($e169 (= (sign_extend[5] ?e68) ?e55))
[all …]
|
| H A D | fuzz03.smt | 25 (let (?e20 (sign_extend[12] ?e15))
32 (let (?e27 (store ?e25 (sign_extend[13] ?e15) (sign_extend[6] ?e18)))
38 (let (?e33 (select a4 (sign_extend[1] v0)))
39 (let (?e34 (select ?e29 (sign_extend[13] ?e30)))
40 (let (?e35 (select ?e25 (sign_extend[13] ?e31)))
41 (let (?e36 (select ?e25 (sign_extend[10] ?e23)))
42 (let (?e37 (select a8 (sign_extend[10] ?e10)))
47 (let (?e42 (select ?e39 (sign_extend[1] ?e20)))
70 (let (?e65 (bvand (sign_extend[1] ?e37) ?e16))
76 (let (?e71 (sign_extend[3] ?e51))
[all …]
|
| H A D | fuzz11.smt | 13 (let (?e8 (bvurem (sign_extend[7] v1) v2))
15 (let (?e10 (bvmul (sign_extend[14] v1) ?e6))
16 (let (?e11 (bvcomp v0 (sign_extend[2] v2)))
25 (let (?e20 (bvurem (sign_extend[12] v1) ?e19))
26 (let (?e21 (bvnand (sign_extend[6] ?e12) ?e7))
33 (let (?e28 (bvxor (sign_extend[2] v2) v0))
49 (flet ($e44 (= (sign_extend[12] v1) ?e15))
57 (flet ($e52 (= ?e8 (sign_extend[8] ?e25)))
63 (flet ($e58 (= (sign_extend[1] ?e22) v1))
66 (flet ($e61 (bvsle (sign_extend[2] v2) v0))
[all …]
|
| /dports/math/yices/yices-2.6.2/tests/regress/mantis/ |
| H A D | 0013.b.smt2 | 16 (let ((e10 (bvudiv ((_ sign_extend 2) v2) e5)))
21 (let ((e15 (bvsdiv ((_ sign_extend 5) e5) v0)))
24 (let ((e18 (bvsrem ((_ sign_extend 2) v2) e10)))
30 (let ((e24 (bvnor e11 ((_ sign_extend 14) e16))))
41 (let ((e35 ((_ sign_extend 7) e27)))
57 (let ((e51 (bvxnor e7 ((_ sign_extend 7) e32))))
66 (let ((e60 ((_ sign_extend 4) e49)))
94 (let ((e88 ((_ sign_extend 6) e49)))
177 (let ((e171 (= ((_ sign_extend 6) e98) e95)))
379 (let ((e373 (= ((_ sign_extend 7) e28) v2)))
[all …]
|
| H A D | 0012.smt2 | 15 (let ((e9 ((_ sign_extend 0) v2)))
22 (let ((e16 (bvxnor e9 ((_ sign_extend 1) v0))))
23 (let ((e17 (bvnor e8 ((_ sign_extend 5) e9))))
29 (let ((e23 (bvand e16 ((_ sign_extend 7) e7))))
33 (let ((e27 ((_ sign_extend 7) e7)))
41 (let ((e35 (bvsub e17 ((_ sign_extend 4) e4))))
48 (let ((e42 (bvshl e32 ((_ sign_extend 6) e19))))
59 (let ((e53 ((_ sign_extend 8) e27)))
86 (let ((e80 ((_ sign_extend 12) e20)))
114 (let ((e108 (= e18 ((_ sign_extend 7) e20))))
[all …]
|
| H A D | 0007.smt2 | 14 (let ((e8 ((_ sign_extend 6) v1)))
18 (let ((e12 (bvudiv ((_ sign_extend 10) e6) e11)))
24 (let ((e18 (bvxnor ((_ sign_extend 9) e6) e15)))
28 (let ((e22 ((_ sign_extend 0) e7)))
34 (let ((e28 (bvand e21 ((_ sign_extend 8) e22))))
35 (let ((e29 ((_ sign_extend 3) e10)))
37 (let ((e31 (bvxor e21 ((_ sign_extend 2) v3))))
41 (let ((e35 (bvlshr v3 ((_ sign_extend 6) e13))))
52 (let ((e46 (bvor v4 ((_ sign_extend 4) e13))))
57 (let ((e51 (bvxor ((_ sign_extend 1) v1) e43)))
[all …]
|
| H A D | 0032.smt2 | 25 (let ((e19 (bvudiv ((_ sign_extend 42) e11) e6)))
29 (let ((e23 (bvcomp e7 ((_ sign_extend 90) e16))))
31 (let ((e25 (bvmul e10 ((_ sign_extend 42) e24))))
37 (let ((e31 (bvxnor ((_ sign_extend 78) e22) e3)))
41 (let ((e35 (bvashr ((_ sign_extend 49) v2) e27)))
42 (let ((e36 (bvashr ((_ sign_extend 11) e5) e35)))
46 (let ((e40 (bvxor ((_ sign_extend 91) e9) e27)))
67 (let ((e61 (bvmul e6 ((_ sign_extend 42) e44))))
70 (let ((e64 (bvsdiv ((_ sign_extend 78) e8) e3)))
75 (let ((e69 (bvugt ((_ sign_extend 1) e65) e46)))
[all …]
|
| H A D | 0035.smt2 | 17 (let ((e8 (ite (p0 ((_ sign_extend 33) e5) ((_ sign_extend 76) e4) ((_ extract 66 1) v2)) (_ bv1 1)…
18 (let ((e9 (bvor ((_ sign_extend 105) e8) v2)))
27 (let ((e18 ((_ sign_extend 2) e11)))
39 (let ((e30 ((_ sign_extend 48) e16)))
51 (let ((e42 (ite (p0 ((_ extract 51 7) e35) ((_ sign_extend 100) e36) ((_ sign_extend 1) e13)) (_ bv…
52 (let ((e43 ((_ sign_extend 96) e27)))
84 (let ((e75 ((_ sign_extend 19) e65)))
113 (let ((e104 (p0 ((_ sign_extend 44) e22) ((_ sign_extend 52) e30) ((_ zero_extend 65) e91))))
165 (let ((e156 (p0 ((_ sign_extend 44) e59) ((_ sign_extend 76) e26) ((_ extract 96 31) e62))))
209 (let ((e200 (p0 ((_ extract 90 46) e49) ((_ sign_extend 100) e59) ((_ sign_extend 65) e95))))
[all …]
|
| H A D | 0006.smt2 | 18 (let ((e12 ((_ sign_extend 2) v1)))
22 (let ((e16 (bvurem ((_ sign_extend 3) e9) e6)))
26 (let ((e20 (select e18 ((_ sign_extend 7) e19))))
33 (let ((e27 (bvsub ((_ sign_extend 1) e10) e5)))
55 (let ((e49 (bvult ((_ sign_extend 3) e41) e6)))
64 (let ((e58 (= ((_ sign_extend 14) e34) e47)))
66 (let ((e60 (bvsgt e28 ((_ sign_extend 2) e9))))
88 (let ((e82 (bvuge e5 ((_ sign_extend 1) e8))))
95 (let ((e89 (= e22 ((_ sign_extend 1) e13))))
114 (let ((e108 (= v2 ((_ sign_extend 14) e25))))
[all …]
|
| /dports/math/cvc4/CVC4-1.7/test/regress/regress1/bv/ |
| H A D | fuzz34.smt | 17 (let (?e12 (sign_extend[2] ?e6))
42 (let (?e37 (sign_extend[0] v1))
46 (let (?e41 (sign_extend[0] ?e37))
89 (let (?e84 (sign_extend[1] ?e14))
128 (let (?e123 (sign_extend[2] ?e86))
131 (let (?e126 (sign_extend[3] ?e81))
206 (let (?e201 (sign_extend[3] ?e13))
305 (let (?e300 (sign_extend[0] ?e2))
306 (let (?e301 (sign_extend[3] ?e75))
359 (let (?e354 (sign_extend[0] ?e57))
[all …]
|
| H A D | bv-proof00.smt | 17 (let (?e12 (bvsub (sign_extend[6] ?e10) v2))
21 (let (?e16 (bvcomp ?e4 (sign_extend[1] ?e5)))
24 (let (?e19 (bvadd (sign_extend[4] ?e5) ?e12))
53 (let (?e48 (sign_extend[7] ?e43))
57 (let (?e52 (sign_extend[1] ?e20))
136 (let (?e131 (sign_extend[1] ?e71))
140 (let (?e135 (sign_extend[6] ?e102))
151 (let (?e146 (sign_extend[0] ?e140))
170 (let (?e165 (sign_extend[1] ?e156))
206 (let (?e201 (sign_extend[0] ?e157))
[all …]
|
| /dports/math/stp/stp-2.3.3/tests/query-files/sample-smt-tests/ |
| H A D | tmp.m8W1FfWP7L.smt2 | 24 (let ((e733896 (bvashr ((_ sign_extend 3) e733889) e733886)))
30 (let ((e733902 (bvudiv ((_ sign_extend 10) e733895) v733885)))
31 (let ((e733903 (bvxor v733881 ((_ sign_extend 2) v733884))))
37 (let ((e733909 (bvadd ((_ sign_extend 13) e733904) e733908)))
42 (let ((e733914 (bvadd ((_ sign_extend 9) e733907) v733884)))
66 (let ((e733938 (= e733908 ((_ sign_extend 3) e733890))))
71 (let ((e733943 (= e733902 ((_ sign_extend 10) v733882))))
74 (let ((e733946 (= ((_ sign_extend 13) e733898) e733908)))
97 (let ((e733969 (= ((_ sign_extend 1) e733913) e733912)))
107 (let ((e733979 (= ((_ sign_extend 9) e733918) e733914)))
[all …]
|
| H A D | tmp.liyo9rgPx3.smt2 | 15 (let ((e1109390 (bvxnor v1109385 ((_ sign_extend 1) v1109384))))
28 (let ((e1109403 (bvurem ((_ sign_extend 5) e1109400) v1109386)))
32 (let ((e1109407 (bvsmod ((_ sign_extend 5) v1109385) e1109402)))
34 (let ((e1109409 (bvsrem ((_ sign_extend 6) e1109388) e1109398)))
74 (let ((e1109449 (= e1109409 ((_ sign_extend 10) e1109399))))
109 (let ((e1109484 (= ((_ sign_extend 5) e1109400) e1109392)))
141 (let ((e1109516 (= ((_ sign_extend 10) e1109423) e1109390)))
151 (let ((e1109526 (= e1109432 ((_ sign_extend 11) e1109435))))
153 (let ((e1109528 (= ((_ sign_extend 6) e1109410) e1109396)))
219 (let ((e1109594 (= ((_ sign_extend 6) e1109388) e1109391)))
[all …]
|