diff options
Diffstat (limited to 'test/regress/regress0/quantifiers/florian-case-ax.smt2')
-rw-r--r-- | test/regress/regress0/quantifiers/florian-case-ax.smt2 | 168 |
1 files changed, 0 insertions, 168 deletions
diff --git a/test/regress/regress0/quantifiers/florian-case-ax.smt2 b/test/regress/regress0/quantifiers/florian-case-ax.smt2 deleted file mode 100644 index 35ebb28e9..000000000 --- a/test/regress/regress0/quantifiers/florian-case-ax.smt2 +++ /dev/null @@ -1,168 +0,0 @@ -(set-logic AUFLIA) -(set-info :status unsat) -(declare-sort U 0) -(declare-fun A (U U U - U U U U - U U U U - U U U U - U U U U - U U U U - U U U U - U U U U - U U U U - U U U U - U U U U - U U U U - U U U U - U U U U - U U - U) (Array Int U)) - -(assert - (forall ((v_184 U) (v_185 U) - (v_186 U) (v_187 U) - (v_188 U) (v_189 U) - (v_190 U) (v_191 U) - (v_192 U) (v_193 U) - (v_194 U) (v_195 U) - (v_196 U) (v_197 U) - (v_198 U) (v_199 U) - (v_200 U) (v_201 U) - (v_202 U) (v_203 U) - (v_204 U) (v_205 U) - (v_206 U) (v_207 U) - (v_208 U) (v_209 U) - (v_210 U) (v_211 U) - (v_212 U) (v_213 U) - (v_214 U) (v_215 U) - (v_216 U) (v_217 U) - (v_218 U) (v_219 U) - (v_220 U) (v_221 U) - (v_222 U) (v_223 U) - (v_224 U) (v_225 U) - (v_226 U) (v_227 U) - (v_228 U) (v_229 U) - (v_230 U) (v_231 U) - (v_232 U) (v_233 U) - (v_234 U) (v_235 U) - (v_236 U) (v_237 U) - (v_238 U) (v_239 U) - (v_240 U) (v_241 U) (v_242 Int)) - (let ((v_183 (A v_184 v_185 v_186 v_187 - v_188 v_189 v_190 v_191 v_192 - v_193 v_194 v_195 v_196 v_197 - v_198 v_199 v_200 v_201 v_202 - v_203 v_204 v_205 v_206 v_207 - v_208 v_209 v_210 v_211 v_212 - v_213 v_214 v_215 v_216 v_217 - v_218 v_219 v_220 v_221 v_222 - v_223 v_224 v_225 v_226 v_227 - v_228 v_229 v_230 v_231 v_232 - v_233 v_234 v_235 v_236 v_237 - v_238 v_239 v_240 v_241))) - (ite (= v_242 59) (= (select v_183 v_242) v_240) - (ite (= v_242 58) (= (select v_183 v_242) v_239) - (ite (= v_242 57) (= (select v_183 v_242) v_238) - (ite (= v_242 56) (= (select v_183 v_242) v_237) - (ite (= v_242 55) (= (select v_183 v_242) v_236) - (ite (= v_242 54) (= (select v_183 v_242) v_235) - (ite (= v_242 53) (= (select v_183 v_242) v_234) - (ite (= v_242 52) (= (select v_183 v_242) v_233) - (ite (= v_242 51) (= (select v_183 v_242) v_232) - (ite (= v_242 50) (= (select v_183 v_242) v_231) - (ite (= v_242 49) (= (select v_183 v_242) v_230) - (ite (= v_242 48) (= (select v_183 v_242) v_229) - (ite (= v_242 47) (= (select v_183 v_242) v_228) - (ite (= v_242 46) (= (select v_183 v_242) v_227) - (ite (= v_242 45) (= (select v_183 v_242) v_226) - (ite (= v_242 44) (= (select v_183 v_242) v_225) - (ite (= v_242 43) (= (select v_183 v_242) v_224) - (ite (= v_242 41) (= (select v_183 v_242) v_223) - (ite (= v_242 40) (= (select v_183 v_242) v_222) - (ite (= v_242 39) (= (select v_183 v_242) v_221) - (ite (= v_242 37) (= (select v_183 v_242) v_220) - (ite (= v_242 36) (= (select v_183 v_242) v_219) - (ite (= v_242 34) (= (select v_183 v_242) v_218) - (ite (= v_242 33) (= (select v_183 v_242) v_217) - (ite (= v_242 32) (= (select v_183 v_242) v_216) - (ite (= v_242 31) (= (select v_183 v_242) v_215) - (ite (= v_242 30) (= (select v_183 v_242) v_214) - (ite (= v_242 29) (= (select v_183 v_242) v_213) - (ite (= v_242 28) (= (select v_183 v_242) v_212) - (ite (= v_242 27) (= (select v_183 v_242) v_211) - (ite (= v_242 26) (= (select v_183 v_242) v_210) - (ite (= v_242 25) (= (select v_183 v_242) v_209) - (ite (= v_242 24) (= (select v_183 v_242) v_208) - (ite (= v_242 23) (= (select v_183 v_242) v_207) - (ite (= v_242 22) (= (select v_183 v_242) v_206) - (ite (= v_242 21) (= (select v_183 v_242) v_205) - (ite (= v_242 20) (= (select v_183 v_242) v_204) - (ite (= v_242 19) (= (select v_183 v_242) v_203) - (ite (= v_242 18) (= (select v_183 v_242) v_202) - (ite (= v_242 17) (= (select v_183 v_242) v_201) - (ite (= v_242 16) (= (select v_183 v_242) v_200) - (ite (= v_242 15) (= (select v_183 v_242) v_199) - (ite (= v_242 14) (= (select v_183 v_242) v_198) - (ite (= v_242 13) (= (select v_183 v_242) v_197) - (ite (= v_242 12) (= (select v_183 v_242) v_196) - (ite (= v_242 11) (= (select v_183 v_242) v_195) - (ite (= v_242 10) (= (select v_183 v_242) v_194) - (ite (= v_242 9) (= (select v_183 v_242) v_193) - (ite (= v_242 8) (= (select v_183 v_242) v_192) - (ite (= v_242 7) (= (select v_183 v_242) v_191) - (ite (= v_242 6) (= (select v_183 v_242) v_190) - (ite (= v_242 5) (= (select v_183 v_242) v_189) - (ite (= v_242 4) (= (select v_183 v_242) v_188) - (ite (= v_242 3) (= (select v_183 v_242) v_187) - (ite (= v_242 2) (= (select v_183 v_242) v_186) - (ite (= v_242 1) (= (select v_183 v_242) v_185) - (ite (= v_242 0) (= (select v_183 v_242) v_184) - (= (select v_183 v_242) v_241))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) - -(declare-const c_184 U) (declare-const c_185 U) -(declare-const c_186 U) (declare-const c_187 U) -(declare-const c_188 U) (declare-const c_189 U) -(declare-const c_190 U) (declare-const c_191 U) -(declare-const c_192 U) (declare-const c_193 U) -(declare-const c_194 U) (declare-const c_195 U) -(declare-const c_196 U) (declare-const c_197 U) -(declare-const c_198 U) (declare-const c_199 U) -(declare-const c_200 U) (declare-const c_201 U) -(declare-const c_202 U) (declare-const c_203 U) -(declare-const c_204 U) (declare-const c_205 U) -(declare-const c_206 U) (declare-const c_207 U) -(declare-const c_208 U) (declare-const c_209 U) -(declare-const c_210 U) (declare-const c_211 U) -(declare-const c_212 U) (declare-const c_213 U) -(declare-const c_214 U) (declare-const c_215 U) -(declare-const c_216 U) (declare-const c_217 U) -(declare-const c_218 U) (declare-const c_219 U) -(declare-const c_220 U) (declare-const c_221 U) -(declare-const c_222 U) (declare-const c_223 U) -(declare-const c_224 U) (declare-const c_225 U) -(declare-const c_226 U) (declare-const c_227 U) -(declare-const c_228 U) (declare-const c_229 U) -(declare-const c_230 U) (declare-const c_231 U) -(declare-const c_232 U) (declare-const c_233 U) -(declare-const c_234 U) (declare-const c_235 U) -(declare-const c_236 U) (declare-const c_237 U) -(declare-const c_238 U) (declare-const c_239 U) -(declare-const c_240 U) (declare-const c_241 U) - -(declare-fun b () Int) -(declare-fun c () U) -(assert (not (= (select (A c_184 c_185 c_186 c_187 - c_188 c_189 c_190 c_191 c_192 - c_193 c_194 c_195 c_196 c_197 - c_198 c_199 c_200 c_201 c_202 - c_203 c_204 c_205 c_206 c_207 - c_208 c_209 c_210 c_211 c_212 - c_213 c_214 c_215 c_216 c_217 - c_218 c_219 c_220 c_221 c_222 - c_223 c_224 c_225 c_226 c_227 - c_228 c_229 c_230 c_231 c_232 - c_233 c_234 c_235 c_236 c_237 - c_238 c_239 c_240 c_241) b) c))) -(assert (and (= b 28) (= c c_212))) - -(check-sat) |