Assignment computed by Houdini:
_houdini_0 = False
_houdini_1 = False
_houdini_2 = False
_houdini_3 = False
_houdini_4 = True
_houdini_5 = True
_houdini_6 = True
_houdini_7 = True
_houdini_8 = True
_houdini_9 = True
_houdini_10 = True
_houdini_11 = True
_houdini_12 = True
_houdini_13 = True
_houdini_14 = True
_houdini_15 = True
_houdini_16 = False
_houdini_17 = True
_houdini_18 = True
_houdini_19 = True
_houdini_20 = True
_houdini_21 = True
_houdini_22 = True
_houdini_23 = True
_houdini_24 = False
_houdini_25 = False
_houdini_26 = True
_houdini_27 = True
_houdini_28 = True
_houdini_29 = False
_houdini_30 = False
_houdini_31 = True
_houdini_32 = True
_houdini_33 = True
_houdini_34 = True
_houdini_35 = True
_houdini_36 = True
_houdini_37 = True
_houdini_38 = True
_houdini_39 = True
_houdini_40 = True
_houdini_41 = True
_houdini_42 = True
_houdini_43 = True
_houdini_44 = True
_houdini_45 = True
_houdini_46 = True
_houdini_47 = True
_houdini_48 = True
_houdini_49 = True
_houdini_50 = True
_houdini_51 = True
_houdini_52 = True
_houdini_53 = True
_houdini_54 = True
_houdini_55 = True
_houdini_56 = True
_houdini_57 = True
_houdini_58 = True
_houdini_59 = True
_houdini_60 = True
_houdini_61 = True
_houdini_62 = True
_houdini_63 = True
_houdini_64 = True
_houdini_65 = True
_houdini_66 = True
_houdini_67 = True
_houdini_68 = True
_houdini_69 = True
_houdini_70 = True
_houdini_71 = True
_houdini_72 = True
_houdini_73 = True
_houdini_74 = True
_houdini_75 = True
_houdini_76 = False
_houdini_77 = False
_houdini_78 = True
_houdini_79 = False
_houdini_80 = False
_houdini_81 = True
_houdini_82 = True
_houdini_83 = True
_houdini_84 = True
_houdini_85 = True
_houdini_86 = True
_houdini_87 = True
_houdini_88 = True
_houdini_89 = True
_houdini_90 = True
_houdini_91 = True
_houdini_92 = True
_houdini_93 = True
_houdini_94 = True
_houdini_95 = True
_houdini_96 = True
_houdini_97 = True
_houdini_98 = True
_houdini_99 = True
_houdini_100 = True
_houdini_101 = True
_houdini_102 = True
_houdini_103 = True
_houdini_104 = True
_houdini_105 = True
_houdini_106 = True
_houdini_107 = True
_houdini_108 = True
_houdini_109 = True
_houdini_110 = True
_houdini_111 = True
_houdini_112 = True
_houdini_113 = True
_houdini_114 = True
_houdini_115 = False
_houdini_116 = False
_houdini_117 = False
_houdini_118 = False
_houdini_119 = False
_houdini_120 = False
_houdini_121 = False
_houdini_122 = True
_houdini_123 = False
_houdini_124 = False
_houdini_125 = True
_houdini_126 = True
_houdini_127 = True
_houdini_128 = True
_houdini_129 = True
_houdini_130 = True
_houdini_131 = True
_houdini_132 = False
_houdini_133 = False
_houdini_134 = True
_houdini_135 = True
_houdini_136 = True
_houdini_137 = True
_houdini_138 = True
_houdini_139 = True
_houdini_140 = True
_houdini_141 = True
_houdini_142 = True
_houdini_143 = True
_houdini_144 = True
_houdini_145 = True
_houdini_146 = True
_houdini_147 = True
_houdini_148 = True
_houdini_149 = True
_houdini_150 = True
_houdini_151 = True
_houdini_152 = True
_houdini_153 = True
_houdini_154 = True
_houdini_155 = True
_houdini_156 = True
_houdini_157 = True
_houdini_158 = True
_houdini_159 = True
_houdini_160 = True
_houdini_161 = False
_houdini_162 = False
_houdini_163 = True
_houdini_164 = True
_houdini_165 = True
_houdini_166 = True
_houdini_167 = True
_houdini_168 = True
_houdini_169 = True
_houdini_170 = True
_houdini_171 = True
_houdini_172 = True
_houdini_173 = True
_houdini_174 = True
_houdini_175 = True
_houdini_176 = True
_houdini_177 = True
_houdini_178 = True
_houdini_179 = True
_houdini_180 = True
_houdini_181 = True
_houdini_182 = True
_houdini_183 = True
_houdini_184 = True
_houdini_185 = True
_houdini_186 = True

Boogie program verifier finished with 12 verified, 0 errors