diff --git a/tests/bench/bv_decide_rewriter.lean b/tests/bench/bv_decide_rewriter.lean new file mode 100644 index 0000000000..c921dc5bc3 --- /dev/null +++ b/tests/bench/bv_decide_rewriter.lean @@ -0,0 +1,1674 @@ +import Std.Tactic.BVDecide + +/-! +This benchmark is extracted from SMT-LIB problem `QF_BV/sage/app7/bench_6129.smt2` and is meant to +exercise the rewriting engine of bv_decide. It takes about one second to elaborate and another +second to solve at the time of adding this. Bitwuzla is capable of solving it in 0.006 seconds on +the same machine that these numbers were measured on. +-/ + +set_option maxRecDepth 2048 in +example: +∀ (T1_114127 T1_114128 T1_114129 : BitVec 8), + (!have v_3 := BitVec.setWidth 32 1#8; + have v_2 := BitVec.setWidth 32 2#8; + have v_0 := BitVec.setWidth 32 T1_114127 - 48#32; + have v_1 := BitVec.setWidth 32 T1_114128 + (v_0 + v_0 <<< v_2) <<< v_3 - 48#32; + have v_4 := BitVec.setWidth 32 T1_114129 + (v_1 + v_1 <<< v_2) <<< v_3; + have v_215 := v_4 - 49#32; + have v_214 := v_4 - 48#32; + have v_213 := v_214 * 4#32; + have v_212 := v_213 + 15#32 &&& 4294967288#32; + have v_111 := BitVec.setWidth 32 3#8; + have v_83 := v_212.sshiftRight' v_111; + have v_211 := v_83.sshiftRight' (BitVec.setWidth 32 5#8); + have v_210 := 64#32 - v_83; + have v_5 := 233#32 - v_83; + have v_206 := v_83 <<< v_111; + have v_209 := v_206 + 41810080#32; + have v_115 := BitVec.setWidth 32 32010#16; + have v_6 := BitVec.extractLsb' 8 8 v_5; + have v_7 := BitVec.extractLsb' 0 8 v_5; + have v_121 := BitVec.setWidth 32 v_7 + BitVec.setWidth 32 v_6 <<< 8#32; + have v_122 := BitVec.extractLsb' 0 16 (v_121 ^^^ v_115); + have v_127 := + 41811936#32 - + (BitVec.setWidth 32 (BitVec.extractLsb' 0 8 v_122) + + BitVec.setWidth 32 (BitVec.extractLsb' 8 8 v_122) <<< 8#32 ^^^ + 32010#32) <<< + v_111; + have v_208 := v_127 + 8#32; + have v_130 := BitVec.setWidth 32 16#8; + have v_207 := (v_206 + 105392#32).sshiftRight' v_130 + v_3; + have v_205 := (v_206 + 194712#32).sshiftRight' v_130 + v_3; + have v_188 := v_121 + BitVec.setWidth 32 (v_6 ^^^ v_7 ^^^ 0#8) <<< 24#32 ^^^ 1117097792#32; + have v_84 := v_188 ^^^ 1117097792#32; + have v_129 := v_127 &&& 4294901760#32; + have v_204 := v_129 - v_205 <<< v_130 + 65536#32; + have v_8 := v_84 + 1024#32; + have v_203 := v_127 + 521#32; + have v_125 := v_127 + 770#32; + have v_199 := v_127 + 778#32; + have v_198 := BitVec.extractLsb' 16 8 v_84; + have v_191 := (v_127 - v_204).sshiftRight' v_130 + v_3; + have v_202 := v_129 - v_191 <<< v_130 + 65536#32; + have v_128 := v_127 + 513#32; + have v_187 := (v_128 - v_202).sshiftRight' v_130 + v_3; + have v_201 := (v_128 &&& 4294901760#32) - v_187 <<< v_130 + 65536#32; + have v_200 := v_125 + 1040#32; + have v_123 := v_125 + 1057#32; + have v_194 := v_125 + 1065#32; + have v_186 := (v_125 - v_201).sshiftRight' v_130 + v_3; + have v_184 := (v_125 &&& 4294901760#32) - v_186 <<< v_130 + 65536#32; + have v_10 := BitVec.extractLsb' 0 8 v_8; + have v_9 := BitVec.extractLsb' 8 8 v_8; + have v_192 := BitVec.setWidth 32 v_10 + BitVec.setWidth 32 v_9 <<< 8#32; + have v_85 := v_192 + BitVec.setWidth 32 (v_9 ^^^ 0#8 ^^^ v_10) <<< 24#32 ^^^ 1117097792#32 ^^^ 1117097792#32; + have v_126 := v_125 + 1032#32; + have v_179 := (v_126 - v_184).sshiftRight' v_130 + v_3; + have v_197 := (v_126 &&& 4294901760#32) - v_179 <<< v_130 + 65536#32; + have v_196 := v_123 + 528#32; + have v_195 := v_123 + 553#32; + have v_11 := v_85 - 513#32; + have v_13 := BitVec.extractLsb' 0 8 v_11; + have v_12 := BitVec.extractLsb' 8 8 v_11; + have v_173 := + BitVec.setWidth 32 v_13 + BitVec.setWidth 32 v_12 <<< 8#32 + + BitVec.setWidth 32 (v_12 ^^^ v_13 ^^^ 0#8) <<< 24#32 ^^^ + 1117097792#32; + have v_86 := v_173 ^^^ 1117097792#32; + have v_14 := v_86 - 257#32; + have v_16 := BitVec.extractLsb' 0 8 v_14; + have v_15 := BitVec.extractLsb' 8 8 v_14; + have v_153 := + BitVec.setWidth 32 v_16 + BitVec.setWidth 32 v_15 <<< 8#32 + + BitVec.setWidth 32 (v_15 ^^^ v_16 ^^^ 0#8) <<< 24#32 ^^^ + 1117097792#32; + have v_87 := v_153 ^^^ 1117097792#32; + have v_17 := v_87 - 33#32; + have v_19 := BitVec.extractLsb' 0 8 v_17; + have v_18 := BitVec.extractLsb' 8 8 v_17; + have v_138 := + BitVec.setWidth 32 v_19 + BitVec.setWidth 32 v_18 <<< 8#32 + + BitVec.setWidth 32 (v_18 ^^^ v_19 ^^^ 0#8) <<< 24#32 ^^^ + 1117097792#32; + have v_88 := v_138 ^^^ 1117097792#32; + have v_20 := v_88 - 32#32; + have v_22 := BitVec.extractLsb' 0 8 v_20; + have v_21 := BitVec.extractLsb' 8 8 v_20; + have v_89 := + BitVec.setWidth 32 v_22 + BitVec.setWidth 32 v_21 <<< 8#32 + + BitVec.setWidth 32 (v_21 ^^^ v_22 ^^^ 0#8) <<< 24#32 ^^^ + 1117097792#32 ^^^ + 1117097792#32; + have v_23 := v_89 - 64#32; + have v_25 := BitVec.extractLsb' 0 8 v_23; + have v_24 := BitVec.extractLsb' 8 8 v_23; + have v_82 := + BitVec.setWidth 32 v_25 + BitVec.setWidth 32 v_24 <<< 8#32 + + BitVec.setWidth 32 (v_24 ^^^ v_25 ^^^ 0#8) <<< 24#32 ^^^ + 1117097792#32; + have v_81 := v_82 ^^^ 1117097792#32; + have v_26 := v_81 - 25#32; + have v_28 := BitVec.extractLsb' 0 8 v_26; + have v_27 := BitVec.extractLsb' 8 8 v_26; + have v_71 := + BitVec.setWidth 32 v_28 + BitVec.setWidth 32 v_27 <<< 8#32 + + BitVec.setWidth 32 (v_27 ^^^ v_28 ^^^ 0#8) <<< 24#32 ^^^ + 1117097792#32; + have v_70 := v_71 ^^^ 1117097792#32; + have v_29 := v_70 - 33#32; + have v_31 := BitVec.extractLsb' 0 8 v_29; + have v_30 := BitVec.extractLsb' 8 8 v_29; + have v_105 := + BitVec.setWidth 32 v_31 + BitVec.setWidth 32 v_30 <<< 8#32 + + BitVec.setWidth 32 (v_30 ^^^ v_31 ^^^ 0#8) <<< 24#32 ^^^ + 1117097792#32; + have v_94 := v_105 ^^^ 1117097792#32; + have v_32 := v_94 - 32#32; + have v_34 := BitVec.extractLsb' 0 8 v_32; + have v_33 := BitVec.extractLsb' 8 8 v_32; + have v_135 := + BitVec.setWidth 32 v_34 + BitVec.setWidth 32 v_33 <<< 8#32 + + BitVec.setWidth 32 (v_33 ^^^ v_34 ^^^ 0#8) <<< 24#32 ^^^ + 1117097792#32; + have v_95 := v_135 ^^^ 1117097792#32; + have v_35 := v_95 - 25#32; + have v_36 := BitVec.extractLsb' 8 8 v_35; + have v_37 := BitVec.extractLsb' 0 8 v_35; + have v_114 := BitVec.setWidth 32 v_37 + BitVec.setWidth 32 v_36 <<< 8#32; + have v_116 := BitVec.extractLsb' 0 16 (v_114 ^^^ v_115); + have v_119 := + 41820128#32 - + (BitVec.setWidth 32 (BitVec.extractLsb' 0 8 v_116) + + BitVec.setWidth 32 (BitVec.extractLsb' 8 8 v_116) <<< 8#32 ^^^ + 32010#32) <<< + v_111; + have v_168 := v_119 + 8#32; + have v_178 := (v_123 - v_197).sshiftRight' v_130 + v_3; + have v_181 := (v_123 &&& 4294901760#32) - v_178 <<< v_130 + 65536#32; + have v_193 := BitVec.extractLsb' 16 8 v_85; + have v_158 := BitVec.setWidth 32 0#16; + have v_124 := v_123 + 520#32; + have v_172 := (v_124 - v_181).sshiftRight' v_130 + v_3; + have v_190 := (v_124 &&& 4294901760#32) - v_172 <<< v_130 + 65536#32; + have v_189 := (v_127 + 803#32 - v_184).sshiftRight' v_130 + v_3; + have v_185 := (v_125 + 520#32 - v_184).sshiftRight' v_130 + v_3; + have v_176 := v_168 + 24#32; + have v_169 := v_119 + 1032#32; + have v_183 := v_168 + 16#32; + have v_182 := (v_125 + 1090#32 - v_181).sshiftRight' v_130 + v_3; + have v_180 := BitVec.extractLsb' 16 8 v_86; + have v_171 := (v_123 + 545#32 - v_190).sshiftRight' v_130 + v_3; + have v_120 := v_119 &&& 4294901760#32; + have v_177 := v_120 - v_171 <<< v_130 + 65536#32; + have v_142 := v_114 + BitVec.setWidth 32 (v_36 ^^^ v_37 ^^^ 0#8) <<< 24#32 ^^^ 1117097792#32; + have v_96 := v_142 ^^^ 1117097792#32; + have v_38 := v_96 + 1024#32; + have v_118 := v_119 + 1024#32; + have v_167 := + (v_119 + 24#32).sshiftRight' v_111 ^^^ 1296737859#32 ^^^ 39452672#32 ^^^ 41703576#32 ^^^ + v_183.sshiftRight' v_111 ^^^ + 1296737859#32 ^^^ + 39452672#32; + have v_175 := + 200#32 - + (BitVec.setWidth 32 (BitVec.extractLsb' 16 8 v_167) <<< 16#32 + + BitVec.setWidth 32 (BitVec.extractLsb' 24 8 v_167) <<< 24#32 &&& + 63#32); + have v_174 := v_210 + 155#32 + v_5 - 77#32 - v_84 + v_8 - v_85 + v_11 - v_86 + v_14; + have v_161 := (v_119 - v_177).sshiftRight' v_130 + v_3; + have v_170 := v_120 - v_161 <<< v_130 + 65536#32; + have v_117 := v_118 + 776#32; + have v_164 := v_118 + 784#32; + have v_40 := BitVec.extractLsb' 0 8 v_38; + have v_39 := BitVec.extractLsb' 8 8 v_38; + have v_157 := BitVec.setWidth 32 v_40 + BitVec.setWidth 32 v_39 <<< 8#32; + have v_97 := v_157 + BitVec.setWidth 32 (v_39 ^^^ 0#8 ^^^ v_40) <<< 24#32 ^^^ 1117097792#32 ^^^ 1117097792#32; + have v_41 := v_97 - 1024#32; + have v_43 := BitVec.extractLsb' 0 8 v_41; + have v_42 := BitVec.extractLsb' 8 8 v_41; + have v_134 := + BitVec.setWidth 32 v_43 + BitVec.setWidth 32 v_42 <<< 8#32 + + BitVec.setWidth 32 (v_42 ^^^ v_43 ^^^ 0#8) <<< 24#32 ^^^ + 1117097792#32; + have v_98 := v_134 ^^^ 1117097792#32; + have v_44 := v_98 - 49#32; + have v_46 := BitVec.extractLsb' 0 8 v_44; + have v_45 := BitVec.extractLsb' 8 8 v_44; + have v_99 := + BitVec.setWidth 32 v_46 + BitVec.setWidth 32 v_45 <<< 8#32 + + BitVec.setWidth 32 (v_45 ^^^ v_46 ^^^ 0#8) <<< 24#32 ^^^ + 1117097792#32 ^^^ + 1117097792#32; + have v_47 := v_99 - 48#32; + have v_49 := BitVec.extractLsb' 0 8 v_47; + have v_48 := BitVec.extractLsb' 8 8 v_47; + have v_69 := + BitVec.setWidth 32 v_49 + BitVec.setWidth 32 v_48 <<< 8#32 + + BitVec.setWidth 32 (v_48 ^^^ v_49 ^^^ 0#8) <<< 24#32 ^^^ + 1117097792#32; + have v_68 := v_69 ^^^ 1117097792#32; + have v_50 := v_68 - 33#32; + have v_52 := BitVec.extractLsb' 0 8 v_50; + have v_51 := BitVec.extractLsb' 8 8 v_50; + have v_74 := + BitVec.setWidth 32 v_52 + BitVec.setWidth 32 v_51 <<< 8#32 + + BitVec.setWidth 32 (v_51 ^^^ v_52 ^^^ 0#8) <<< 24#32 ^^^ + 1117097792#32; + have v_72 := v_74 ^^^ 1117097792#32; + have v_53 := v_72 - 32#32; + have v_54 := BitVec.extractLsb' 8 8 v_53; + have v_55 := BitVec.extractLsb' 0 8 v_53; + have v_109 := BitVec.setWidth 32 v_55 + BitVec.setWidth 32 v_54 <<< 8#32; + have v_110 := BitVec.extractLsb' 0 16 (v_109 ^^^ v_115); + have v_112 := + 41828320#32 - + (BitVec.setWidth 32 (BitVec.extractLsb' 0 8 v_110) + + BitVec.setWidth 32 (BitVec.extractLsb' 8 8 v_110) <<< 8#32 ^^^ + 32010#32) <<< + v_111; + have v_165 := v_112 + 8#32; + have v_149 := (v_118 - v_170).sshiftRight' v_130 + v_3; + have v_155 := (v_118 &&& 4294901760#32) - v_149 <<< v_130 + 65536#32; + have v_166 := v_117 + 528#32; + have v_144 := (v_117 - v_155).sshiftRight' v_130 + v_3; + have v_145 := (v_117 &&& 4294901760#32) - v_144 <<< v_130 + 65536#32; + have v_163 := 20#32 - v_87; + have v_162 := BitVec.extractLsb' 16 8 v_87; + have v_160 := 20#32 - v_96; + have v_159 := 41#32 - v_96; + have v_152 := BitVec.extractLsb' 16 8 v_96; + have v_156 := (v_119 + 1073#32 - v_155).sshiftRight' v_130 + v_3; + have v_154 := v_174 - 9#32 - v_87 + v_17 + 17#32; + have v_93 := v_154 - v_88 + v_20 - v_89 + v_23 - v_81 + v_26; + have v_136 := v_93 - 17#32 - v_70 + v_29 + 17#32; + have v_151 := v_136 - v_94 + v_32 - v_95 + v_35; + have v_150 := BitVec.extractLsb' 16 8 v_97; + have v_139 := (v_117 + 520#32 - v_145).sshiftRight' v_130 + v_3; + have v_113 := v_112 &&& 4294901760#32; + have v_148 := v_113 - v_139 <<< v_130 + 65536#32; + have v_56 := v_109 + BitVec.setWidth 32 (v_54 ^^^ v_55 ^^^ 0#8) <<< 24#32 ^^^ 1117097792#32 ^^^ 1117097792#32; + have v_59 := BitVec.extractLsb' 0 8 v_56; + have v_58 := BitVec.extractLsb' 16 8 v_56; + have v_57 := BitVec.extractLsb' 8 8 v_56; + have v_90 := + BitVec.setWidth 32 v_59 + BitVec.setWidth 32 v_57 <<< 8#32 + BitVec.setWidth 32 v_58 <<< 16#32 + + BitVec.setWidth 32 (v_57 ^^^ v_58 ^^^ v_59) <<< 24#32 ^^^ + 1117097792#32; + have v_100 := v_90 ^^^ 1117097792#32; + have v_60 := v_100 + 512#32; + have v_147 := v_112 + 137#32; + have v_146 := (v_118 + 809#32 - v_145).sshiftRight' v_130 + v_3; + have v_133 := (v_112 - v_148).sshiftRight' v_130 + v_3; + have v_143 := v_113 - v_133 <<< v_130 + 65536#32; + have v_137 := BitVec.extractLsb' 16 8 v_88; + have v_141 := BitVec.extractLsb' 16 8 v_95; + have v_140 := BitVec.extractLsb' 16 8 v_98; + have v_108 := BitVec.extractLsb' 16 8 v_100; + have v_61 := BitVec.extractLsb' 8 8 v_60; + have v_62 := BitVec.extractLsb' 0 8 v_60; + have v_132 := BitVec.setWidth 32 v_62 + BitVec.setWidth 32 v_61 <<< 8#32; + have v_92 := v_132 + BitVec.setWidth 32 (v_61 ^^^ 0#8 ^^^ v_62) <<< 24#32 ^^^ 1117097792#32 ^^^ 1117097792#32; + have v_131 := (v_112 + 129#32 - v_143).sshiftRight' v_130 + v_3; + have v_106 := BitVec.extractLsb' 16 8 v_89; + have v_104 := BitVec.extractLsb' 16 8 v_94; + have v_102 := BitVec.extractLsb' 16 8 v_99; + have v_63 := v_92 - 129#32; + have v_107 := BitVec.extractLsb' 16 8 v_92; + have v_103 := v_151 - v_96 + v_38 - v_97 + v_41 - v_98 + v_44 - v_99 + v_47; + have v_101 := v_103 - 17#32 - v_68 + v_50 + 17#32; + have v_91 := BitVec.extractLsb' 16 8 v_81; + have v_73 := BitVec.extractLsb' 16 8 v_72; + have v_80 := 20#32 - v_70; + have v_79 := 41#32 - v_70; + have v_78 := BitVec.extractLsb' 16 8 v_70; + have v_77 := 20#32 - v_68; + have v_76 := 41#32 - v_68; + have v_75 := BitVec.extractLsb' 16 8 v_68; + have v_65 := BitVec.extractLsb' 0 8 v_63; + have v_64 := BitVec.extractLsb' 8 8 v_63; + have v_66 := + BitVec.setWidth 32 v_65 + BitVec.setWidth 32 v_64 <<< 8#32 + + BitVec.setWidth 32 (v_64 ^^^ v_65 ^^^ 0#8) <<< 24#32 ^^^ + 1117097792#32; + have v_67 := v_66 ^^^ 1117097792#32; + true && 5#32 == v_215 && (65#32 - v_67).sle 0#32 && !1048576#32 &&& v_66 == 0#32 && (65#32).ule v_67 && + !v_66 &&& + 1048576#32 == + 0#32 && + (v_56 + + 65#32).ult + 129#32 && + v_58 &&& + 1#8 == + 0#8 && + BitVec.extractLsb' + 24 + 8 + v_56 == + v_58 ^^^ + v_57 ^^^ + v_59 && + v_75 &&& + 8#8 == + 0#8 && + !1048576#32 &&& + v_69 == + 0#32 && + !v_69 &&& + 1048576#32 == + 0#32 && + v_78 &&& + 8#8 == + 0#8 && + !1048576#32 &&& + v_71 == + 0#32 && + !v_71 &&& + 1048576#32 == + 0#32 && + v_73 &&& + 4#8 == + 0#8 && + v_73 &&& + 8#8 == + 0#8 && + v_73 &&& + 1#8 == + 0#8 && + !v_74 &&& + 1048576#32 == + 0#32 && + (0#32).slt + (v_68 - + 53#32) && + BitVec.extractLsb' + 24 + 8 + v_68 == + v_75 ^^^ + BitVec.extractLsb' + 8 + 8 + v_68 ^^^ + BitVec.extractLsb' + 0 + 8 + v_68 && + (33#32 - + v_68).sle + 0#32 && + !v_76 == + 0#32 && + v_76.sle + 0#32 && + v_77.sle + 0#32 && + !v_77 == + 0#32 && + !v_50 == + 127#32 && + v_50.ult + 128#32 && + !v_50 == + 1#32 && + !v_50 == + 0#32 && + (0#32).slt + (v_70 - + 53#32) && + BitVec.extractLsb' + 24 + 8 + v_70 == + v_78 ^^^ + BitVec.extractLsb' + 8 + 8 + v_70 ^^^ + BitVec.extractLsb' + 0 + 8 + v_70 && + (33#32 - + v_70).sle + 0#32 && + !v_79 == + 0#32 && + v_79.sle + 0#32 && + v_80.sle + 0#32 && + !v_80 == + 0#32 && + v_91 &&& + 8#8 == + 0#8 && + !v_82 &&& + 1048576#32 == + 0#32 && + (v_93 + + 44#32).ule + 8192#32 && + (0#32).slt + (v_72 - + 52#32) && + (65#32).ule + (v_72 + + 33#32) && + BitVec.extractLsb' + 24 + 8 + v_72 == + v_73 ^^^ + BitVec.extractLsb' + 8 + 8 + v_72 ^^^ + BitVec.extractLsb' + 0 + 8 + v_72 && + (17#32 - + v_72).sle + 0#32 && + (BitVec.extractLsb' + 16 + 8 + v_90 ^^^ + 1#8) &&& + 1#8 == + 0#8 && + !v_68 == + 127#32 && + v_68.ult + 128#32 && + (33#32).ule + v_68 && + (20#32).ule + v_68 && + (41#32).ule + v_68 && + v_70.ult + 2047#32 && + !v_70 == + 2047#32 && + v_70.ult + 2048#32 && + (128#32).ule + v_70 && + (33#32).ule + v_70 && + (20#32).ule + v_70 && + (41#32).ule + v_70 && + (0#32).slt + (v_81 - + 45#32) && + BitVec.extractLsb' + 24 + 8 + v_81 == + v_91 ^^^ + BitVec.extractLsb' + 8 + 8 + v_81 ^^^ + BitVec.extractLsb' + 0 + 8 + v_81 && + (25#32 - + v_81).sle + 0#32 && + !v_26 == + 2047#32 && + v_26.ult + 2048#32 && + (128#32).ule + v_26 && + !v_26 == + 1#32 && + !v_26 == + 0#32 && + v_107 &&& + 8#8 == + 0#8 && + (v_101 - + v_72 + + v_53 - + v_100 + + v_60 - + v_92 + + v_63 + + 109#32).ule + 8192#32 && + !v_72 == + 127#32 && + v_72.ult + 128#32 && + v_101.ule + 8192#32 && + v_102 &&& + 4#8 == + 0#8 && + v_102 &&& + 8#8 == + 0#8 && + v_102 &&& + 1#8 == + 0#8 && + (v_103 + + 44#32).ule + 8192#32 && + v_104 &&& + 4#8 == + 0#8 && + v_104 &&& + 8#8 == + 0#8 && + v_104 &&& + 1#8 == + 0#8 && + !v_105 &&& + 1048576#32 == + 0#32 && + !v_29 == + 2047#32 && + v_29.ult + 2048#32 && + (128#32).ule + v_29 && + !v_29 == + 1#32 && + !v_29 == + 0#32 && + v_106 &&& + 4#8 == + 0#8 && + v_106 &&& + 8#8 == + 0#8 && + v_106 &&& + 1#8 == + 0#8 && + v_81.ult + 2047#32 && + !v_81 == + 2047#32 && + v_81.ult + 2048#32 && + (128#32).ule + v_81 && + (25#32).ule + v_81 && + (0#32).slt + (v_92 - + 149#32) && + BitVec.extractLsb' + 24 + 8 + v_92 == + v_107 ^^^ + BitVec.extractLsb' + 8 + 8 + v_92 ^^^ + BitVec.extractLsb' + 0 + 8 + v_92 && + !v_63 == + 2047#32 && + v_63.ult + 2048#32 && + (128#32).ule + v_63 && + !v_63 == + 1#32 && + !v_63 == + 0#32 && + !v_53 == + 127#32 && + v_53.ult + 128#32 && + !v_53 == + 0#32 && + (2#32).ult + v_53 && + v_108 &&& + 4#8 == + 0#8 && + v_108 &&& + 8#8 == + 0#8 && + !v_90 &&& + 1048576#32 == + 0#32 && + (0#32).slt + (v_99 - + 68#32) && + (97#32).ule + (v_99 + + 49#32) && + BitVec.extractLsb' + 24 + 8 + v_99 == + v_102 ^^^ + BitVec.extractLsb' + 8 + 8 + v_99 ^^^ + BitVec.extractLsb' + 0 + 8 + v_99 && + !v_47 == + 127#32 && + v_47.ult + 128#32 && + !v_47 == + 0#32 && + (2#32).ult + v_47 && + (0#32).slt + (v_94 - + 52#32) && + (65#32).ule + (v_94 + + 33#32) && + BitVec.extractLsb' + 24 + 8 + v_94 == + v_104 ^^^ + BitVec.extractLsb' + 8 + 8 + v_94 ^^^ + BitVec.extractLsb' + 0 + 8 + v_94 && + (17#32 - + v_94).sle + 0#32 && + (0#32).slt + (v_89 - + 84#32) && + (129#32).ule + (v_89 + + 65#32) && + BitVec.extractLsb' + 24 + 8 + v_89 == + v_106 ^^^ + BitVec.extractLsb' + 8 + 8 + v_89 ^^^ + BitVec.extractLsb' + 0 + 8 + v_89 && + !v_23 == + 2047#32 && + v_23.ult + 2048#32 && + (128#32).ule + v_23 && + !v_23 == + 0#32 && + (2#32).ult + v_23 && + v_131.slt + 254#32 && + (0#32).slt + v_131 && + v_92.ult + 2047#32 && + !v_92 == + 2047#32 && + v_92.ult + 2048#32 && + (128#32).ule + v_92 && + !v_132 == + v_158 && + (0#32).slt + (v_100 + + 492#32) && + BitVec.extractLsb' + 24 + 8 + v_100 == + BitVec.extractLsb' + 8 + 8 + v_100 ^^^ + BitVec.extractLsb' + 0 + 8 + v_100 ^^^ + v_108 && + (0#32).slt + (129#32 - + v_100) && + !BitVec.extractLsb' + 0 + 8 + v_133 == + 0#8 && + v_140 &&& + 8#8 == + 0#8 && + !v_134 &&& + 1048576#32 == + 0#32 && + v_99.ult + 2047#32 && + !v_99 == + 2047#32 && + v_99.ult + 2048#32 && + (128#32).ule + v_99 && + v_141 &&& + 8#8 == + 0#8 && + !v_135 &&& + 1048576#32 == + 0#32 && + v_94.ult + 2047#32 && + !v_94 == + 2047#32 && + v_94.ult + 2048#32 && + (128#32).ule + v_94 && + v_136.ule + 8192#32 && + v_137 &&& + 4#8 == + 0#8 && + v_137 &&& + 8#8 == + 0#8 && + v_137 &&& + 1#8 == + 0#8 && + !v_138 &&& + 1048576#32 == + 0#32 && + v_89.ult + 2047#32 && + !v_89 == + 2047#32 && + v_89.ult + 2048#32 && + (128#32).ule + v_89 && + !v_100 == + 127#32 && + v_100.ult + 128#32 && + v_133.slt + 254#32 && + (0#32).slt + v_133 && + !BitVec.extractLsb' + 0 + 8 + v_139 == + 0#8 && + (0#32).slt + (v_98 - + 69#32) && + BitVec.extractLsb' + 24 + 8 + v_98 == + v_140 ^^^ + BitVec.extractLsb' + 8 + 8 + v_98 ^^^ + BitVec.extractLsb' + 0 + 8 + v_98 && + (49#32 - + v_98).sle + 0#32 && + !v_44 == + 2047#32 && + v_44.ult + 2048#32 && + (128#32).ule + v_44 && + !v_44 == + 1#32 && + !v_44 == + 0#32 && + (0#32).slt + (v_95 - + 45#32) && + BitVec.extractLsb' + 24 + 8 + v_95 == + v_141 ^^^ + BitVec.extractLsb' + 8 + 8 + v_95 ^^^ + BitVec.extractLsb' + 0 + 8 + v_95 && + (25#32 - + v_95).sle + 0#32 && + !v_32 == + 2047#32 && + v_32.ult + 2048#32 && + (128#32).ule + v_32 && + !v_32 == + 0#32 && + (2#32).ult + v_32 && + (BitVec.extractLsb' + 16 + 8 + v_142 ^^^ + 1#8) &&& + 1#8 == + 0#8 && + (0#32).slt + (v_88 - + 52#32) && + (65#32).ule + (v_88 + + 33#32) && + BitVec.extractLsb' + 24 + 8 + v_88 == + v_137 ^^^ + BitVec.extractLsb' + 8 + 8 + v_88 ^^^ + BitVec.extractLsb' + 0 + 8 + v_88 && + (17#32 - + v_88).sle + 0#32 && + !v_20 == + 2047#32 && + v_20.ult + 2048#32 && + (128#32).ule + v_20 && + !v_20 == + 0#32 && + (2#32).ult + v_20 && + v_112 + + 0#32 &&& + 0#32 == + 0#32 && + !39452672#32 == + v_143 && + !v_60 == + 2047#32 && + v_60.ult + 2048#32 && + (128#32).ule + v_60 && + v_60.ule + 65024#32 && + !v_60 == + 0#32 && + v_139.slt + 254#32 && + (0#32).slt + v_139 && + !BitVec.extractLsb' + 0 + 8 + v_144 == + 0#8 && + v_150 &&& + 8#8 == + 0#8 && + v_98.ult + 2047#32 && + !v_98 == + 2047#32 && + v_98.ult + 2048#32 && + (128#32).ule + v_98 && + (49#32).ule + v_98 && + v_95.ult + 2047#32 && + !v_95 == + 2047#32 && + v_95.ult + 2048#32 && + (128#32).ule + v_95 && + (25#32).ule + v_95 && + v_88.ult + 2047#32 && + !v_88 == + 2047#32 && + v_88.ult + 2048#32 && + (128#32).ule + v_88 && + v_146.slt + 254#32 && + (0#32).slt + v_146 && + !v_147 == + 0#32 && + !39452868#32 == + v_147 && + (v_112 + + v_60 <<< + v_111).ult + 42663936#32 && + !39452672#32 == + v_148 && + v_144.slt + 254#32 && + (0#32).slt + v_144 && + !BitVec.extractLsb' + 0 + 8 + v_149 == + 0#8 && + (0#32).slt + (v_97 - + 1044#32) && + BitVec.extractLsb' + 24 + 8 + v_97 == + v_150 ^^^ + BitVec.extractLsb' + 8 + 8 + v_97 ^^^ + BitVec.extractLsb' + 0 + 8 + v_97 && + !v_41 == + 2047#32 && + v_41.ult + 2048#32 && + (128#32).ule + v_41 && + !v_41 == + 1#32 && + !v_41 == + 0#32 && + (v_151 + + 44#32).ule + 8192#32 && + !v_35 == + 2047#32 && + v_35.ult + 2048#32 && + (128#32).ule + v_35 && + !v_35 == + 1#32 && + !v_35 == + 0#32 && + v_152 &&& + 4#8 == + 0#8 && + v_152 &&& + 8#8 == + 0#8 && + !1048576#32 &&& + v_142 == + 0#32 && + !v_142 &&& + 1048576#32 == + 0#32 && + v_162 &&& + 8#8 == + 0#8 && + !1048576#32 &&& + v_153 == + 0#32 && + !v_153 &&& + 1048576#32 == + 0#32 && + v_154.ule + 8192#32 && + v_156.slt + 254#32 && + (0#32).slt + v_156 && + v_165 &&& + 3#32 == + 0#32 && + !v_112 == + 0#32 && + !v_112 == + 41828320#32 && + BitVec.extractLsb' + 0 + 8 + v_164 &&& + 7#8 == + 0#8 && + v_149.slt + 254#32 && + (0#32).slt + v_149 && + v_97.ult + 2047#32 && + !v_97 == + 2047#32 && + v_97.ult + 2048#32 && + (128#32).ule + v_97 && + !v_157 == + v_158 && + (0#32).slt + (v_96 + + 1004#32) && + BitVec.extractLsb' + 24 + 8 + v_96 == + BitVec.extractLsb' + 8 + 8 + v_96 ^^^ + BitVec.extractLsb' + 0 + 8 + v_96 ^^^ + v_152 && + (0#32).slt + (1024#32 - + v_96) && + (21#32 - + v_96).sle + 0#32 && + !v_159 == + 0#32 && + v_159.sle + 0#32 && + v_160.sle + 0#32 && + !v_160 == + 0#32 && + !BitVec.extractLsb' + 0 + 8 + v_161 == + 0#8 && + (0#32).slt + (v_87 - + 53#32) && + BitVec.extractLsb' + 24 + 8 + v_87 == + v_162 ^^^ + BitVec.extractLsb' + 8 + 8 + v_87 ^^^ + BitVec.extractLsb' + 0 + 8 + v_87 && + (33#32 - + v_87).sle + 0#32 && + !v_163 == + 0#32 && + v_163.sle + 0#32 && + !41#32 - + v_87 == + 0#32 && + (42#32 - + v_87).sle + 0#32 && + !v_17 == + 2047#32 && + v_17.ult + 2048#32 && + (128#32).ule + v_17 && + !v_17 == + 1#32 && + !v_17 == + 0#32 && + BitVec.extractLsb' + 0 + 8 + v_169 &&& + 7#8 == + 0#8 && + !39452672#32 == + v_145 && + (v_164 + + 512#32).ule + v_165 && + !v_165 == + 0#32 && + v_164 &&& + 3#32 == + 0#32 && + v_166 == + v_165 && + !39452868#32 == + v_166 && + v_117 &&& + 0#32 == + 0#32 && + v_96.ult + 2047#32 && + !v_96 == + 2047#32 && + v_96.ult + 2048#32 && + (128#32).ule + v_96 && + (20#32).ule + v_96 && + (41#32).ule + v_96 && + v_161.slt + 254#32 && + (0#32).slt + v_161 && + v_87.ult + 2047#32 && + !v_87 == + 2047#32 && + v_87.ult + 2048#32 && + (128#32).ule + v_87 && + (33#32).ule + v_87 && + (20#32).ule + v_87 && + (42#32).ule + v_87 && + (8#32).ule + (v_175.sshiftRight' + v_2) && + BitVec.extractLsb' + 0 + 8 + v_176 &&& + 7#8 == + 0#8 && + !39452672#32 == + v_155 && + v_169 &&& + 3#32 == + 0#32 && + !39452868#32 == + v_118 + + 817#32 && + v_164.ult + v_165 && + (41773216#32).ule + v_164 && + (41773088#32).ult + v_164 && + !v_164 == + 0#32 && + !v_164 == + 39452868#32 && + !39452868#32 == + v_164 && + !v_117 == + 0#32 && + !39452672#32 == + v_170 && + !v_38 == + 2047#32 && + v_38.ult + 2048#32 && + (128#32).ule + v_38 && + v_38.ule + 65024#32 && + !v_38 == + 0#32 && + !BitVec.extractLsb' + 0 + 8 + v_171 == + 0#8 && + !BitVec.extractLsb' + 0 + 8 + v_172 == + 0#8 && + v_180 &&& + 8#8 == + 0#8 && + !v_173 &&& + 1048576#32 == + 0#32 && + (v_174 + + 77#32).ule + 8192#32 && + v_175.ult + 384#32 && + v_175.ule + 384#32 && + (v_175 + + v_176).ule + v_169 && + !v_169 == + 0#32 && + !39452868#32 == + v_169 && + !v_118 == + 0#32 && + (v_119 + + v_38 <<< + v_111).ult + 42663936#32 && + !39452672#32 == + v_177 && + v_171.slt + 254#32 && + (0#32).slt + v_171 && + v_172.slt + 254#32 && + (0#32).slt + v_172 && + !BitVec.extractLsb' + 0 + 8 + v_178 == + 0#8 && + !BitVec.extractLsb' + 0 + 8 + v_179 == + 0#8 && + (0#32).slt + (v_86 - + 277#32) && + BitVec.extractLsb' + 24 + 8 + v_86 == + v_180 ^^^ + BitVec.extractLsb' + 8 + 8 + v_86 ^^^ + BitVec.extractLsb' + 0 + 8 + v_86 && + (257#32 - + v_86).sle + 0#32 && + !v_14 == + 2047#32 && + v_14.ult + 2048#32 && + (128#32).ule + v_14 && + !v_14 == + 1#32 && + !v_14 == + 0#32 && + v_182.slt + 254#32 && + (0#32).slt + v_182 && + !v_183 == + 0#32 && + v_176.ult + v_169 && + !v_176 == + 0#32 && + !v_119 == + 0#32 && + !v_119 == + 41820128#32 && + v_178.slt + 254#32 && + (0#32).slt + v_178 && + v_179.slt + 254#32 && + (0#32).slt + v_179 && + v_185.slt + 254#32 && + (0#32).slt + v_185 && + !BitVec.extractLsb' + 0 + 8 + v_186 == + 0#8 && + !BitVec.extractLsb' + 0 + 8 + v_187 == + 0#8 && + v_193 &&& + 8#8 == + 0#8 && + v_86.ult + 2047#32 && + !v_86 == + 2047#32 && + v_86.ult + 2048#32 && + (128#32).ule + v_86 && + (257#32).ule + v_86 && + (BitVec.extractLsb' + 16 + 8 + v_188 ^^^ + 1#8) &&& + 1#8 == + 0#8 && + v_189.slt + 254#32 && + (0#32).slt + v_189 && + BitVec.extractLsb' + 0 + 8 + v_194 &&& + 7#8 == + 0#8 && + v_195 &&& + 0#32 == + 0#32 && + !v_168 == + 0#32 && + !39452672#32 == + v_190 && + v_186.slt + 254#32 && + (0#32).slt + v_186 && + v_187.slt + 254#32 && + (0#32).slt + v_187 && + !BitVec.extractLsb' + 0 + 8 + v_191 == + 0#8 && + !v_192 == + v_158 && + (0#32).slt + (v_85 - + 533#32) && + BitVec.extractLsb' + 24 + 8 + v_85 == + v_193 ^^^ + BitVec.extractLsb' + 8 + 8 + v_85 ^^^ + BitVec.extractLsb' + 0 + 8 + v_85 && + !v_11 == + 2047#32 && + v_11.ult + 2048#32 && + (128#32).ule + v_11 && + !v_11 == + 1#32 && + !v_11 == + 0#32 && + BitVec.extractLsb' + 0 + 8 + v_199 &&& + 7#8 == + 0#8 && + !39452672#32 == + v_181 && + v_194 &&& + 3#32 == + 0#32 && + v_195 == + v_168 && + !v_195 == + 0#32 && + !v_195 == + 39452868#32 && + !39452868#32 == + v_195 && + !v_196 == + 0#32 && + !39452868#32 == + v_196 && + v_123 &&& + 0#32 == + 0#32 && + !39452672#32 == + v_197 && + v_191.slt + 254#32 && + (0#32).slt + v_191 && + v_198 &&& + 4#8 == + 0#8 && + v_198 &&& + 8#8 == + 0#8 && + v_85.ult + 2047#32 && + !v_85 == + 2047#32 && + v_85.ult + 2048#32 && + (128#32).ule + v_85 && + !1048576#32 &&& + v_188 == + 0#32 && + !v_188 &&& + 1048576#32 == + 0#32 && + !39452672#32 == + v_184 && + v_199 &&& + 3#32 == + 0#32 && + !39452868#32 == + v_125 + + 1098#32 && + (41773216#32).ule + v_194 && + (41773088#32).ult + v_194 && + !v_194 == + 0#32 && + !v_194 == + 39452868#32 && + !39452868#32 == + v_194 && + !v_123 == + 0#32 && + !v_200 == + 0#32 && + !39452868#32 == + v_200 && + v_125 &&& + 0#32 == + 0#32 && + !39452672#32 == + v_201 && + !39452672#32 == + v_202 && + (0#32).slt + (v_84 + + 1004#32) && + BitVec.extractLsb' + 24 + 8 + v_84 == + BitVec.extractLsb' + 8 + 8 + v_84 ^^^ + BitVec.extractLsb' + 0 + 8 + v_84 ^^^ + v_198 && + (0#32).slt + (513#32 - + v_84) && + !42#32 - + v_84 == + 0#32 && + (33#32 - + v_84).sle + 0#32 && + (20#32 - + v_84).sle + 0#32 && + !v_8 == + 2047#32 && + v_8.ult + 2048#32 && + (128#32).ule + v_8 && + v_8.ule + 65024#32 && + !v_8 == + 0#32 && + v_125 + + 528#32 == + v_127 + + 843#32 && + !39452868#32 == + v_127 + + 811#32 && + (41773216#32).ule + v_199 && + (41773088#32).ult + v_199 && + !v_199 == + 39452868#32 && + !v_199 == + 0#32 && + !39452868#32 == + v_199 && + !v_125 == + 0#32 && + !v_203 == + 0#32 && + !39452868#32 == + v_203 && + (v_127 + + v_8 <<< + v_111).ult + 42663936#32 && + !39452672#32 == + v_204 && + !BitVec.extractLsb' + 0 + 8 + v_205 == + 0#8 && + !BitVec.extractLsb' + 0 + 16 + (BitVec.setWidth + 32 + (BitVec.extractLsb' + 0 + 8 + v_83) + + BitVec.setWidth + 32 + (BitVec.extractLsb' + 8 + 8 + v_83) <<< + 8#32 ^^^ + v_115) ^^^ + 32010#16 == + 0#16 && + v_84.ult + 2047#32 && + !v_84 == + 2047#32 && + v_84.ult + 2048#32 && + (128#32).ule + v_84 && + !v_127 == + 0#32 && + !v_127 == + 41811936#32 && + v_205.slt + 254#32 && + (0#32).slt + v_205 && + v_207.slt + 254#32 && + (0#32).slt + v_207 && + !v_208 == 0#32 && + !(v_83 + v_83) <<< + v_2 + + 39453052#32 == + 0#32 && + (0#32).slt + (v_5 - 42#32) && + v_209 == v_208 && + !v_209 == 39452868#32 && + !39452868#32 == v_209 && + (v_210 - 13#32).sle 0#32 && + (0#32).slt (v_210 - 2#32) && + (v_210 - 233#32).sle 0#32 && + (3#32).ult (v_211 + 3#32) && + (v_211 + 2#32).ule 3#32 && + !v_5 == 2047#32 && + v_5.ult 2048#32 && + (128#32).ule v_5 && + !v_5 == 1#32 && + !v_210 == 127#32 && + v_210.ule 13#32 && + v_210.ult 128#32 && + !v_210 == 1#32 && + !v_210 == 0#32 && + v_211.ule 3#32 && + (0#32).slt (v_83 - 2#32) && + (v_83 - 233#32).sle 0#32 && + v_83.ule 64#32 && + v_83.ule 65024#32 && + (2#32).ule v_83 && + v_83.ult 127#32 && + v_83.ult 128#32 && + (v_212 - v_213).ult 63#32 && + v_213.ult 2147483648#32 && + v_213.ule 2147483647#32 && + !v_213 == 0#32 && + v_213.ule 4294967264#32 && + (0#32).slt v_213 && + (v_4 - 149#32).slt 0#32 && + (0#32).sle (v_4 - 148#32) && + v_214.sle 100#32 && + (99#32).slt v_214 && + v_214.slt 536870911#32 && + (0#32).sle v_214 && + !v_214 == 0#32 && + (0#32).slt v_214 && + !4#32 == v_215 && + !3#32 == v_215 && + !2#32 == v_215 && + !1#32 == v_215 && + !0#32 == v_215 && + (0#32).sle v_215) = + true := by + bv_normalize diff --git a/tests/bench/speedcenter.exec.velcom.yaml b/tests/bench/speedcenter.exec.velcom.yaml index cd0d1e1488..809a92ed22 100644 --- a/tests/bench/speedcenter.exec.velcom.yaml +++ b/tests/bench/speedcenter.exec.velcom.yaml @@ -457,6 +457,12 @@ run_config: <<: *time cmd: lean bv_decide_large_aig.lean +- attributes: + description: bv_decide_rewriter.lean + tags: [fast] + run_config: + <<: *time + cmd: lean bv_decide_rewriter.lean - attributes: description: big_do tags: [fast]