diff --git a/tests/sat/uart-10.induction.cvc.smt2 b/tests/sat/uart-10.induction.cvc.smt2
new file mode 100644
index 00000000..ba42a762
--- /dev/null
+++ b/tests/sat/uart-10.induction.cvc.smt2
@@ -0,0 +1,203 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_LRA)
+(set-info :source |
+Specification and verification of a 8N1 decoder.
+Geoffrey Brown, Indiana University <geobrown@cs.indiana.edu>
+Lee Pike, Galois Connections, Inc. <leepike@galois.com> 
+
+Translated into CVC format by Leonardo de Moura.
+
+This benchmark was automatically translated into SMT-LIB format from
+CVC format using CVC Lite
+
+
+
+|)
+(set-info :category "industrial")
+(set-info :status sat)
+(declare-fun x_0 () Real)
+(declare-fun x_1 () Real)
+(declare-fun x_2 () Real)
+(declare-fun x_3 () Real)
+(declare-fun x_4 () Real)
+(declare-fun x_5 () Real)
+(declare-fun x_6 () Real)
+(declare-fun x_7 () Real)
+(declare-fun x_8 () Real)
+(declare-fun x_9 () Real)
+(declare-fun x_10 () Bool)
+(declare-fun x_11 () Real)
+(declare-fun x_12 () Bool)
+(declare-fun x_13 () Real)
+(declare-fun x_14 () Bool)
+(declare-fun x_15 () Real)
+(declare-fun x_16 () Bool)
+(declare-fun x_17 () Real)
+(declare-fun x_18 () Bool)
+(declare-fun x_19 () Real)
+(declare-fun x_20 () Bool)
+(declare-fun x_21 () Real)
+(declare-fun x_22 () Bool)
+(declare-fun x_23 () Real)
+(declare-fun x_24 () Bool)
+(declare-fun x_25 () Real)
+(declare-fun x_26 () Bool)
+(declare-fun x_27 () Real)
+(declare-fun x_28 () Bool)
+(declare-fun x_29 () Real)
+(declare-fun x_30 () Bool)
+(declare-fun x_31 () Real)
+(declare-fun x_32 () Real)
+(declare-fun x_33 () Real)
+(declare-fun x_34 () Real)
+(declare-fun x_35 () Real)
+(declare-fun x_36 () Real)
+(declare-fun x_37 () Real)
+(declare-fun x_38 () Real)
+(declare-fun x_39 () Real)
+(declare-fun x_40 () Real)
+(declare-fun x_41 () Real)
+(declare-fun x_42 () Real)
+(declare-fun x_43 () Real)
+(declare-fun x_44 () Real)
+(declare-fun x_45 () Real)
+(declare-fun x_46 () Real)
+(declare-fun x_47 () Real)
+(declare-fun x_48 () Real)
+(declare-fun x_49 () Real)
+(declare-fun x_50 () Real)
+(declare-fun x_51 () Real)
+(declare-fun x_52 () Real)
+(declare-fun x_53 () Real)
+(declare-fun x_54 () Real)
+(declare-fun x_55 () Real)
+(declare-fun x_56 () Real)
+(declare-fun x_57 () Real)
+(declare-fun x_58 () Real)
+(declare-fun x_59 () Real)
+(declare-fun x_60 () Real)
+(declare-fun x_61 () Real)
+(declare-fun x_62 () Real)
+(declare-fun x_63 () Real)
+(declare-fun x_64 () Real)
+(declare-fun x_65 () Real)
+(declare-fun x_66 () Real)
+(declare-fun x_67 () Real)
+(declare-fun x_68 () Real)
+(declare-fun x_69 () Real)
+(declare-fun x_70 () Real)
+(declare-fun x_71 () Real)
+(declare-fun x_72 () Real)
+(declare-fun x_73 () Real)
+(declare-fun x_74 () Real)
+(declare-fun x_75 () Real)
+(declare-fun x_76 () Real)
+(declare-fun x_77 () Real)
+(declare-fun x_78 () Real)
+(declare-fun x_79 () Real)
+(declare-fun x_80 () Real)
+(declare-fun x_81 () Real)
+(declare-fun x_82 () Real)
+(declare-fun x_83 () Real)
+(declare-fun x_84 () Real)
+(declare-fun x_85 () Real)
+(declare-fun x_86 () Real)
+(declare-fun x_87 () Real)
+(declare-fun x_88 () Real)
+(declare-fun x_89 () Real)
+(declare-fun x_90 () Real)
+(declare-fun x_91 () Real)
+(declare-fun x_92 () Real)
+(declare-fun x_93 () Real)
+(declare-fun x_94 () Real)
+(declare-fun x_95 () Real)
+(declare-fun x_96 () Real)
+(declare-fun x_97 () Real)
+(declare-fun x_98 () Real)
+(declare-fun x_99 () Real)
+(declare-fun x_100 () Real)
+(declare-fun x_101 () Real)
+(declare-fun x_102 () Real)
+(declare-fun x_103 () Real)
+(declare-fun x_104 () Real)
+(declare-fun x_105 () Real)
+(declare-fun x_106 () Real)
+(declare-fun x_107 () Real)
+(declare-fun x_108 () Real)
+(declare-fun x_109 () Real)
+(declare-fun x_110 () Real)
+(declare-fun x_111 () Real)
+(declare-fun x_112 () Real)
+(declare-fun x_113 () Real)
+(declare-fun x_114 () Real)
+(declare-fun x_115 () Real)
+(declare-fun x_116 () Real)
+(declare-fun x_117 () Real)
+(declare-fun x_118 () Real)
+(declare-fun x_119 () Real)
+(declare-fun x_120 () Real)
+(declare-fun x_121 () Real)
+(declare-fun x_122 () Real)
+(declare-fun x_123 () Real)
+(declare-fun x_124 () Real)
+(declare-fun x_125 () Real)
+(declare-fun x_126 () Real)
+(declare-fun x_127 () Real)
+(declare-fun x_128 () Real)
+(declare-fun x_129 () Real)
+(declare-fun x_130 () Real)
+(declare-fun x_131 () Real)
+(declare-fun x_132 () Real)
+(declare-fun x_133 () Real)
+(declare-fun x_134 () Real)
+(declare-fun x_135 () Real)
+(declare-fun x_136 () Real)
+(declare-fun x_137 () Real)
+(declare-fun x_138 () Real)
+(declare-fun x_139 () Real)
+(declare-fun x_140 () Real)
+(declare-fun x_141 () Real)
+(declare-fun x_142 () Real)
+(declare-fun x_143 () Real)
+(declare-fun x_144 () Real)
+(declare-fun x_145 () Real)
+(declare-fun x_146 () Real)
+(declare-fun x_147 () Real)
+(declare-fun x_148 () Real)
+(declare-fun x_149 () Real)
+(declare-fun x_150 () Real)
+(declare-fun x_151 () Real)
+(declare-fun x_152 () Real)
+(declare-fun x_153 () Real)
+(declare-fun x_154 () Real)
+(declare-fun x_155 () Real)
+(declare-fun x_156 () Real)
+(declare-fun x_157 () Real)
+(declare-fun x_158 () Real)
+(declare-fun x_159 () Real)
+(declare-fun x_160 () Real)
+(declare-fun x_161 () Real)
+(declare-fun x_162 () Real)
+(declare-fun x_163 () Real)
+(declare-fun x_164 () Real)
+(declare-fun x_165 () Real)
+(declare-fun x_166 () Real)
+(declare-fun x_167 () Real)
+(declare-fun x_168 () Real)
+(declare-fun x_169 () Real)
+(declare-fun x_170 () Real)
+(declare-fun x_171 () Real)
+(declare-fun x_172 () Real)
+(declare-fun x_173 () Real)
+(declare-fun x_174 () Real)
+(declare-fun x_175 () Real)
+(declare-fun x_176 () Real)
+(declare-fun x_177 () Real)
+(declare-fun x_178 () Real)
+(declare-fun x_179 () Real)
+(declare-fun x_180 () Real)
+(declare-fun x_181 () Real)
+(declare-fun x_182 () Real)
+(assert (let ((?v_14 (not x_28))) (let ((?v_16 (and ?v_14 (< x_29 8))) (?v_57 (not x_26))) (let ((?v_59 (and ?v_57 (< x_27 8))) (?v_95 (not x_24))) (let ((?v_97 (and ?v_95 (< x_25 8))) (?v_133 (not x_22))) (let ((?v_135 (and ?v_133 (< x_23 8))) (?v_171 (not x_20))) (let ((?v_173 (and ?v_171 (< x_21 8))) (?v_209 (not x_18))) (let ((?v_211 (and ?v_209 (< x_19 8))) (?v_247 (not x_16))) (let ((?v_249 (and ?v_247 (< x_17 8))) (?v_285 (not x_14))) (let ((?v_287 (and ?v_285 (< x_15 8))) (?v_323 (not x_12))) (let ((?v_325 (and ?v_323 (< x_13 8))) (?v_361 (not x_10))) (let ((?v_363 (and ?v_361 (< x_11 8))) (?v_351 (= x_32 10)) (?v_353 (= x_33 1)) (?v_355 (= x_12 x_10)) (?v_356 (= x_34 x_35)) (?v_360 (= x_36 x_35)) (?v_357 (= x_37 x_38)) (?v_359 (= x_39 x_40)) (?v_364 (= x_11 9)) (?v_365 (= x_37 1)) (?v_366 (not (= x_40 1))) (?v_367 (not (= x_40 0))) (?v_368 (= x_40 3)) (?v_369 (= x_40 2)) (?v_358 (= x_13 x_11)) (?v_370 (= x_41 x_36)) (?v_349 (= x_42 x_43)) (?v_371 (= x_33 x_44)) (?v_350 (= x_45 x_32)) (?v_372 (= x_46 x_47)) (?v_373 (< x_32 9)) (?v_375 (= x_0 2)) (?v_374 (= x_36 x_47)) (?v_379 (= x_35 x_36))) (let ((?v_380 (not ?v_379)) (?v_377 (= x_11 x_32)) (?v_385 (not (= x_43 x_38))) (?v_344 (= x_1 1)) (?v_313 (= x_45 10)) (?v_315 (= x_56 1)) (?v_317 (= x_14 x_12)) (?v_318 (= x_57 x_34)) (?v_322 (= x_41 x_34)) (?v_319 (= x_58 x_37)) (?v_321 (= x_59 x_39)) (?v_326 (= x_13 9)) (?v_327 (= x_58 1)) (?v_328 (not (= x_39 1))) (?v_329 (not (= x_39 0))) (?v_330 (= x_39 3)) (?v_331 (= x_39 2)) (?v_320 (= x_15 x_13)) (?v_332 (= x_60 x_41)) (?v_311 (= x_61 x_42)) (?v_333 (= x_56 x_33)) (?v_312 (= x_62 x_45)) (?v_334 (= x_63 x_46)) (?v_335 (< x_45 9)) (?v_337 (= x_1 2)) (?v_336 (= x_41 x_46)) (?v_341 (= x_34 x_41))) (let ((?v_342 (not ?v_341)) (?v_339 (= x_13 x_45)) (?v_347 (not (= x_42 x_37))) (?v_306 (= x_2 1)) (?v_275 (= x_62 10)) (?v_277 (= x_70 1)) (?v_279 (= x_16 x_14)) (?v_280 (= x_71 x_57)) (?v_284 (= x_60 x_57)) (?v_281 (= x_72 x_58)) (?v_283 (= x_73 x_59)) (?v_288 (= x_15 9)) (?v_289 (= x_72 1)) (?v_290 (not (= x_59 1))) (?v_291 (not (= x_59 0))) (?v_292 (= x_59 3)) (?v_293 (= x_59 2)) (?v_282 (= x_17 x_15)) (?v_294 (= x_74 x_60)) (?v_273 (= x_75 x_61)) (?v_295 (= x_70 x_56)) (?v_274 (= x_76 x_62)) (?v_296 (= x_77 x_63)) (?v_297 (< x_62 9)) (?v_299 (= x_2 2)) (?v_298 (= x_60 x_63)) (?v_303 (= x_57 x_60))) (let ((?v_304 (not ?v_303)) (?v_301 (= x_15 x_62)) (?v_309 (not (= x_61 x_58))) (?v_268 (= x_3 1)) (?v_237 (= x_76 10)) (?v_239 (= x_84 1)) (?v_241 (= x_18 x_16)) (?v_242 (= x_85 x_71)) (?v_246 (= x_74 x_71)) (?v_243 (= x_86 x_72)) (?v_245 (= x_87 x_73)) (?v_250 (= x_17 9)) (?v_251 (= x_86 1)) (?v_252 (not (= x_73 1))) (?v_253 (not (= x_73 0))) (?v_254 (= x_73 3)) (?v_255 (= x_73 2)) (?v_244 (= x_19 x_17)) (?v_256 (= x_88 x_74)) (?v_235 (= x_89 x_75)) (?v_257 (= x_84 x_70)) (?v_236 (= x_90 x_76)) (?v_258 (= x_91 x_77)) (?v_259 (< x_76 9)) (?v_261 (= x_3 2)) (?v_260 (= x_74 x_77)) (?v_265 (= x_71 x_74))) (let ((?v_266 (not ?v_265)) (?v_263 (= x_17 x_76)) (?v_271 (not (= x_75 x_72))) (?v_230 (= x_4 1)) (?v_199 (= x_90 10)) (?v_201 (= x_98 1)) (?v_203 (= x_20 x_18)) (?v_204 (= x_99 x_85)) (?v_208 (= x_88 x_85)) (?v_205 (= x_100 x_86)) (?v_207 (= x_101 x_87)) (?v_212 (= x_19 9)) (?v_213 (= x_100 1)) (?v_214 (not (= x_87 1))) (?v_215 (not (= x_87 0))) (?v_216 (= x_87 3)) (?v_217 (= x_87 2)) (?v_206 (= x_21 x_19)) (?v_218 (= x_102 x_88)) (?v_197 (= x_103 x_89)) (?v_219 (= x_98 x_84)) (?v_198 (= x_104 x_90)) (?v_220 (= x_105 x_91)) (?v_221 (< x_90 9)) (?v_223 (= x_4 2)) (?v_222 (= x_88 x_91)) (?v_227 (= x_85 x_88))) (let ((?v_228 (not ?v_227)) (?v_225 (= x_19 x_90)) (?v_233 (not (= x_89 x_86))) (?v_192 (= x_5 1)) (?v_161 (= x_104 10)) (?v_163 (= x_112 1)) (?v_165 (= x_22 x_20)) (?v_166 (= x_113 x_99)) (?v_170 (= x_102 x_99)) (?v_167 (= x_114 x_100)) (?v_169 (= x_115 x_101)) (?v_174 (= x_21 9)) (?v_175 (= x_114 1)) (?v_176 (not (= x_101 1))) (?v_177 (not (= x_101 0))) (?v_178 (= x_101 3)) (?v_179 (= x_101 2)) (?v_168 (= x_23 x_21)) (?v_180 (= x_116 x_102)) (?v_159 (= x_117 x_103)) (?v_181 (= x_112 x_98)) (?v_160 (= x_118 x_104)) (?v_182 (= x_119 x_105)) (?v_183 (< x_104 9)) (?v_185 (= x_5 2)) (?v_184 (= x_102 x_105)) (?v_189 (= x_99 x_102))) (let ((?v_190 (not ?v_189)) (?v_187 (= x_21 x_104)) (?v_195 (not (= x_103 x_100))) (?v_154 (= x_6 1)) (?v_123 (= x_118 10)) (?v_125 (= x_126 1)) (?v_127 (= x_24 x_22)) (?v_128 (= x_127 x_113)) (?v_132 (= x_116 x_113)) (?v_129 (= x_128 x_114)) (?v_131 (= x_129 x_115)) (?v_136 (= x_23 9)) (?v_137 (= x_128 1)) (?v_138 (not (= x_115 1))) (?v_139 (not (= x_115 0))) (?v_140 (= x_115 3)) (?v_141 (= x_115 2)) (?v_130 (= x_25 x_23)) (?v_142 (= x_130 x_116)) (?v_121 (= x_131 x_117)) (?v_143 (= x_126 x_112)) (?v_122 (= x_132 x_118)) (?v_144 (= x_133 x_119)) (?v_145 (< x_118 9)) (?v_147 (= x_6 2)) (?v_146 (= x_116 x_119)) (?v_151 (= x_113 x_116))) (let ((?v_152 (not ?v_151)) (?v_149 (= x_23 x_118)) (?v_157 (not (= x_117 x_114))) (?v_116 (= x_7 1)) (?v_85 (= x_132 10)) (?v_87 (= x_140 1)) (?v_89 (= x_26 x_24)) (?v_90 (= x_141 x_127)) (?v_94 (= x_130 x_127)) (?v_91 (= x_142 x_128)) (?v_93 (= x_143 x_129)) (?v_98 (= x_25 9)) (?v_99 (= x_142 1)) (?v_100 (not (= x_129 1))) (?v_101 (not (= x_129 0))) (?v_102 (= x_129 3)) (?v_103 (= x_129 2)) (?v_92 (= x_27 x_25)) (?v_104 (= x_144 x_130)) (?v_83 (= x_145 x_131)) (?v_105 (= x_140 x_126)) (?v_84 (= x_146 x_132)) (?v_106 (= x_147 x_133)) (?v_107 (< x_132 9)) (?v_109 (= x_7 2)) (?v_108 (= x_130 x_133)) (?v_113 (= x_127 x_130))) (let ((?v_114 (not ?v_113)) (?v_111 (= x_25 x_132)) (?v_119 (not (= x_131 x_128))) (?v_78 (= x_8 1)) (?v_42 (= x_146 10)) (?v_44 (= x_154 1)) (?v_50 (= x_28 x_26)) (?v_51 (= x_155 x_141)) (?v_55 (= x_144 x_141)) (?v_52 (= x_156 x_142)) (?v_54 (= x_157 x_143)) (?v_60 (= x_27 9)) (?v_61 (= x_156 1)) (?v_62 (not (= x_143 1))) (?v_63 (not (= x_143 0))) (?v_64 (= x_143 3)) (?v_65 (= x_143 2)) (?v_53 (= x_29 x_27)) (?v_66 (= x_158 x_144)) (?v_40 (= x_159 x_145)) (?v_67 (= x_154 x_140)) (?v_41 (= x_160 x_146)) (?v_68 (= x_161 x_147)) (?v_69 (< x_146 9)) (?v_71 (= x_8 2)) (?v_70 (= x_144 x_147)) (?v_75 (= x_141 x_144))) (let ((?v_76 (not ?v_75)) (?v_73 (= x_27 x_146)) (?v_81 (not (= x_145 x_142))) (?v_34 (= x_9 1)) (?v_2 (= x_160 10)) (?v_4 (= x_168 1)) (?v_8 (= x_30 x_28)) (?v_9 (= x_169 x_155)) (?v_13 (= x_158 x_155)) (?v_10 (= x_170 x_156)) (?v_12 (= x_171 x_157)) (?v_17 (= x_29 9)) (?v_18 (= x_170 1)) (?v_19 (not (= x_157 1))) (?v_20 (not (= x_157 0))) (?v_21 (= x_157 3)) (?v_22 (= x_157 2)) (?v_11 (= x_31 x_29)) (?v_23 (= x_172 x_158)) (?v_0 (= x_173 x_159)) (?v_24 (= x_168 x_154)) (?v_1 (= x_174 x_160)) (?v_25 (= x_175 x_161)) (?v_26 (< x_160 9)) (?v_28 (= x_9 2)) (?v_27 (= x_158 x_161)) (?v_32 (= x_155 x_158))) (let ((?v_33 (not ?v_32)) (?v_30 (= x_29 x_160)) (?v_38 (not (= x_159 x_156))) (?v_35 (= x_176 1)) (?v_362 (not (< x_37 0))) (?v_324 (not (< x_58 0))) (?v_286 (not (< x_72 0))) (?v_248 (not (< x_86 0))) (?v_210 (not (< x_100 0))) (?v_172 (not (< x_114 0))) (?v_134 (not (< x_128 0))) (?v_96 (not (< x_142 0))) (?v_58 (not (< x_156 0))) (?v_15 (not (< x_170 0))) (?v_382 (= x_0 1)) (?v_3 (= x_168 0)) (?v_5 (= x_174 1)) (?v_77 (= x_9 0)) (?v_43 (= x_154 0)) (?v_45 (= x_160 1)) (?v_115 (= x_8 0)) (?v_86 (= x_140 0)) (?v_88 (= x_146 1)) (?v_153 (= x_7 0)) (?v_124 (= x_126 0)) (?v_126 (= x_132 1)) (?v_191 (= x_6 0)) (?v_162 (= x_112 0)) (?v_164 (= x_118 1)) (?v_229 (= x_5 0)) (?v_200 (= x_98 0)) (?v_202 (= x_104 1)) (?v_267 (= x_4 0)) (?v_238 (= x_84 0)) (?v_240 (= x_90 1)) (?v_305 (= x_3 0)) (?v_276 (= x_70 0)) (?v_278 (= x_76 1)) (?v_343 (= x_2 0)) (?v_314 (= x_56 0)) (?v_316 (= x_62 1)) (?v_381 (= x_1 0)) (?v_352 (= x_33 0)) (?v_354 (= x_45 1)) (?v_36 (not ?v_26)) (?v_37 (and ?v_26 (not ?v_27))) (?v_31 (and ?v_26 ?v_27))) (let ((?v_29 (and ?v_31 ?v_33))) (let ((?v_39 (and ?v_29 ?v_30)) (?v_79 (not ?v_69)) (?v_80 (and ?v_69 (not ?v_70))) (?v_74 (and ?v_69 ?v_70))) (let ((?v_72 (and ?v_74 ?v_76))) (let ((?v_82 (and ?v_72 ?v_73)) (?v_117 (not ?v_107)) (?v_118 (and ?v_107 (not ?v_108))) (?v_112 (and ?v_107 ?v_108))) (let ((?v_110 (and ?v_112 ?v_114))) (let ((?v_120 (and ?v_110 ?v_111)) (?v_155 (not ?v_145)) (?v_156 (and ?v_145 (not ?v_146))) (?v_150 (and ?v_145 ?v_146))) (let ((?v_148 (and ?v_150 ?v_152))) (let ((?v_158 (and ?v_148 ?v_149)) (?v_193 (not ?v_183)) (?v_194 (and ?v_183 (not ?v_184))) (?v_188 (and ?v_183 ?v_184))) (let ((?v_186 (and ?v_188 ?v_190))) (let ((?v_196 (and ?v_186 ?v_187)) (?v_231 (not ?v_221)) (?v_232 (and ?v_221 (not ?v_222))) (?v_226 (and ?v_221 ?v_222))) (let ((?v_224 (and ?v_226 ?v_228))) (let ((?v_234 (and ?v_224 ?v_225)) (?v_269 (not ?v_259)) (?v_270 (and ?v_259 (not ?v_260))) (?v_264 (and ?v_259 ?v_260))) (let ((?v_262 (and ?v_264 ?v_266))) (let ((?v_272 (and ?v_262 ?v_263)) (?v_307 (not ?v_297)) (?v_308 (and ?v_297 (not ?v_298))) (?v_302 (and ?v_297 ?v_298))) (let ((?v_300 (and ?v_302 ?v_304))) (let ((?v_310 (and ?v_300 ?v_301)) (?v_345 (not ?v_335)) (?v_346 (and ?v_335 (not ?v_336))) (?v_340 (and ?v_335 ?v_336))) (let ((?v_338 (and ?v_340 ?v_342))) (let ((?v_348 (and ?v_338 ?v_339)) (?v_383 (not ?v_373)) (?v_384 (and ?v_373 (not ?v_374))) (?v_378 (and ?v_373 ?v_374))) (let ((?v_376 (and ?v_378 ?v_380))) (let ((?v_386 (and ?v_376 ?v_377)) (?v_6 (- 1 x_51))) (let ((?v_46 (* ?v_6 23)) (?v_7 (+ x_51 1))) (let ((?v_47 (* ?v_7 23)) (?v_48 (* ?v_6 16)) (?v_49 (* ?v_7 16)) (?v_56 (- 16 x_53))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (<= x_171 3) (>= x_171 0)) (<= x_168 3)) (>= x_168 0)) (<= x_157 3)) (>= x_157 0)) (<= x_154 3)) (>= x_154 0)) (<= x_143 3)) (>= x_143 0)) (<= x_140 3)) (>= x_140 0)) (<= x_129 3)) (>= x_129 0)) (<= x_126 3)) (>= x_126 0)) (<= x_115 3)) (>= x_115 0)) (<= x_112 3)) (>= x_112 0)) (<= x_101 3)) (>= x_101 0)) (<= x_98 3)) (>= x_98 0)) (<= x_87 3)) (>= x_87 0)) (<= x_84 3)) (>= x_84 0)) (<= x_73 3)) (>= x_73 0)) (<= x_70 3)) (>= x_70 0)) (<= x_59 3)) (>= x_59 0)) (<= x_56 3)) (>= x_56 0)) (<= x_44 3)) (>= x_44 0)) (<= x_40 3)) (>= x_40 0)) (<= x_39 3)) (>= x_39 0)) (<= x_33 3)) (>= x_33 0)) (not (< x_0 0))) (<= x_0 2)) (not (< x_1 0))) (<= x_1 2)) (not (< x_2 0))) (<= x_2 2)) (not (< x_3 0))) (<= x_3 2)) (not (< x_4 0))) (<= x_4 2)) (not (< x_5 0))) (<= x_5 2)) (not (< x_6 0))) (<= x_6 2)) (not (< x_7 0))) (<= x_7 2)) (not (< x_8 0))) (<= x_8 2)) (not (< x_9 0))) (<= x_9 2)) (not (< x_11 0))) (<= x_11 9)) (not (< x_13 0))) (<= x_13 9)) (not (< x_15 0))) (<= x_15 9)) (not (< x_17 0))) (<= x_17 9)) (not (< x_19 0))) (<= x_19 9)) (not (< x_21 0))) (<= x_21 9)) (not (< x_23 0))) (<= x_23 9)) (not (< x_25 0))) (<= x_25 9)) (not (< x_27 0))) (<= x_27 9)) (not (< x_29 0))) (<= x_29 9)) (not (< x_31 0))) (<= x_31 9)) (not (< x_32 1))) (<= x_32 10)) ?v_362) (<= x_37 1)) (not (< x_38 0))) (<= x_38 1)) (not (< x_42 0))) (<= x_42 1)) (not (< x_43 0))) (<= x_43 1)) (not (< x_45 1))) (<= x_45 10)) (>= x_51 0)) (< x_51 (/ 3 151))) (>= x_53 0)) (< x_53 4)) ?v_324) (<= x_58 1)) (not (< x_61 0))) (<= x_61 1)) (not (< x_62 1))) (<= x_62 10)) ?v_286) (<= x_72 1)) (not (< x_75 0))) (<= x_75 1)) (not (< x_76 1))) (<= x_76 10)) ?v_248) (<= x_86 1)) (not (< x_89 0))) (<= x_89 1)) (not (< x_90 1))) (<= x_90 10)) ?v_210) (<= x_100 1)) (not (< x_103 0))) (<= x_103 1)) (not (< x_104 1))) (<= x_104 10)) ?v_172) (<= x_114 1)) (not (< x_117 0))) (<= x_117 1)) (not (< x_118 1))) (<= x_118 10)) ?v_134) (<= x_128 1)) (not (< x_131 0))) (<= x_131 1)) (not (< x_132 1))) (<= x_132 10)) ?v_96) (<= x_142 1)) (not (< x_145 0))) (<= x_145 1)) (not (< x_146 1))) (<= x_146 10)) ?v_58) (<= x_156 1)) (not (< x_159 0))) (<= x_159 1)) (not (< x_160 1))) (<= x_160 10)) ?v_15) (<= x_170 1)) (not (< x_173 0))) (<= x_173 1)) (not (< x_174 1))) (<= x_174 10)) (not (< x_176 0))) (<= x_176 2)) (not ?v_34)) (not ?v_78)) (not ?v_116)) (not ?v_154)) (not ?v_192)) (not ?v_230)) (not ?v_268)) (not ?v_306)) (not ?v_344)) (not ?v_382)) (or (or (and (and (and (and (and (and (and (and (and (and (= x_177 0) (or (and (and (and (= x_178 0) (< x_158 x_161)) (<= x_161 x_155)) (= x_172 x_161)) (and (and (and (= x_178 1) (< x_158 x_155)) (<= x_155 x_161)) (= x_172 x_155)))) ?v_0) ?v_24) ?v_1) ?v_25) ?v_8) ?v_9) ?v_10) ?v_11) ?v_12) (and (and (and (and (and (and (and (and (and (= x_177 1) (or (or (and (and (and (and (and (= x_179 0) ?v_2) ?v_20) ?v_4) ?v_0) ?v_1) (and (and (and (and (and (= x_179 1) ?v_2) ?v_19) ?v_3) ?v_5) ?v_0)) (and (and (and (and (= x_179 2) (not ?v_2)) (ite (or ?v_22 ?v_21) (or ?v_3 ?v_4) (= x_168 x_157))) (= x_174 (+ x_160 1))) (= x_173 (ite ?v_4 1 0))))) ?v_27) (ite (= x_174 10) (and (<= (+ x_158 ?v_6) x_175) (<= x_175 (+ (+ x_158 x_51) 1))) (ite ?v_5 (and (<= (+ x_158 ?v_46) x_175) (<= x_175 (+ x_158 ?v_47))) (and (<= (+ x_158 ?v_48) x_175) (<= x_175 (+ x_158 ?v_49)))))) ?v_23) ?v_8) ?v_9) ?v_10) ?v_11) ?v_12)) (and (and (and (and (and (and (and (and (= x_177 2) (or (and (and (and (and (= x_180 0) ?v_13) ?v_14) (= x_169 (+ x_158 x_53))) x_30) (and (and (and (and (= x_180 1) ?v_13) x_28) (= x_169 (+ x_158 ?v_56))) (not x_30)))) (or (and (and (and (= x_181 0) ?v_16) (or (= x_170 0) ?v_18)) ?v_15) (and (and (= x_181 1) (not ?v_16)) ?v_10))) (or (or (or (and (and (and (and (= x_182 0) ?v_14) ?v_17) (= x_31 9)) ?v_12) (and (and (and (and (= x_182 1) ?v_14) ?v_17) (= x_171 2)) (= x_31 0))) (and (and (and (and (= x_182 2) ?v_14) (< x_29 9)) (= x_171 (ite (or ?v_18 (= x_29 8)) (ite ?v_19 3 x_157) (ite ?v_20 2 x_157)))) (= x_31 (+ x_29 1)))) (and (and (and (= x_182 3) x_28) (= x_171 (ite ?v_21 1 (ite ?v_22 0 x_157)))) ?v_11))) ?v_23) ?v_0) ?v_24) ?v_1) ?v_25))) (or (or (or (or (and (and ?v_28 (or (or ?v_36 ?v_37) ?v_39)) (= x_176 2)) (and (and ?v_28 (or (and ?v_29 (not ?v_30)) (and ?v_31 ?v_32))) ?v_35)) (and (and (and (and (and ?v_28 ?v_26) ?v_27) ?v_33) ?v_30) (= x_176 0))) (and ?v_34 ?v_35)) (and (and ?v_77 (or (or (and ?v_36 ?v_38) (and ?v_37 ?v_38)) (and ?v_39 ?v_38))) ?v_35))) (or (or (and (and (and (and (and (and (and (and (and (and (= x_162 0) (or (and (and (and (= x_163 0) (< x_144 x_147)) (<= x_147 x_141)) (= x_158 x_147)) (and (and (and (= x_163 1) (< x_144 x_141)) (<= x_141 x_147)) (= x_158 x_141)))) ?v_40) ?v_67) ?v_41) ?v_68) ?v_50) ?v_51) ?v_52) ?v_53) ?v_54) (and (and (and (and (and (and (and (and (and (= x_162 1) (or (or (and (and (and (and (and (= x_164 0) ?v_42) ?v_63) ?v_44) ?v_40) ?v_41) (and (and (and (and (and (= x_164 1) ?v_42) ?v_62) ?v_43) ?v_45) ?v_40)) (and (and (and (and (= x_164 2) (not ?v_42)) (ite (or ?v_65 ?v_64) (or ?v_43 ?v_44) (= x_154 x_143))) (= x_160 (+ x_146 1))) (= x_159 (ite ?v_44 1 0))))) ?v_70) (ite ?v_2 (and (<= (+ x_144 ?v_6) x_161) (<= x_161 (+ (+ x_144 x_51) 1))) (ite ?v_45 (and (<= (+ x_144 ?v_46) x_161) (<= x_161 (+ x_144 ?v_47))) (and (<= (+ x_144 ?v_48) x_161) (<= x_161 (+ x_144 ?v_49)))))) ?v_66) ?v_50) ?v_51) ?v_52) ?v_53) ?v_54)) (and (and (and (and (and (and (and (and (= x_162 2) (or (and (and (and (and (= x_165 0) ?v_55) ?v_57) (= x_155 (+ x_144 x_53))) x_28) (and (and (and (and (= x_165 1) ?v_55) x_26) (= x_155 (+ x_144 ?v_56))) ?v_14))) (or (and (and (and (= x_166 0) ?v_59) (or (= x_156 0) ?v_61)) ?v_58) (and (and (= x_166 1) (not ?v_59)) ?v_52))) (or (or (or (and (and (and (and (= x_167 0) ?v_57) ?v_60) ?v_17) ?v_54) (and (and (and (and (= x_167 1) ?v_57) ?v_60) ?v_22) (= x_29 0))) (and (and (and (and (= x_167 2) ?v_57) (< x_27 9)) (= x_157 (ite (or ?v_61 (= x_27 8)) (ite ?v_62 3 x_143) (ite ?v_63 2 x_143)))) (= x_29 (+ x_27 1)))) (and (and (and (= x_167 3) x_26) (= x_157 (ite ?v_64 1 (ite ?v_65 0 x_143)))) ?v_53))) ?v_66) ?v_40) ?v_67) ?v_41) ?v_68))) (or (or (or (or (and (and ?v_71 (or (or ?v_79 ?v_80) ?v_82)) ?v_28) (and (and ?v_71 (or (and ?v_72 (not ?v_73)) (and ?v_74 ?v_75))) ?v_34)) (and (and (and (and (and ?v_71 ?v_69) ?v_70) ?v_76) ?v_73) ?v_77)) (and ?v_78 ?v_34)) (and (and ?v_115 (or (or (and ?v_79 ?v_81) (and ?v_80 ?v_81)) (and ?v_82 ?v_81))) ?v_34))) (or (or (and (and (and (and (and (and (and (and (and (and (= x_148 0) (or (and (and (and (= x_149 0) (< x_130 x_133)) (<= x_133 x_127)) (= x_144 x_133)) (and (and (and (= x_149 1) (< x_130 x_127)) (<= x_127 x_133)) (= x_144 x_127)))) ?v_83) ?v_105) ?v_84) ?v_106) ?v_89) ?v_90) ?v_91) ?v_92) ?v_93) (and (and (and (and (and (and (and (and (and (= x_148 1) (or (or (and (and (and (and (and (= x_150 0) ?v_85) ?v_101) ?v_87) ?v_83) ?v_84) (and (and (and (and (and (= x_150 1) ?v_85) ?v_100) ?v_86) ?v_88) ?v_83)) (and (and (and (and (= x_150 2) (not ?v_85)) (ite (or ?v_103 ?v_102) (or ?v_86 ?v_87) (= x_140 x_129))) (= x_146 (+ x_132 1))) (= x_145 (ite ?v_87 1 0))))) ?v_108) (ite ?v_42 (and (<= (+ x_130 ?v_6) x_147) (<= x_147 (+ (+ x_130 x_51) 1))) (ite ?v_88 (and (<= (+ x_130 ?v_46) x_147) (<= x_147 (+ x_130 ?v_47))) (and (<= (+ x_130 ?v_48) x_147) (<= x_147 (+ x_130 ?v_49)))))) ?v_104) ?v_89) ?v_90) ?v_91) ?v_92) ?v_93)) (and (and (and (and (and (and (and (and (= x_148 2) (or (and (and (and (and (= x_151 0) ?v_94) ?v_95) (= x_141 (+ x_130 x_53))) x_26) (and (and (and (and (= x_151 1) ?v_94) x_24) (= x_141 (+ x_130 ?v_56))) ?v_57))) (or (and (and (and (= x_152 0) ?v_97) (or (= x_142 0) ?v_99)) ?v_96) (and (and (= x_152 1) (not ?v_97)) ?v_91))) (or (or (or (and (and (and (and (= x_153 0) ?v_95) ?v_98) ?v_60) ?v_93) (and (and (and (and (= x_153 1) ?v_95) ?v_98) ?v_65) (= x_27 0))) (and (and (and (and (= x_153 2) ?v_95) (< x_25 9)) (= x_143 (ite (or ?v_99 (= x_25 8)) (ite ?v_100 3 x_129) (ite ?v_101 2 x_129)))) (= x_27 (+ x_25 1)))) (and (and (and (= x_153 3) x_24) (= x_143 (ite ?v_102 1 (ite ?v_103 0 x_129)))) ?v_92))) ?v_104) ?v_83) ?v_105) ?v_84) ?v_106))) (or (or (or (or (and (and ?v_109 (or (or ?v_117 ?v_118) ?v_120)) ?v_71) (and (and ?v_109 (or (and ?v_110 (not ?v_111)) (and ?v_112 ?v_113))) ?v_78)) (and (and (and (and (and ?v_109 ?v_107) ?v_108) ?v_114) ?v_111) ?v_115)) (and ?v_116 ?v_78)) (and (and ?v_153 (or (or (and ?v_117 ?v_119) (and ?v_118 ?v_119)) (and ?v_120 ?v_119))) ?v_78))) (or (or (and (and (and (and (and (and (and (and (and (and (= x_134 0) (or (and (and (and (= x_135 0) (< x_116 x_119)) (<= x_119 x_113)) (= x_130 x_119)) (and (and (and (= x_135 1) (< x_116 x_113)) (<= x_113 x_119)) (= x_130 x_113)))) ?v_121) ?v_143) ?v_122) ?v_144) ?v_127) ?v_128) ?v_129) ?v_130) ?v_131) (and (and (and (and (and (and (and (and (and (= x_134 1) (or (or (and (and (and (and (and (= x_136 0) ?v_123) ?v_139) ?v_125) ?v_121) ?v_122) (and (and (and (and (and (= x_136 1) ?v_123) ?v_138) ?v_124) ?v_126) ?v_121)) (and (and (and (and (= x_136 2) (not ?v_123)) (ite (or ?v_141 ?v_140) (or ?v_124 ?v_125) (= x_126 x_115))) (= x_132 (+ x_118 1))) (= x_131 (ite ?v_125 1 0))))) ?v_146) (ite ?v_85 (and (<= (+ x_116 ?v_6) x_133) (<= x_133 (+ (+ x_116 x_51) 1))) (ite ?v_126 (and (<= (+ x_116 ?v_46) x_133) (<= x_133 (+ x_116 ?v_47))) (and (<= (+ x_116 ?v_48) x_133) (<= x_133 (+ x_116 ?v_49)))))) ?v_142) ?v_127) ?v_128) ?v_129) ?v_130) ?v_131)) (and (and (and (and (and (and (and (and (= x_134 2) (or (and (and (and (and (= x_137 0) ?v_132) ?v_133) (= x_127 (+ x_116 x_53))) x_24) (and (and (and (and (= x_137 1) ?v_132) x_22) (= x_127 (+ x_116 ?v_56))) ?v_95))) (or (and (and (and (= x_138 0) ?v_135) (or (= x_128 0) ?v_137)) ?v_134) (and (and (= x_138 1) (not ?v_135)) ?v_129))) (or (or (or (and (and (and (and (= x_139 0) ?v_133) ?v_136) ?v_98) ?v_131) (and (and (and (and (= x_139 1) ?v_133) ?v_136) ?v_103) (= x_25 0))) (and (and (and (and (= x_139 2) ?v_133) (< x_23 9)) (= x_129 (ite (or ?v_137 (= x_23 8)) (ite ?v_138 3 x_115) (ite ?v_139 2 x_115)))) (= x_25 (+ x_23 1)))) (and (and (and (= x_139 3) x_22) (= x_129 (ite ?v_140 1 (ite ?v_141 0 x_115)))) ?v_130))) ?v_142) ?v_121) ?v_143) ?v_122) ?v_144))) (or (or (or (or (and (and ?v_147 (or (or ?v_155 ?v_156) ?v_158)) ?v_109) (and (and ?v_147 (or (and ?v_148 (not ?v_149)) (and ?v_150 ?v_151))) ?v_116)) (and (and (and (and (and ?v_147 ?v_145) ?v_146) ?v_152) ?v_149) ?v_153)) (and ?v_154 ?v_116)) (and (and ?v_191 (or (or (and ?v_155 ?v_157) (and ?v_156 ?v_157)) (and ?v_158 ?v_157))) ?v_116))) (or (or (and (and (and (and (and (and (and (and (and (and (= x_120 0) (or (and (and (and (= x_121 0) (< x_102 x_105)) (<= x_105 x_99)) (= x_116 x_105)) (and (and (and (= x_121 1) (< x_102 x_99)) (<= x_99 x_105)) (= x_116 x_99)))) ?v_159) ?v_181) ?v_160) ?v_182) ?v_165) ?v_166) ?v_167) ?v_168) ?v_169) (and (and (and (and (and (and (and (and (and (= x_120 1) (or (or (and (and (and (and (and (= x_122 0) ?v_161) ?v_177) ?v_163) ?v_159) ?v_160) (and (and (and (and (and (= x_122 1) ?v_161) ?v_176) ?v_162) ?v_164) ?v_159)) (and (and (and (and (= x_122 2) (not ?v_161)) (ite (or ?v_179 ?v_178) (or ?v_162 ?v_163) (= x_112 x_101))) (= x_118 (+ x_104 1))) (= x_117 (ite ?v_163 1 0))))) ?v_184) (ite ?v_123 (and (<= (+ x_102 ?v_6) x_119) (<= x_119 (+ (+ x_102 x_51) 1))) (ite ?v_164 (and (<= (+ x_102 ?v_46) x_119) (<= x_119 (+ x_102 ?v_47))) (and (<= (+ x_102 ?v_48) x_119) (<= x_119 (+ x_102 ?v_49)))))) ?v_180) ?v_165) ?v_166) ?v_167) ?v_168) ?v_169)) (and (and (and (and (and (and (and (and (= x_120 2) (or (and (and (and (and (= x_123 0) ?v_170) ?v_171) (= x_113 (+ x_102 x_53))) x_22) (and (and (and (and (= x_123 1) ?v_170) x_20) (= x_113 (+ x_102 ?v_56))) ?v_133))) (or (and (and (and (= x_124 0) ?v_173) (or (= x_114 0) ?v_175)) ?v_172) (and (and (= x_124 1) (not ?v_173)) ?v_167))) (or (or (or (and (and (and (and (= x_125 0) ?v_171) ?v_174) ?v_136) ?v_169) (and (and (and (and (= x_125 1) ?v_171) ?v_174) ?v_141) (= x_23 0))) (and (and (and (and (= x_125 2) ?v_171) (< x_21 9)) (= x_115 (ite (or ?v_175 (= x_21 8)) (ite ?v_176 3 x_101) (ite ?v_177 2 x_101)))) (= x_23 (+ x_21 1)))) (and (and (and (= x_125 3) x_20) (= x_115 (ite ?v_178 1 (ite ?v_179 0 x_101)))) ?v_168))) ?v_180) ?v_159) ?v_181) ?v_160) ?v_182))) (or (or (or (or (and (and ?v_185 (or (or ?v_193 ?v_194) ?v_196)) ?v_147) (and (and ?v_185 (or (and ?v_186 (not ?v_187)) (and ?v_188 ?v_189))) ?v_154)) (and (and (and (and (and ?v_185 ?v_183) ?v_184) ?v_190) ?v_187) ?v_191)) (and ?v_192 ?v_154)) (and (and ?v_229 (or (or (and ?v_193 ?v_195) (and ?v_194 ?v_195)) (and ?v_196 ?v_195))) ?v_154))) (or (or (and (and (and (and (and (and (and (and (and (and (= x_106 0) (or (and (and (and (= x_107 0) (< x_88 x_91)) (<= x_91 x_85)) (= x_102 x_91)) (and (and (and (= x_107 1) (< x_88 x_85)) (<= x_85 x_91)) (= x_102 x_85)))) ?v_197) ?v_219) ?v_198) ?v_220) ?v_203) ?v_204) ?v_205) ?v_206) ?v_207) (and (and (and (and (and (and (and (and (and (= x_106 1) (or (or (and (and (and (and (and (= x_108 0) ?v_199) ?v_215) ?v_201) ?v_197) ?v_198) (and (and (and (and (and (= x_108 1) ?v_199) ?v_214) ?v_200) ?v_202) ?v_197)) (and (and (and (and (= x_108 2) (not ?v_199)) (ite (or ?v_217 ?v_216) (or ?v_200 ?v_201) (= x_98 x_87))) (= x_104 (+ x_90 1))) (= x_103 (ite ?v_201 1 0))))) ?v_222) (ite ?v_161 (and (<= (+ x_88 ?v_6) x_105) (<= x_105 (+ (+ x_88 x_51) 1))) (ite ?v_202 (and (<= (+ x_88 ?v_46) x_105) (<= x_105 (+ x_88 ?v_47))) (and (<= (+ x_88 ?v_48) x_105) (<= x_105 (+ x_88 ?v_49)))))) ?v_218) ?v_203) ?v_204) ?v_205) ?v_206) ?v_207)) (and (and (and (and (and (and (and (and (= x_106 2) (or (and (and (and (and (= x_109 0) ?v_208) ?v_209) (= x_99 (+ x_88 x_53))) x_20) (and (and (and (and (= x_109 1) ?v_208) x_18) (= x_99 (+ x_88 ?v_56))) ?v_171))) (or (and (and (and (= x_110 0) ?v_211) (or (= x_100 0) ?v_213)) ?v_210) (and (and (= x_110 1) (not ?v_211)) ?v_205))) (or (or (or (and (and (and (and (= x_111 0) ?v_209) ?v_212) ?v_174) ?v_207) (and (and (and (and (= x_111 1) ?v_209) ?v_212) ?v_179) (= x_21 0))) (and (and (and (and (= x_111 2) ?v_209) (< x_19 9)) (= x_101 (ite (or ?v_213 (= x_19 8)) (ite ?v_214 3 x_87) (ite ?v_215 2 x_87)))) (= x_21 (+ x_19 1)))) (and (and (and (= x_111 3) x_18) (= x_101 (ite ?v_216 1 (ite ?v_217 0 x_87)))) ?v_206))) ?v_218) ?v_197) ?v_219) ?v_198) ?v_220))) (or (or (or (or (and (and ?v_223 (or (or ?v_231 ?v_232) ?v_234)) ?v_185) (and (and ?v_223 (or (and ?v_224 (not ?v_225)) (and ?v_226 ?v_227))) ?v_192)) (and (and (and (and (and ?v_223 ?v_221) ?v_222) ?v_228) ?v_225) ?v_229)) (and ?v_230 ?v_192)) (and (and ?v_267 (or (or (and ?v_231 ?v_233) (and ?v_232 ?v_233)) (and ?v_234 ?v_233))) ?v_192))) (or (or (and (and (and (and (and (and (and (and (and (and (= x_92 0) (or (and (and (and (= x_93 0) (< x_74 x_77)) (<= x_77 x_71)) (= x_88 x_77)) (and (and (and (= x_93 1) (< x_74 x_71)) (<= x_71 x_77)) (= x_88 x_71)))) ?v_235) ?v_257) ?v_236) ?v_258) ?v_241) ?v_242) ?v_243) ?v_244) ?v_245) (and (and (and (and (and (and (and (and (and (= x_92 1) (or (or (and (and (and (and (and (= x_94 0) ?v_237) ?v_253) ?v_239) ?v_235) ?v_236) (and (and (and (and (and (= x_94 1) ?v_237) ?v_252) ?v_238) ?v_240) ?v_235)) (and (and (and (and (= x_94 2) (not ?v_237)) (ite (or ?v_255 ?v_254) (or ?v_238 ?v_239) (= x_84 x_73))) (= x_90 (+ x_76 1))) (= x_89 (ite ?v_239 1 0))))) ?v_260) (ite ?v_199 (and (<= (+ x_74 ?v_6) x_91) (<= x_91 (+ (+ x_74 x_51) 1))) (ite ?v_240 (and (<= (+ x_74 ?v_46) x_91) (<= x_91 (+ x_74 ?v_47))) (and (<= (+ x_74 ?v_48) x_91) (<= x_91 (+ x_74 ?v_49)))))) ?v_256) ?v_241) ?v_242) ?v_243) ?v_244) ?v_245)) (and (and (and (and (and (and (and (and (= x_92 2) (or (and (and (and (and (= x_95 0) ?v_246) ?v_247) (= x_85 (+ x_74 x_53))) x_18) (and (and (and (and (= x_95 1) ?v_246) x_16) (= x_85 (+ x_74 ?v_56))) ?v_209))) (or (and (and (and (= x_96 0) ?v_249) (or (= x_86 0) ?v_251)) ?v_248) (and (and (= x_96 1) (not ?v_249)) ?v_243))) (or (or (or (and (and (and (and (= x_97 0) ?v_247) ?v_250) ?v_212) ?v_245) (and (and (and (and (= x_97 1) ?v_247) ?v_250) ?v_217) (= x_19 0))) (and (and (and (and (= x_97 2) ?v_247) (< x_17 9)) (= x_87 (ite (or ?v_251 (= x_17 8)) (ite ?v_252 3 x_73) (ite ?v_253 2 x_73)))) (= x_19 (+ x_17 1)))) (and (and (and (= x_97 3) x_16) (= x_87 (ite ?v_254 1 (ite ?v_255 0 x_73)))) ?v_244))) ?v_256) ?v_235) ?v_257) ?v_236) ?v_258))) (or (or (or (or (and (and ?v_261 (or (or ?v_269 ?v_270) ?v_272)) ?v_223) (and (and ?v_261 (or (and ?v_262 (not ?v_263)) (and ?v_264 ?v_265))) ?v_230)) (and (and (and (and (and ?v_261 ?v_259) ?v_260) ?v_266) ?v_263) ?v_267)) (and ?v_268 ?v_230)) (and (and ?v_305 (or (or (and ?v_269 ?v_271) (and ?v_270 ?v_271)) (and ?v_272 ?v_271))) ?v_230))) (or (or (and (and (and (and (and (and (and (and (and (and (= x_78 0) (or (and (and (and (= x_79 0) (< x_60 x_63)) (<= x_63 x_57)) (= x_74 x_63)) (and (and (and (= x_79 1) (< x_60 x_57)) (<= x_57 x_63)) (= x_74 x_57)))) ?v_273) ?v_295) ?v_274) ?v_296) ?v_279) ?v_280) ?v_281) ?v_282) ?v_283) (and (and (and (and (and (and (and (and (and (= x_78 1) (or (or (and (and (and (and (and (= x_80 0) ?v_275) ?v_291) ?v_277) ?v_273) ?v_274) (and (and (and (and (and (= x_80 1) ?v_275) ?v_290) ?v_276) ?v_278) ?v_273)) (and (and (and (and (= x_80 2) (not ?v_275)) (ite (or ?v_293 ?v_292) (or ?v_276 ?v_277) (= x_70 x_59))) (= x_76 (+ x_62 1))) (= x_75 (ite ?v_277 1 0))))) ?v_298) (ite ?v_237 (and (<= (+ x_60 ?v_6) x_77) (<= x_77 (+ (+ x_60 x_51) 1))) (ite ?v_278 (and (<= (+ x_60 ?v_46) x_77) (<= x_77 (+ x_60 ?v_47))) (and (<= (+ x_60 ?v_48) x_77) (<= x_77 (+ x_60 ?v_49)))))) ?v_294) ?v_279) ?v_280) ?v_281) ?v_282) ?v_283)) (and (and (and (and (and (and (and (and (= x_78 2) (or (and (and (and (and (= x_81 0) ?v_284) ?v_285) (= x_71 (+ x_60 x_53))) x_16) (and (and (and (and (= x_81 1) ?v_284) x_14) (= x_71 (+ x_60 ?v_56))) ?v_247))) (or (and (and (and (= x_82 0) ?v_287) (or (= x_72 0) ?v_289)) ?v_286) (and (and (= x_82 1) (not ?v_287)) ?v_281))) (or (or (or (and (and (and (and (= x_83 0) ?v_285) ?v_288) ?v_250) ?v_283) (and (and (and (and (= x_83 1) ?v_285) ?v_288) ?v_255) (= x_17 0))) (and (and (and (and (= x_83 2) ?v_285) (< x_15 9)) (= x_73 (ite (or ?v_289 (= x_15 8)) (ite ?v_290 3 x_59) (ite ?v_291 2 x_59)))) (= x_17 (+ x_15 1)))) (and (and (and (= x_83 3) x_14) (= x_73 (ite ?v_292 1 (ite ?v_293 0 x_59)))) ?v_282))) ?v_294) ?v_273) ?v_295) ?v_274) ?v_296))) (or (or (or (or (and (and ?v_299 (or (or ?v_307 ?v_308) ?v_310)) ?v_261) (and (and ?v_299 (or (and ?v_300 (not ?v_301)) (and ?v_302 ?v_303))) ?v_268)) (and (and (and (and (and ?v_299 ?v_297) ?v_298) ?v_304) ?v_301) ?v_305)) (and ?v_306 ?v_268)) (and (and ?v_343 (or (or (and ?v_307 ?v_309) (and ?v_308 ?v_309)) (and ?v_310 ?v_309))) ?v_268))) (or (or (and (and (and (and (and (and (and (and (and (and (= x_64 0) (or (and (and (and (= x_65 0) (< x_41 x_46)) (<= x_46 x_34)) (= x_60 x_46)) (and (and (and (= x_65 1) (< x_41 x_34)) (<= x_34 x_46)) (= x_60 x_34)))) ?v_311) ?v_333) ?v_312) ?v_334) ?v_317) ?v_318) ?v_319) ?v_320) ?v_321) (and (and (and (and (and (and (and (and (and (= x_64 1) (or (or (and (and (and (and (and (= x_66 0) ?v_313) ?v_329) ?v_315) ?v_311) ?v_312) (and (and (and (and (and (= x_66 1) ?v_313) ?v_328) ?v_314) ?v_316) ?v_311)) (and (and (and (and (= x_66 2) (not ?v_313)) (ite (or ?v_331 ?v_330) (or ?v_314 ?v_315) (= x_56 x_39))) (= x_62 (+ x_45 1))) (= x_61 (ite ?v_315 1 0))))) ?v_336) (ite ?v_275 (and (<= (+ x_41 ?v_6) x_63) (<= x_63 (+ (+ x_41 x_51) 1))) (ite ?v_316 (and (<= (+ x_41 ?v_46) x_63) (<= x_63 (+ x_41 ?v_47))) (and (<= (+ x_41 ?v_48) x_63) (<= x_63 (+ x_41 ?v_49)))))) ?v_332) ?v_317) ?v_318) ?v_319) ?v_320) ?v_321)) (and (and (and (and (and (and (and (and (= x_64 2) (or (and (and (and (and (= x_67 0) ?v_322) ?v_323) (= x_57 (+ x_41 x_53))) x_14) (and (and (and (and (= x_67 1) ?v_322) x_12) (= x_57 (+ x_41 ?v_56))) ?v_285))) (or (and (and (and (= x_68 0) ?v_325) (or (= x_58 0) ?v_327)) ?v_324) (and (and (= x_68 1) (not ?v_325)) ?v_319))) (or (or (or (and (and (and (and (= x_69 0) ?v_323) ?v_326) ?v_288) ?v_321) (and (and (and (and (= x_69 1) ?v_323) ?v_326) ?v_293) (= x_15 0))) (and (and (and (and (= x_69 2) ?v_323) (< x_13 9)) (= x_59 (ite (or ?v_327 (= x_13 8)) (ite ?v_328 3 x_39) (ite ?v_329 2 x_39)))) (= x_15 (+ x_13 1)))) (and (and (and (= x_69 3) x_12) (= x_59 (ite ?v_330 1 (ite ?v_331 0 x_39)))) ?v_320))) ?v_332) ?v_311) ?v_333) ?v_312) ?v_334))) (or (or (or (or (and (and ?v_337 (or (or ?v_345 ?v_346) ?v_348)) ?v_299) (and (and ?v_337 (or (and ?v_338 (not ?v_339)) (and ?v_340 ?v_341))) ?v_306)) (and (and (and (and (and ?v_337 ?v_335) ?v_336) ?v_342) ?v_339) ?v_343)) (and ?v_344 ?v_306)) (and (and ?v_381 (or (or (and ?v_345 ?v_347) (and ?v_346 ?v_347)) (and ?v_348 ?v_347))) ?v_306))) (or (or (and (and (and (and (and (and (and (and (and (and (= x_48 0) (or (and (and (and (= x_49 0) (< x_36 x_47)) (<= x_47 x_35)) (= x_41 x_47)) (and (and (and (= x_49 1) (< x_36 x_35)) (<= x_35 x_47)) (= x_41 x_35)))) ?v_349) ?v_371) ?v_350) ?v_372) ?v_355) ?v_356) ?v_357) ?v_358) ?v_359) (and (and (and (and (and (and (and (and (and (= x_48 1) (or (or (and (and (and (and (and (= x_50 0) ?v_351) ?v_367) ?v_353) ?v_349) ?v_350) (and (and (and (and (and (= x_50 1) ?v_351) ?v_366) ?v_352) ?v_354) ?v_349)) (and (and (and (and (= x_50 2) (not ?v_351)) (ite (or ?v_369 ?v_368) (or ?v_352 ?v_353) (= x_33 x_40))) (= x_45 (+ x_32 1))) (= x_42 (ite ?v_353 1 0))))) ?v_374) (ite ?v_313 (and (<= (+ x_36 ?v_6) x_46) (<= x_46 (+ (+ x_36 x_51) 1))) (ite ?v_354 (and (<= (+ x_36 ?v_46) x_46) (<= x_46 (+ x_36 ?v_47))) (and (<= (+ x_36 ?v_48) x_46) (<= x_46 (+ x_36 ?v_49)))))) ?v_370) ?v_355) ?v_356) ?v_357) ?v_358) ?v_359)) (and (and (and (and (and (and (and (and (= x_48 2) (or (and (and (and (and (= x_52 0) ?v_360) ?v_361) (= x_34 (+ x_36 x_53))) x_12) (and (and (and (and (= x_52 1) ?v_360) x_10) (= x_34 (+ x_36 ?v_56))) ?v_323))) (or (and (and (and (= x_54 0) ?v_363) (or (= x_37 0) ?v_365)) ?v_362) (and (and (= x_54 1) (not ?v_363)) ?v_357))) (or (or (or (and (and (and (and (= x_55 0) ?v_361) ?v_364) ?v_326) ?v_359) (and (and (and (and (= x_55 1) ?v_361) ?v_364) ?v_331) (= x_13 0))) (and (and (and (and (= x_55 2) ?v_361) (< x_11 9)) (= x_39 (ite (or ?v_365 (= x_11 8)) (ite ?v_366 3 x_40) (ite ?v_367 2 x_40)))) (= x_13 (+ x_11 1)))) (and (and (and (= x_55 3) x_10) (= x_39 (ite ?v_368 1 (ite ?v_369 0 x_40)))) ?v_358))) ?v_370) ?v_349) ?v_371) ?v_350) ?v_372))) (or (or (or (or (and (and ?v_375 (or (or ?v_383 ?v_384) ?v_386)) ?v_337) (and (and ?v_375 (or (and ?v_376 (not ?v_377)) (and ?v_378 ?v_379))) ?v_344)) (and (and (and (and (and ?v_375 ?v_373) ?v_374) ?v_380) ?v_377) ?v_381)) (and ?v_382 ?v_344)) (and (and (= x_0 0) (or (or (and ?v_383 ?v_385) (and ?v_384 ?v_385)) (and ?v_386 ?v_385))) ?v_344))) ?v_35)))))))))))))))))))))))))))))))))))))))))))))
+(check-sat)
+(exit)
diff --git a/tests/unsat/reg_lra_fm1.smt2 b/tests/unsat/reg_lra_fm1.smt2
new file mode 100644
index 00000000..bee80771
--- /dev/null
+++ b/tests/unsat/reg_lra_fm1.smt2
@@ -0,0 +1,36 @@
+
+; expect: unsat
+; intermediate problem in tests/unsat/clocksynchro_2clocks.worst_case_skew.base.smt2
+
+(set-logic QF_LRA)
+(declare-fun x_0 () Real)
+(declare-fun x_1 () Real)
+(declare-fun x_2 () Real)
+(declare-fun x_3 () Real)
+(declare-fun x_4 () Real)
+(declare-fun x_5 () Real)
+(declare-fun x_6 () Real)
+(declare-fun x_7 () Real)
+
+(assert (< (+ (/ 2335 666) x_5 x_6 (* (/ 2 999) x_7) (* (/ 2 999) x_4)) 0))
+(assert (<= (+ (- (/ 1001 1000)) (* -1 x_0) x_2) 0))
+(assert (<= (+ (/ 999 1000) x_0 (* -1 x_2)) 0))
+(assert (<= (+ (- (/ 1001 1000)) (* -1 x_0) x_1) 0))
+(assert (<= (+ (/ 999 1000) x_0 (- 0 x_1)) 0))
+(assert (= x_0 0))
+(assert
+  (<= (+
+    (/ 1502501 999000)
+    (* (/ 1001 999) x_5)
+    (* (/ 1001 999) x_6)
+    (* -1 x_7)
+    (* (/ 1001 999) x_3))
+    0))
+
+(assert (< (+ (/ 1001 2) (* (/ 999 2) x_6) x_7 (* (/ -999 2) x_4)) 0))
+(assert (<= (+ (/ 1001 999) x_5 (* -1 x_6) (* (/ 1001 1998) x_4)) 0))
+(assert (< (* -1 x_5) 0))
+(assert (< (* -1 x_4) 0))
+(assert (< (* -1 x_3) 0))
+
+(check-sat)
diff --git a/tests/unsat/smtlib.624916.smt2 b/tests/unsat/smtlib.624916.smt2
new file mode 100644
index 00000000..e22880db
--- /dev/null
+++ b/tests/unsat/smtlib.624916.smt2
@@ -0,0 +1,16 @@
+(set-info :smt-lib-version 2.6)
+(set-logic QF_UFLRA)
+(set-info :source |Benchmarks from the paper: "Extending Sledgehammer with SMT Solvers" by Jasmin Blanchette, Sascha Bohme, and Lawrence C. Paulson, CADE 2011.  Translated to SMT2 by Andrew Reynolds and Morgan Deters.|)
+(set-info :category "industrial")
+(set-info :status unsat)
+(declare-sort S1 0)
+(declare-fun f1 () S1)
+(declare-fun f2 () S1)
+(declare-fun f3 (Real) Real)
+(declare-fun f4 () Real)
+(declare-fun f5 () Real)
+(assert (not (= f1 f2)))
+(assert (= (f3 f4) (- 1)))
+(assert (not (=> (= f5 f4) (not (= (f3 f5) 1.0)))))
+(check-sat)
+(exit)