diff options
Diffstat (limited to 'test/regress/regress0/simplification_bug4.smt2')
-rw-r--r-- | test/regress/regress0/simplification_bug4.smt2 | 295 |
1 files changed, 0 insertions, 295 deletions
diff --git a/test/regress/regress0/simplification_bug4.smt2 b/test/regress/regress0/simplification_bug4.smt2 deleted file mode 100644 index 0d62d6921..000000000 --- a/test/regress/regress0/simplification_bug4.smt2 +++ /dev/null @@ -1,295 +0,0 @@ -(set-logic QF_LIA) -;; Simplified benchmark, derived from NuSMV output durationThm_1.bmc_k100.smt2 -;; -;; Original version generated by Alberto Griggio <griggio@fbk.eu> -;; on Fri Feb 4 15:56:12 2011 -(declare-fun sb_0__AT0 () Bool) -(declare-fun si_0__AT0 () Int) -(declare-fun si_1__AT0 () Int) -(declare-fun sb_1__AT0 () Bool) -(declare-fun si_2__AT0 () Int) -(declare-fun si_3__AT0 () Int) -(declare-fun sb_2__AT0 () Bool) -(declare-fun si_4__AT0 () Int) -(declare-fun si_5__AT0 () Int) -(declare-fun sb_3__AT0 () Bool) -(declare-fun sb_4__AT0 () Bool) -(declare-fun sb_5__AT0 () Bool) -(declare-fun si_6__AT0 () Int) -(declare-fun si_7__AT0 () Int) -(declare-fun si_8__AT0 () Int) -(declare-fun si_9__AT0 () Int) -(declare-fun si_10__AT0 () Int) -(declare-fun si_11__AT0 () Int) -(declare-fun sb_6__AT0 () Bool) -(declare-fun sb_7__AT0 () Bool) -(declare-fun si_12__AT0 () Int) -(declare-fun si_13__AT0 () Int) -(declare-fun si_14__AT0 () Int) -(assert (let ((.def_61 (= si_2__AT0 si_4__AT0))) -(let ((.def_60 (= si_3__AT0 si_5__AT0))) -(let ((.def_62 (and .def_60 .def_61))) -(let ((.def_63 (and sb_2__AT0 .def_62))) -(let ((.def_59 (= si_8__AT0 0))) -(let ((.def_64 (and .def_59 .def_63))) -(let ((.def_58 (= si_11__AT0 0))) -(let ((.def_65 (and .def_58 .def_64))) -(let ((.def_53 (<= 1 si_0__AT0))) -(let ((.def_52 (<= 1 si_1__AT0))) -(let ((.def_54 (and .def_52 .def_53))) -(let ((.def_48 (<= si_0__AT0 si_6__AT0))) -(let ((.def_49 (not .def_48))) -(let ((.def_50 (or sb_4__AT0 .def_49))) -(let ((.def_55 (and .def_50 .def_54))) -(let ((.def_45 (<= si_1__AT0 si_9__AT0))) -(let ((.def_46 (not .def_45))) -(let ((.def_47 (or sb_5__AT0 .def_46))) -(let ((.def_56 (and .def_47 .def_55))) -(let ((.def_57 (= sb_7__AT0 .def_56))) -(let ((.def_66 (and .def_57 .def_65))) -(let ((.def_44 (= si_14__AT0 0))) -(let ((.def_67 (and .def_44 .def_66))) -(let ((.def_33 (not sb_1__AT0))) -(let ((.def_34 (or sb_2__AT0 .def_33))) -(let ((.def_35 (= sb_0__AT0 .def_34))) -(let ((.def_32 (= si_0__AT0 si_2__AT0))) -(let ((.def_36 (and .def_32 .def_35))) -(let ((.def_31 (= si_1__AT0 si_3__AT0))) -(let ((.def_37 (and .def_31 .def_36))) -(let ((.def_30 (= sb_1__AT0 sb_6__AT0))) -(let ((.def_38 (and .def_30 .def_37))) -(let ((.def_29 (= si_6__AT0 si_8__AT0))) -(let ((.def_39 (and .def_29 .def_38))) -(let ((.def_28 (= si_9__AT0 si_11__AT0))) -(let ((.def_40 (and .def_28 .def_39))) -(let ((.def_27 (= sb_6__AT0 sb_7__AT0))) -(let ((.def_41 (and .def_27 .def_40))) -(let ((.def_26 (= si_12__AT0 si_14__AT0))) -(let ((.def_42 (and .def_26 .def_41))) -(let ((.def_68 (and .def_42 .def_67))) -.def_68 -)))))))))))))))))))))))))))))))))))))))))) - -; (push 1) -; (assert (let ((.def_69 (not sb_0__AT0))) -; .def_69 -; )) -; (check-sat) -; (pop 1) - -(declare-fun sb_0__AT1 () Bool) -(declare-fun si_0__AT1 () Int) -(declare-fun si_1__AT1 () Int) -(declare-fun sb_1__AT1 () Bool) -(declare-fun si_2__AT1 () Int) -(declare-fun si_3__AT1 () Int) -(declare-fun sb_2__AT1 () Bool) -(declare-fun si_4__AT1 () Int) -(declare-fun si_5__AT1 () Int) -(declare-fun sb_3__AT1 () Bool) -(declare-fun sb_4__AT1 () Bool) -(declare-fun sb_5__AT1 () Bool) -(declare-fun si_6__AT1 () Int) -(declare-fun si_7__AT1 () Int) -(declare-fun si_8__AT1 () Int) -(declare-fun si_9__AT1 () Int) -(declare-fun si_10__AT1 () Int) -(declare-fun si_11__AT1 () Int) -(declare-fun sb_6__AT1 () Bool) -(declare-fun sb_7__AT1 () Bool) -(declare-fun si_12__AT1 () Int) -(declare-fun si_13__AT1 () Int) -(declare-fun si_14__AT1 () Int) -(assert (let ((.def_163 (= si_0__AT0 si_2__AT1))) -(let ((.def_162 (= si_1__AT0 si_3__AT1))) -(let ((.def_164 (and .def_162 .def_163))) -(let ((.def_155 (* (- 1) si_12__AT1))) -(let ((.def_156 (+ si_1__AT1 .def_155))) -(let ((.def_157 (+ si_0__AT1 .def_156))) -(let ((.def_158 (<= .def_157 0))) -(let ((.def_159 (not .def_158))) -(let ((.def_160 (or sb_5__AT1 .def_159))) -(let ((.def_161 (= sb_2__AT1 .def_160))) -(let ((.def_165 (and .def_161 .def_164))) -(let ((.def_147 (* (- 1) si_7__AT1))) -(let ((.def_148 (+ si_6__AT0 .def_147))) -(let ((.def_149 (= .def_148 (- 1)))) -(let ((.def_142 (not sb_3__AT0))) -(let ((.def_150 (or .def_142 .def_149))) -(let ((.def_144 (= si_7__AT1 0))) -(let ((.def_145 (or sb_3__AT0 .def_144))) -(let ((.def_151 (and .def_145 .def_150))) -(let ((.def_139 (* (- 1) si_13__AT1))) -(let ((.def_140 (+ si_12__AT0 .def_139))) -(let ((.def_141 (= .def_140 (- 1)))) -(let ((.def_143 (or .def_141 .def_142))) -(let ((.def_152 (and .def_143 .def_151))) -(let ((.def_136 (= si_13__AT1 0))) -(let ((.def_137 (or sb_3__AT0 .def_136))) -(let ((.def_153 (and .def_137 .def_152))) -(let ((.def_166 (and .def_153 .def_165))) -(let ((.def_133 (not sb_4__AT0))) -(let ((.def_130 (* (- 1) si_10__AT1))) -(let ((.def_131 (+ si_9__AT0 .def_130))) -(let ((.def_132 (= .def_131 (- 1)))) -(let ((.def_134 (or .def_132 .def_133))) -(let ((.def_126 (= si_10__AT1 0))) -(let ((.def_127 (or sb_4__AT0 .def_126))) -(let ((.def_135 (and .def_127 .def_134))) -(let ((.def_167 (and .def_135 .def_166))) -(let ((.def_125 (= si_7__AT1 si_8__AT1))) -(let ((.def_168 (and .def_125 .def_167))) -(let ((.def_124 (= si_10__AT1 si_11__AT1))) -(let ((.def_169 (and .def_124 .def_168))) -(let ((.def_118 (<= 1 si_0__AT1))) -(let ((.def_117 (<= 1 si_1__AT1))) -(let ((.def_119 (and .def_117 .def_118))) -(let ((.def_114 (<= si_0__AT1 si_6__AT1))) -(let ((.def_115 (not .def_114))) -(let ((.def_116 (or sb_4__AT1 .def_115))) -(let ((.def_120 (and .def_116 .def_119))) -(let ((.def_111 (<= si_1__AT1 si_9__AT1))) -(let ((.def_112 (not .def_111))) -(let ((.def_113 (or sb_5__AT1 .def_112))) -(let ((.def_121 (and .def_113 .def_120))) -(let ((.def_122 (and sb_6__AT0 .def_121))) -(let ((.def_123 (= sb_7__AT1 .def_122))) -(let ((.def_170 (and .def_123 .def_169))) -(let ((.def_110 (= si_13__AT1 si_14__AT1))) -(let ((.def_171 (and .def_110 .def_170))) -(let ((.def_100 (not sb_1__AT1))) -(let ((.def_101 (or sb_2__AT1 .def_100))) -(let ((.def_102 (= sb_0__AT1 .def_101))) -(let ((.def_99 (= si_0__AT1 si_2__AT1))) -(let ((.def_103 (and .def_99 .def_102))) -(let ((.def_98 (= si_1__AT1 si_3__AT1))) -(let ((.def_104 (and .def_98 .def_103))) -(let ((.def_97 (= sb_1__AT1 sb_6__AT1))) -(let ((.def_105 (and .def_97 .def_104))) -(let ((.def_96 (= si_6__AT1 si_8__AT1))) -(let ((.def_106 (and .def_96 .def_105))) -(let ((.def_95 (= si_9__AT1 si_11__AT1))) -(let ((.def_107 (and .def_95 .def_106))) -(let ((.def_94 (= sb_6__AT1 sb_7__AT1))) -(let ((.def_108 (and .def_94 .def_107))) -(let ((.def_93 (= si_12__AT1 si_14__AT1))) -(let ((.def_109 (and .def_93 .def_108))) -(let ((.def_172 (and .def_109 .def_171))) -(let ((.def_173 (and sb_0__AT0 .def_172))) -.def_173 -))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) - -; (push 1) -; (assert (let ((.def_174 (not sb_0__AT1))) -; .def_174 -; )) -; (check-sat) -; (pop 1) - -(declare-fun sb_0__AT2 () Bool) -(declare-fun si_0__AT2 () Int) -(declare-fun si_1__AT2 () Int) -(declare-fun sb_1__AT2 () Bool) -(declare-fun si_2__AT2 () Int) -(declare-fun si_3__AT2 () Int) -(declare-fun sb_2__AT2 () Bool) -(declare-fun si_4__AT2 () Int) -(declare-fun si_5__AT2 () Int) -(declare-fun sb_3__AT2 () Bool) -(declare-fun sb_4__AT2 () Bool) -(declare-fun sb_5__AT2 () Bool) -(declare-fun si_6__AT2 () Int) -(declare-fun si_7__AT2 () Int) -(declare-fun si_8__AT2 () Int) -(declare-fun si_9__AT2 () Int) -(declare-fun si_10__AT2 () Int) -(declare-fun si_11__AT2 () Int) -(declare-fun sb_6__AT2 () Bool) -(declare-fun sb_7__AT2 () Bool) -(declare-fun si_12__AT2 () Int) -(declare-fun si_13__AT2 () Int) -(declare-fun si_14__AT2 () Int) -(assert (let ((.def_267 (= si_0__AT1 si_2__AT2))) -(let ((.def_266 (= si_1__AT1 si_3__AT2))) -(let ((.def_268 (and .def_266 .def_267))) -(let ((.def_259 (* (- 1) si_12__AT2))) -(let ((.def_260 (+ si_1__AT2 .def_259))) -(let ((.def_261 (+ si_0__AT2 .def_260))) -(let ((.def_262 (<= .def_261 0))) -(let ((.def_263 (not .def_262))) -(let ((.def_264 (or sb_5__AT2 .def_263))) -(let ((.def_265 (= sb_2__AT2 .def_264))) -(let ((.def_269 (and .def_265 .def_268))) -(let ((.def_251 (* (- 1) si_7__AT2))) -(let ((.def_252 (+ si_6__AT1 .def_251))) -(let ((.def_253 (= .def_252 (- 1)))) -(let ((.def_246 (not sb_3__AT1))) -(let ((.def_254 (or .def_246 .def_253))) -(let ((.def_248 (= si_7__AT2 0))) -(let ((.def_249 (or sb_3__AT1 .def_248))) -(let ((.def_255 (and .def_249 .def_254))) -(let ((.def_243 (* (- 1) si_13__AT2))) -(let ((.def_244 (+ si_12__AT1 .def_243))) -(let ((.def_245 (= .def_244 (- 1)))) -(let ((.def_247 (or .def_245 .def_246))) -(let ((.def_256 (and .def_247 .def_255))) -(let ((.def_240 (= si_13__AT2 0))) -(let ((.def_241 (or sb_3__AT1 .def_240))) -(let ((.def_257 (and .def_241 .def_256))) -(let ((.def_270 (and .def_257 .def_269))) -(let ((.def_237 (not sb_4__AT1))) -(let ((.def_234 (* (- 1) si_10__AT2))) -(let ((.def_235 (+ si_9__AT1 .def_234))) -(let ((.def_236 (= .def_235 (- 1)))) -(let ((.def_238 (or .def_236 .def_237))) -(let ((.def_231 (= si_10__AT2 0))) -(let ((.def_232 (or sb_4__AT1 .def_231))) -(let ((.def_239 (and .def_232 .def_238))) -(let ((.def_271 (and .def_239 .def_270))) -(let ((.def_230 (= si_7__AT2 si_8__AT2))) -(let ((.def_272 (and .def_230 .def_271))) -(let ((.def_229 (= si_10__AT2 si_11__AT2))) -(let ((.def_273 (and .def_229 .def_272))) -(let ((.def_223 (<= 1 si_0__AT2))) -(let ((.def_222 (<= 1 si_1__AT2))) -(let ((.def_224 (and .def_222 .def_223))) -(let ((.def_219 (<= si_0__AT2 si_6__AT2))) -(let ((.def_220 (not .def_219))) -(let ((.def_221 (or sb_4__AT2 .def_220))) -(let ((.def_225 (and .def_221 .def_224))) -(let ((.def_216 (<= si_1__AT2 si_9__AT2))) -(let ((.def_217 (not .def_216))) -(let ((.def_218 (or sb_5__AT2 .def_217))) -(let ((.def_226 (and .def_218 .def_225))) -(let ((.def_227 (and sb_6__AT1 .def_226))) -(let ((.def_228 (= sb_7__AT2 .def_227))) -(let ((.def_274 (and .def_228 .def_273))) -(let ((.def_215 (= si_13__AT2 si_14__AT2))) -(let ((.def_275 (and .def_215 .def_274))) -(let ((.def_205 (not sb_1__AT2))) -(let ((.def_206 (or sb_2__AT2 .def_205))) -(let ((.def_207 (= sb_0__AT2 .def_206))) -(let ((.def_204 (= si_0__AT2 si_2__AT2))) -(let ((.def_208 (and .def_204 .def_207))) -(let ((.def_203 (= si_1__AT2 si_3__AT2))) -(let ((.def_209 (and .def_203 .def_208))) -(let ((.def_202 (= sb_1__AT2 sb_6__AT2))) -(let ((.def_210 (and .def_202 .def_209))) -(let ((.def_201 (= si_6__AT2 si_8__AT2))) -(let ((.def_211 (and .def_201 .def_210))) -(let ((.def_200 (= si_9__AT2 si_11__AT2))) -(let ((.def_212 (and .def_200 .def_211))) -(let ((.def_199 (= sb_6__AT2 sb_7__AT2))) -(let ((.def_213 (and .def_199 .def_212))) -(let ((.def_198 (= si_12__AT2 si_14__AT2))) -(let ((.def_214 (and .def_198 .def_213))) -(let ((.def_276 (and .def_214 .def_275))) -(let ((.def_277 (and sb_0__AT1 .def_276))) -.def_277 -))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) - -(push 1) -(assert (not sb_0__AT2)) -(check-sat) -(pop 1) - |