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, 168 insertions, 0 deletions
diff --git a/test/regress/regress0/quantifiers/florian-case-ax.smt2 b/test/regress/regress0/quantifiers/florian-case-ax.smt2
new file mode 100644
index 000000000..35ebb28e9
--- /dev/null
+++ b/test/regress/regress0/quantifiers/florian-case-ax.smt2
@@ -0,0 +1,168 @@
+(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