08eb78a5b2
This PR sets up the new integrated test/bench suite. It then migrates all benchmarks and some related tests to the new suite. There's also some documentation and some linting. For now, a lot of the old tests are left alone so this PR doesn't become even larger than it already is. Eventually, all tests should be migrated to the new suite though so there isn't a confusing mix of two systems.
1674 lines
770 KiB
Text
1674 lines
770 KiB
Text
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
|