/dports/math/cvc4/CVC4-1.7/test/regress/regress0/bv/ |
H A D | fuzz15.smt | 53 (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 D | fuzz17.smt | 135 (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 D | fuzz16.smt | 59 (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 D | fuzz26.smt | 30 (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 D | incorrect1.smt | 9 (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 D | fuzz09.smt | 26 (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 D | fuzz05.smt | 10 (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 D | fuzz07.smt | 18 (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 D | write-raw.smt2 | 134 (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 D | fuzz02.smt | 31 (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 D | fuzz03.smt | 23 (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 D | fuzz01.smt | 23 (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 D | fuzz09.smt | 13 (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 D | fuzz08.smt | 14 (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 D | fuzz00.smt | 29 (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 D | aufbv-fuzz01.smt | 26 (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 D | tmp.FKuQABT1Bf.smt2 | 18 (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 D | 0007.smt2 | 17 (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 D | 0035.smt2 | 16 (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 D | 0032.smt2 | 13 (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 D | fuzz34.smt | 10 (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 D | alu-zext.md | 54 (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 D | alu-zext.md | 54 (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 D | alu-zext.md | 54 (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 D | alu-zext.md | 54 (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 …]
|