summaryrefslogtreecommitdiff
path: root/test/regress/regress0/quantifiers/florian-case-ax.smt2
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/quantifiers/florian-case-ax.smt2')
-rw-r--r--test/regress/regress0/quantifiers/florian-case-ax.smt2168
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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback