// x = (p - ax - c) * -1/a
// Add the substitution if not recursive
Assert(elim == Rewriter::rewrite(elim));
- Assert(!elim.hasSubterm(minVar));
- if (!minVar.getType().isInteger() || right.isIntegral()) {
+ if(elim.hasSubterm(minVar)){
+ Debug("simplify") << "TheoryArith::solve(): can't substitute due to recursive pattern with sharing: " << minVar << ":" << elim << endl;
+ }else if (!minVar.getType().isInteger() || right.isIntegral()) {
+ Assert(!elim.hasSubterm(minVar));
// cannot eliminate integers here unless we know the resulting
// substitution is integral
Debug("simplify") << "TheoryArith::solve(): substitution " << minVar << " |-> " << elim << endl;
--- /dev/null
+(set-logic QF_UFIDL)
+(set-info :source |
+Benchmark generated from the verification of programs manipulating linked lists inside UCLID. For more information see:
+"Verifying properties of well-founded linked lists", Shuvendu Lahiri and Shaz Qaader, POPL 2006
+
+This benchmark was automatically translated into SMT-LIB format by Albert Oliveras.
+|)
+(set-info :smt-lib-version 2.0)
+(set-info :category "industrial")
+(set-info :status sat)
+(declare-fun t.l () Int)
+(declare-fun en_LOCATION () Int)
+(declare-fun NULL () Int)
+(declare-fun ZERO () Int)
+(declare-fun i1 () Int)
+(declare-fun t.l0 () Int)
+(declare-fun t.pc () Int)
+(declare-fun t.t () Int)
+(declare-fun PRED_VAR__p_0 () Bool)
+(declare-fun PRED_VAR__p_1 () Bool)
+(declare-fun PRED_VAR__p_2 () Bool)
+(declare-fun PRED_VAR__p_16 () Bool)
+(declare-fun PRED_VAR__p_11 () Bool)
+(declare-fun PRED_VAR__p_10 () Bool)
+(declare-fun PRED_VAR__p_14 () Bool)
+(declare-fun PRED_VAR__p_12 () Bool)
+(declare-fun PRED_VAR__p_15 () Bool)
+(declare-fun PRED_VAR__p_18 () Bool)
+(declare-fun PRED_VAR__p_19 () Bool)
+(declare-fun PRED_VAR__p_3 () Bool)
+(declare-fun PRED_VAR__p_20 () Bool)
+(declare-fun PRED_VAR__p_8 () Bool)
+(declare-fun PRED_VAR__p_9 () Bool)
+(declare-fun t.I_nxt (Int) Int)
+(declare-fun t.I_nxt0 (Int) Int)
+(declare-fun t.data (Int) Int)
+(declare-fun t.nxt (Int) Int)
+(declare-fun t.H_nxt (Int) Bool)
+(declare-fun t.R_nxt (Int Int) Bool)
+(declare-fun t.H_nxt0 (Int) Bool)
+(declare-fun t.R_nxt0 (Int Int) Bool)
+(assert (let ((?v_0 (t.nxt t.l))) (let ((?v_7 (t.H_nxt ?v_0)) (?v_242 (+ 1 (+ 1 (+ 1 (+ 1 en_LOCATION)))))) (let ((?v_1 (= t.pc ?v_242)) (?v_2 (t.R_nxt ?v_0 i1))) (let ((?v_3 (not ?v_1))) (let ((?v_6 (or (and ?v_1 ?v_2) (and ?v_3 ?v_2))) (?v_4 (t.R_nxt t.l i1))) (let ((?v_247 (or (and ?v_1 ?v_4) (and ?v_3 ?v_4))) (?v_112 (= i1 t.l))) (let ((?v_5 (and ?v_247 (not ?v_112))) (?v_8 (t.R_nxt ?v_0 t.l)) (?v_9 (t.R_nxt ?v_0 t.t))) (let ((?v_12 (or (and ?v_1 ?v_9) (and ?v_3 ?v_9))) (?v_10 (t.R_nxt t.l t.t)) (?v_127 (= t.t t.l))) (let ((?v_22 (not ?v_127))) (let ((?v_11 (and (or (and ?v_1 ?v_10) (and ?v_3 ?v_10)) ?v_22)) (?v_13 (t.R_nxt ?v_0 ?v_0))) (let ((?v_16 (or (and ?v_1 ?v_13) (and ?v_3 ?v_13))) (?v_14 (t.R_nxt t.l ?v_0)) (?v_55 (= ?v_0 t.l))) (let ((?v_15 (and (or (and ?v_1 ?v_14) (and ?v_3 ?v_14)) (not ?v_55))) (?v_18 (t.nxt t.t))) (let ((?v_17 (t.R_nxt ?v_0 ?v_18))) (let ((?v_21 (or (and ?v_1 ?v_17) (and ?v_3 ?v_17))) (?v_19 (t.R_nxt t.l ?v_18)) (?v_72 (= ?v_18 t.l))) (let ((?v_20 (and (or (and ?v_1 ?v_19) (and ?v_3 ?v_19)) (not ?v_72))) (?v_31 (t.H_nxt ?v_18)) (?v_147 (= t.pc en_LOCATION))) (let ((?v_23 (and ?v_147 ?v_22)) (?v_24 (t.R_nxt ?v_18 i1))) (let ((?v_26 (not ?v_23))) (let ((?v_25 (and ?v_26 ?v_24))) (let ((?v_30 (or (and ?v_23 (or (and ?v_23 ?v_24) ?v_25)) ?v_25)) (?v_27 (t.R_nxt t.t i1))) (let ((?v_28 (and ?v_26 ?v_27)) (?v_116 (= i1 t.t))) (let ((?v_29 (and (or (and ?v_23 (or (and ?v_23 ?v_27) ?v_28)) ?v_28) (not ?v_116))) (?v_32 (t.R_nxt ?v_18 t.l))) (let ((?v_33 (and ?v_26 ?v_32))) (let ((?v_37 (or (and ?v_23 (or (and ?v_23 ?v_32) ?v_33)) ?v_33)) (?v_34 (t.R_nxt t.t t.l))) (let ((?v_35 (and ?v_26 ?v_34))) (let ((?v_36 (and (or (and ?v_23 (or (and ?v_23 ?v_34) ?v_35)) ?v_35) ?v_22)) (?v_38 (t.R_nxt ?v_18 t.t))) (let ((?v_39 (and ?v_26 ?v_38)) (?v_40 (t.R_nxt ?v_18 ?v_0))) (let ((?v_41 (and ?v_26 ?v_40))) (let ((?v_45 (or (and ?v_23 (or (and ?v_23 ?v_40) ?v_41)) ?v_41)) (?v_42 (t.R_nxt t.t ?v_0))) (let ((?v_43 (and ?v_26 ?v_42)) (?v_60 (= ?v_0 t.t))) (let ((?v_44 (and (or (and ?v_23 (or (and ?v_23 ?v_42) ?v_43)) ?v_43) (not ?v_60))) (?v_46 (t.R_nxt ?v_18 ?v_18))) (let ((?v_47 (and ?v_26 ?v_46))) (let ((?v_51 (or (and ?v_23 (or (and ?v_23 ?v_46) ?v_47)) ?v_47)) (?v_48 (t.R_nxt t.t ?v_18))) (let ((?v_49 (and ?v_26 ?v_48)) (?v_78 (= ?v_18 t.t))) (let ((?v_50 (and (or (and ?v_23 (or (and ?v_23 ?v_48) ?v_49)) ?v_49) (not ?v_78))) (?v_54 (t.I_nxt t.l))) (let ((?v_53 (= ?v_54 i1)) (?v_67 (t.H_nxt i1)) (?v_120 (= i1 ?v_0)) (?v_56 (not ?v_7)) (?v_57 (t.I_nxt ?v_0))) (let ((?v_86 (= i1 ?v_57))) (let ((?v_52 (or (and ?v_67 ?v_120) (and ?v_56 ?v_86))) (?v_59 (= ?v_54 t.l))) (let ((?v_260 (not ?v_59)) (?v_71 (t.H_nxt t.l)) (?v_89 (= ?v_57 t.l))) (let ((?v_58 (or (and ?v_71 ?v_55) (and ?v_56 ?v_89))) (?v_62 (= ?v_54 t.t)) (?v_77 (t.H_nxt t.t)) (?v_93 (= t.t ?v_57))) (let ((?v_61 (or (and ?v_77 ?v_60) (and ?v_56 ?v_93))) (?v_64 (= ?v_54 ?v_0)) (?v_95 (= ?v_0 ?v_57))) (let ((?v_63 (or ?v_7 ?v_95)) (?v_66 (= ?v_54 ?v_18)) (?v_81 (= ?v_18 ?v_0)) (?v_97 (= ?v_18 ?v_57))) (let ((?v_65 (or (and ?v_31 ?v_81) (and ?v_56 ?v_97))) (?v_70 (t.I_nxt t.t))) (let ((?v_69 (= ?v_70 i1)) (?v_123 (= i1 ?v_18)) (?v_73 (not ?v_31)) (?v_74 (t.I_nxt ?v_18))) (let ((?v_99 (= i1 ?v_74))) (let ((?v_68 (or (and ?v_67 ?v_123) (and ?v_73 ?v_99))) (?v_76 (= ?v_70 t.l)) (?v_102 (= ?v_74 t.l))) (let ((?v_75 (or (and ?v_71 ?v_72) (and ?v_73 ?v_102))) (?v_80 (= ?v_70 t.t)) (?v_106 (= t.t ?v_74))) (let ((?v_79 (or (and ?v_77 ?v_78) (and ?v_73 ?v_106))) (?v_83 (= ?v_70 ?v_0)) (?v_108 (= ?v_0 ?v_74))) (let ((?v_82 (or (and ?v_7 ?v_81) (and ?v_73 ?v_108))) (?v_85 (= ?v_70 ?v_18)) (?v_110 (= ?v_18 ?v_74))) (let ((?v_84 (or ?v_31 ?v_110)) (?v_87 (t.nxt ?v_0))) (let ((?v_90 (not (t.H_nxt ?v_87))) (?v_91 (t.I_nxt ?v_87))) (let ((?v_88 (or (and ?v_67 (= i1 ?v_87)) (and ?v_90 (= i1 ?v_91)))) (?v_92 (or (and ?v_71 (= t.l ?v_87)) (and ?v_90 (= t.l ?v_91)))) (?v_94 (or (and ?v_77 (= t.t ?v_87)) (and ?v_90 (= t.t ?v_91)))) (?v_96 (or (and ?v_7 (= ?v_0 ?v_87)) (and ?v_90 (= ?v_0 ?v_91)))) (?v_98 (or (and ?v_31 (= ?v_18 ?v_87)) (and ?v_90 (= ?v_18 ?v_91)))) (?v_100 (t.nxt ?v_18))) (let ((?v_103 (not (t.H_nxt ?v_100))) (?v_104 (t.I_nxt ?v_100))) (let ((?v_101 (or (and ?v_67 (= i1 ?v_100)) (and ?v_103 (= i1 ?v_104)))) (?v_105 (or (and ?v_71 (= t.l ?v_100)) (and ?v_103 (= t.l ?v_104)))) (?v_107 (or (and ?v_77 (= t.t ?v_100)) (and ?v_103 (= t.t ?v_104)))) (?v_109 (or (and ?v_7 (= ?v_0 ?v_100)) (and ?v_103 (= ?v_0 ?v_104)))) (?v_111 (or (and ?v_31 (= ?v_18 ?v_100)) (and ?v_103 (= ?v_18 ?v_104)))) (?v_156 (t.R_nxt i1 i1)) (?v_115 (t.R_nxt i1 t.l)) (?v_113 (t.nxt i1))) (let ((?v_117 (not (t.H_nxt ?v_113)))) (let ((?v_114 (or ?v_112 (and ?v_117 (t.R_nxt ?v_113 t.l)))) (?v_119 (t.R_nxt i1 t.t)) (?v_118 (or ?v_116 (and ?v_117 (t.R_nxt ?v_113 t.t)))) (?v_122 (t.R_nxt i1 ?v_0)) (?v_121 (or ?v_120 (and ?v_117 (t.R_nxt ?v_113 ?v_0)))) (?v_125 (t.R_nxt i1 ?v_18)) (?v_124 (or ?v_123 (and ?v_117 (t.R_nxt ?v_113 ?v_18)))) (?v_149 (not ?v_4)) (?v_126 (or ?v_112 (and ?v_56 ?v_2))) (?v_169 (t.R_nxt t.l t.l)) (?v_190 (not ?v_10)) (?v_128 (or ?v_127 (and ?v_56 ?v_9))) (?v_209 (not ?v_14)) (?v_129 (or ?v_55 (and ?v_56 ?v_13))) (?v_227 (not ?v_19)) (?v_130 (or ?v_72 (and ?v_56 ?v_17))) (?v_157 (not ?v_27)) (?v_131 (or ?v_116 (and ?v_73 ?v_24))) (?v_178 (not ?v_34)) (?v_132 (or ?v_127 (and ?v_73 ?v_32))) (?v_196 (t.R_nxt t.t t.t)) (?v_214 (not ?v_42)) (?v_133 (or ?v_60 (and ?v_73 ?v_40))) (?v_232 (not ?v_48)) (?v_134 (or ?v_78 (and ?v_73 ?v_46))) (?v_135 (or ?v_120 (and ?v_90 (t.R_nxt ?v_87 i1)))) (?v_136 (or ?v_55 (and ?v_90 (t.R_nxt ?v_87 t.l)))) (?v_137 (or ?v_60 (and ?v_90 (t.R_nxt ?v_87 t.t)))) (?v_138 (or ?v_81 (and ?v_90 (t.R_nxt ?v_87 ?v_18)))) (?v_139 (or ?v_123 (and ?v_103 (t.R_nxt ?v_100 i1)))) (?v_140 (or ?v_72 (and ?v_103 (t.R_nxt ?v_100 t.l)))) (?v_141 (or ?v_78 (and ?v_103 (t.R_nxt ?v_100 t.t)))) (?v_142 (or ?v_81 (and ?v_103 (t.R_nxt ?v_100 ?v_0)))) (?v_146 (= (t.I_nxt0 t.l0) t.l0)) (?v_143 (= i1 NULL)) (?v_145 (t.H_nxt0 i1)) (?v_144 (= t.l t.l0)) (?v_168 (= t.l NULL)) (?v_170 (t.H_nxt0 t.l)) (?v_187 (= t.t NULL)) (?v_188 (t.H_nxt0 t.t)) (?v_206 (= ?v_0 NULL)) (?v_207 (t.H_nxt0 ?v_0)) (?v_224 (= ?v_18 NULL)) (?v_225 (t.H_nxt0 ?v_18))) (let ((?v_148 (not ?v_143)) (?v_150 (t.R_nxt0 t.l i1)) (?v_152 (and ?v_146 (and ?v_1 (not ?v_147))))) (let ((?v_151 (and ?v_145 ?v_152))) (let ((?v_160 (and ?v_22 (and ?v_59 (and ?v_67 (and ?v_4 (and ?v_144 (and ?v_150 ?v_151))))))) (?v_154 (not ?v_150))) (let ((?v_161 (and ?v_22 (and ?v_59 (and ?v_67 (and ?v_149 (and ?v_144 (and ?v_154 ?v_151))))))) (?v_153 (not ?v_67)) (?v_158 (not ?v_145))) (let ((?v_155 (and ?v_158 ?v_152)) (?v_159 (and ?v_146 (and ?v_147 ?v_3)))) (let ((?v_163 (and ?v_145 ?v_159)) (?v_164 (and ?v_158 ?v_159)) (?v_162 (not ?v_156))) (let ((?v_165 (and ?v_59 (and ?v_67 (and ?v_4 (and ?v_144 (and ?v_150 ?v_163))))))) (let ((?v_167 (and ?v_22 ?v_165)) (?v_258 (t.data i1))) (let ((?v_166 (= ?v_258 ZERO)) (?v_171 (not ?v_168)) (?v_172 (t.R_nxt0 t.l t.l)) (?v_173 (and ?v_170 ?v_152))) (let ((?v_180 (and ?v_22 (and ?v_59 (and ?v_71 (and ?v_169 (and ?v_144 (and ?v_172 ?v_173))))))) (?v_175 (not ?v_169)) (?v_176 (not ?v_172))) (let ((?v_181 (and ?v_22 (and ?v_59 (and ?v_71 (and ?v_175 (and ?v_144 (and ?v_176 ?v_173))))))) (?v_174 (not ?v_71)) (?v_179 (not ?v_170))) (let ((?v_177 (and ?v_179 ?v_152)) (?v_182 (and ?v_170 ?v_159)) (?v_183 (and ?v_179 ?v_159))) (let ((?v_184 (and ?v_59 (and ?v_71 (and ?v_169 (and ?v_144 (and ?v_172 ?v_182))))))) (let ((?v_186 (and ?v_22 ?v_184)) (?v_185 (= (t.data t.l) ZERO)) (?v_189 (not ?v_187)) (?v_191 (t.R_nxt0 t.l t.t)) (?v_192 (and ?v_188 ?v_152))) (let ((?v_199 (and ?v_22 (and ?v_59 (and ?v_77 (and ?v_10 (and ?v_144 (and ?v_191 ?v_192))))))) (?v_194 (not ?v_191))) (let ((?v_200 (and ?v_22 (and ?v_59 (and ?v_77 (and ?v_190 (and ?v_144 (and ?v_194 ?v_192))))))) (?v_193 (not ?v_77)) (?v_198 (not ?v_188))) (let ((?v_195 (and ?v_198 ?v_152)) (?v_197 (not ?v_196)) (?v_201 (and ?v_188 ?v_159)) (?v_202 (and ?v_198 ?v_159))) (let ((?v_203 (and ?v_59 (and ?v_77 (and ?v_10 (and ?v_144 (and ?v_191 ?v_201))))))) (let ((?v_205 (and ?v_22 ?v_203)) (?v_204 (= (t.data t.t) ZERO)) (?v_208 (not ?v_206)) (?v_210 (t.R_nxt0 t.l ?v_0)) (?v_211 (and ?v_207 ?v_152))) (let ((?v_216 (and ?v_22 (and ?v_59 (and ?v_7 (and ?v_14 (and ?v_144 (and ?v_210 ?v_211))))))) (?v_212 (not ?v_210))) (let ((?v_217 (and ?v_22 (and ?v_59 (and ?v_7 (and ?v_209 (and ?v_144 (and ?v_212 ?v_211))))))) (?v_215 (not ?v_207))) (let ((?v_213 (and ?v_215 ?v_152)) (?v_219 (and ?v_207 ?v_159)) (?v_220 (and ?v_215 ?v_159)) (?v_218 (not ?v_13))) (let ((?v_221 (and ?v_59 (and ?v_7 (and ?v_14 (and ?v_144 (and ?v_210 ?v_219))))))) (let ((?v_223 (and ?v_22 ?v_221)) (?v_222 (= (t.data ?v_0) ZERO)) (?v_226 (not ?v_224)) (?v_228 (t.R_nxt0 t.l ?v_18)) (?v_229 (and ?v_225 ?v_152))) (let ((?v_234 (and ?v_22 (and ?v_59 (and ?v_31 (and ?v_19 (and ?v_144 (and ?v_228 ?v_229))))))) (?v_230 (not ?v_228))) (let ((?v_235 (and ?v_22 (and ?v_59 (and ?v_31 (and ?v_227 (and ?v_144 (and ?v_230 ?v_229))))))) (?v_233 (not ?v_225))) (let ((?v_231 (and ?v_233 ?v_152)) (?v_237 (and ?v_225 ?v_159)) (?v_238 (and ?v_233 ?v_159)) (?v_236 (not ?v_46))) (let ((?v_239 (and ?v_59 (and ?v_31 (and ?v_19 (and ?v_144 (and ?v_228 ?v_237))))))) (let ((?v_241 (and ?v_22 ?v_239)) (?v_240 (= (t.data ?v_18) ZERO)) (?v_246 (or ?v_1 ?v_23))) (let ((?v_244 (ite ?v_246 en_LOCATION (+ 1 (+ 1 ?v_242))))) (let ((?v_243 (= ?v_244 ?v_242)) (?v_278 (not PRED_VAR__p_0)) (?v_245 (= ?v_244 en_LOCATION)) (?v_269 (not PRED_VAR__p_1)) (?v_274 (not PRED_VAR__p_3)) (?v_271 (not PRED_VAR__p_16)) (?v_248 (and ?v_26 ?v_4)) (?v_254 (not ?v_246)) (?v_249 (and ?v_147 ?v_127))) (let ((?v_255 (not ?v_249))) (let ((?v_250 (and ?v_255 ?v_4))) (let ((?v_251 (or (and ?v_246 (or (and ?v_1 ?v_247) (and ?v_3 (or (and ?v_23 (or (and ?v_23 (or (and ?v_23 ?v_4) ?v_248)) ?v_248)) ?v_248)))) (and ?v_254 (or (and ?v_249 (or (and ?v_249 ?v_4) ?v_250)) ?v_250)))) (?v_270 (not PRED_VAR__p_8)) (?v_261 (ite ?v_246 (ite ?v_1 ?v_0 (ite ?v_23 ?v_18 t.t)) t.t))) (let ((?v_252 (t.R_nxt ?v_261 i1))) (let ((?v_253 (and ?v_26 ?v_252)) (?v_256 (and ?v_255 ?v_252))) (let ((?v_257 (or (and ?v_246 (or (and ?v_1 (or (and ?v_1 ?v_252) (and ?v_3 ?v_252))) (and ?v_3 (or (and ?v_23 (or (and ?v_23 (or (and ?v_23 ?v_252) ?v_253)) ?v_253)) ?v_253)))) (and ?v_254 (or (and ?v_249 (or (and ?v_249 ?v_252) ?v_256)) ?v_256)))) (?v_277 (not PRED_VAR__p_9)) (?v_273 (not PRED_VAR__p_14)) (?v_259 (= (ite ?v_246 (ite ?v_1 (ite ?v_1 (ite ?v_112 ZERO ?v_258) ?v_258) (ite ?v_23 (ite ?v_23 (ite ?v_116 ZERO ?v_258) ?v_258) ?v_258)) ?v_258) ZERO)) (?v_262 (= (t.I_nxt ?v_261) t.l)) (?v_263 (= ?v_261 t.l)) (?v_268 (not PRED_VAR__p_18)) (?v_267 (not PRED_VAR__p_19)) (?v_264 (and ?v_26 ?v_156)) (?v_265 (and ?v_255 ?v_156))) (let ((?v_266 (or (and ?v_246 (or (and ?v_1 (or (and ?v_1 ?v_156) (and ?v_3 ?v_156))) (and ?v_3 (or (and ?v_23 (or (and ?v_23 (or (and ?v_23 ?v_156) ?v_264)) ?v_264)) ?v_264)))) (and ?v_254 (or (and ?v_249 (or (and ?v_249 ?v_156) ?v_265)) ?v_265)))) (?v_281 (not PRED_VAR__p_20)) (?v_275 (and PRED_VAR__p_2 (and PRED_VAR__p_0 ?v_269)))) (let ((?v_272 (and PRED_VAR__p_3 ?v_275))) (let ((?v_280 (and ?v_268 (and PRED_VAR__p_10 (and PRED_VAR__p_14 (and PRED_VAR__p_8 (and PRED_VAR__p_11 (and PRED_VAR__p_16 ?v_272))))))) (?v_282 (and ?v_268 (and PRED_VAR__p_10 (and PRED_VAR__p_14 (and ?v_270 (and PRED_VAR__p_11 (and ?v_271 ?v_272))))))) (?v_276 (and ?v_274 ?v_275)) (?v_279 (and PRED_VAR__p_2 (and PRED_VAR__p_1 ?v_278)))) (let ((?v_283 (and PRED_VAR__p_3 ?v_279)) (?v_284 (and ?v_274 ?v_279))) (let ((?v_285 (and PRED_VAR__p_10 (and PRED_VAR__p_14 (and PRED_VAR__p_8 (and PRED_VAR__p_11 (and PRED_VAR__p_16 ?v_283))))))) (let ((?v_286 (and ?v_268 ?v_285))) (and (and (and (and (and (and (and (and (and (and (or ?v_7 (and (or (not ?v_6) ?v_5) (or (not ?v_5) ?v_6))) (and (or ?v_7 (not (or (and ?v_1 ?v_8) (and ?v_3 ?v_8)))) (and (or ?v_7 (and (or (not ?v_12) ?v_11) (or (not ?v_11) ?v_12))) (and (or ?v_7 (and (or (not ?v_16) ?v_15) (or (not ?v_15) ?v_16))) (or ?v_7 (and (or (not ?v_21) ?v_20) (or (not ?v_20) ?v_21))))))) (and (or ?v_31 (and (or (not ?v_30) ?v_29) (or (not ?v_29) ?v_30))) (and (or ?v_31 (and (or (not ?v_37) ?v_36) (or (not ?v_36) ?v_37))) (and (or ?v_31 (not (or (and ?v_23 (or (and ?v_23 ?v_38) ?v_39)) ?v_39))) (and (or ?v_31 (and (or (not ?v_45) ?v_44) (or (not ?v_44) ?v_45))) (or ?v_31 (and (or (not ?v_51) ?v_50) (or (not ?v_50) ?v_51)))))))) (and (and (or (not ?v_53) ?v_52) (or (not ?v_52) ?v_53)) (and (and (or ?v_260 ?v_58) (or (not ?v_58) ?v_59)) (and (and (or (not ?v_62) ?v_61) (or (not ?v_61) ?v_62)) (and (and (or (not ?v_64) ?v_63) (or (not ?v_63) ?v_64)) (and (and (or (not ?v_66) ?v_65) (or (not ?v_65) ?v_66)) (and (and (or (not ?v_69) ?v_68) (or (not ?v_68) ?v_69)) (and (and (or (not ?v_76) ?v_75) (or (not ?v_75) ?v_76)) (and (and (or (not ?v_80) ?v_79) (or (not ?v_79) ?v_80)) (and (and (or (not ?v_83) ?v_82) (or (not ?v_82) ?v_83)) (and (and (or (not ?v_85) ?v_84) (or (not ?v_84) ?v_85)) (and (and (or (not ?v_86) ?v_88) (or (not ?v_88) ?v_86)) (and (and (or (not ?v_89) ?v_92) (or (not ?v_92) ?v_89)) (and (and (or (not ?v_93) ?v_94) (or (not ?v_94) ?v_93)) (and (and (or (not ?v_95) ?v_96) (or (not ?v_96) ?v_95)) (and (and (or (not ?v_97) ?v_98) (or (not ?v_98) ?v_97)) (and (and (or (not ?v_99) ?v_101) (or (not ?v_101) ?v_99)) (and (and (or (not ?v_102) ?v_105) (or (not ?v_105) ?v_102)) (and (and (or (not ?v_106) ?v_107) (or (not ?v_107) ?v_106)) (and (and (or (not ?v_108) ?v_109) (or (not ?v_109) ?v_108)) (and (or (not ?v_110) ?v_111) (or (not ?v_111) ?v_110)))))))))))))))))))))) (and ?v_156 (and (and (or (not ?v_115) ?v_114) (or (not ?v_114) ?v_115)) (and (and (or (not ?v_119) ?v_118) (or (not ?v_118) ?v_119)) (and (and (or (not ?v_122) ?v_121) (or (not ?v_121) ?v_122)) (and (and (or (not ?v_125) ?v_124) (or (not ?v_124) ?v_125)) (and (and (or ?v_149 ?v_126) (or (not ?v_126) ?v_4)) (and ?v_169 (and (and (or ?v_190 ?v_128) (or (not ?v_128) ?v_10)) (and (and (or ?v_209 ?v_129) (or (not ?v_129) ?v_14)) (and (and (or ?v_227 ?v_130) (or (not ?v_130) ?v_19)) (and (and (or ?v_157 ?v_131) (or (not ?v_131) ?v_27)) (and (and (or ?v_178 ?v_132) (or (not ?v_132) ?v_34)) (and ?v_196 (and (and (or ?v_214 ?v_133) (or (not ?v_133) ?v_42)) (and (and (or ?v_232 ?v_134) (or (not ?v_134) ?v_48)) (and (and (or (not ?v_2) ?v_135) (or (not ?v_135) ?v_2)) (and (and (or (not ?v_8) ?v_136) (or (not ?v_136) ?v_8)) (and (and (or (not ?v_9) ?v_137) (or (not ?v_137) ?v_9)) (and ?v_13 (and (and (or (not ?v_17) ?v_138) (or (not ?v_138) ?v_17)) (and (and (or (not ?v_24) ?v_139) (or (not ?v_139) ?v_24)) (and (and (or (not ?v_32) ?v_140) (or (not ?v_140) ?v_32)) (and (and (or (not ?v_38) ?v_141) (or (not ?v_141) ?v_38)) (and (and (or (not ?v_40) ?v_142) (or (not ?v_142) ?v_40)) ?v_46))))))))))))))))))))))))) (and (t.H_nxt NULL) (= (t.nxt NULL) NULL))) ?v_146) (and (or (not (or (= i1 t.l0) ?v_143)) ?v_145) (and (or (not (or ?v_144 ?v_168)) ?v_170) (and (or (not (or (= t.t t.l0) ?v_187)) ?v_188) (and (or (not (or (= ?v_0 t.l0) ?v_206)) ?v_207) (or (not (or (= ?v_18 t.l0) ?v_224)) ?v_225)))))) (not (= NULL t.l0))) (and (and (or (or (or (or (or (or (or (or (or (or (or (or (or (and ?v_148 ?v_160) (and ?v_148 ?v_161)) (and ?v_148 (and ?v_22 (and ?v_59 (and ?v_153 (and ?v_4 (and ?v_144 (and ?v_150 ?v_155)))))))) (and ?v_148 (and ?v_22 (and ?v_59 (and ?v_153 (and ?v_149 (and ?v_144 (and ?v_154 ?v_155)))))))) (and ?v_76 (and ?v_156 (and ?v_157 (and ?v_59 (and ?v_67 (and ?v_149 (and ?v_144 (and ?v_154 ?v_163))))))))) (and ?v_76 (and ?v_156 (and ?v_157 (and ?v_148 (and ?v_59 (and ?v_153 (and ?v_149 (and ?v_144 (and ?v_154 ?v_164)))))))))) (and ?v_156 (and ?v_27 ?v_160))) (and ?v_162 (and ?v_157 ?v_160))) (and ?v_156 (and ?v_27 ?v_161))) (and ?v_162 (and ?v_157 ?v_161))) (and ?v_76 (and ?v_156 (and ?v_27 ?v_167)))) (and ?v_76 (and ?v_156 (and ?v_27 (and ?v_148 (and ?v_22 (and ?v_59 (and ?v_153 (and ?v_4 (and ?v_144 (and ?v_150 ?v_164))))))))))) (and ?v_166 (and ?v_76 (and ?v_156 (and ?v_27 (and ?v_148 ?v_165)))))) (and ?v_166 (and ?v_76 (and ?v_156 (and ?v_148 ?v_167))))) (and (or (or (or (or (or (or (or (or (or (or (or (or (or (and ?v_171 ?v_180) (and ?v_171 ?v_181)) (and ?v_171 (and ?v_22 (and ?v_59 (and ?v_174 (and ?v_169 (and ?v_144 (and ?v_172 ?v_177)))))))) (and ?v_171 (and ?v_22 (and ?v_59 (and ?v_174 (and ?v_175 (and ?v_144 (and ?v_176 ?v_177)))))))) (and ?v_76 (and ?v_169 (and ?v_178 (and ?v_59 (and ?v_71 (and ?v_175 (and ?v_144 (and ?v_176 ?v_182))))))))) (and ?v_76 (and ?v_169 (and ?v_178 (and ?v_171 (and ?v_59 (and ?v_174 (and ?v_175 (and ?v_144 (and ?v_176 ?v_183)))))))))) (and ?v_169 (and ?v_34 ?v_180))) (and ?v_175 (and ?v_178 ?v_180))) (and ?v_169 (and ?v_34 ?v_181))) (and ?v_175 (and ?v_178 ?v_181))) (and ?v_76 (and ?v_169 (and ?v_34 ?v_186)))) (and ?v_76 (and ?v_169 (and ?v_34 (and ?v_171 (and ?v_22 (and ?v_59 (and ?v_174 (and ?v_169 (and ?v_144 (and ?v_172 ?v_183))))))))))) (and ?v_185 (and ?v_76 (and ?v_169 (and ?v_34 (and ?v_171 ?v_184)))))) (and ?v_185 (and ?v_76 (and ?v_169 (and ?v_171 ?v_186))))) (and (or (or (or (or (or (or (or (or (or (or (or (or (or (and ?v_189 ?v_199) (and ?v_189 ?v_200)) (and ?v_189 (and ?v_22 (and ?v_59 (and ?v_193 (and ?v_10 (and ?v_144 (and ?v_191 ?v_195)))))))) (and ?v_189 (and ?v_22 (and ?v_59 (and ?v_193 (and ?v_190 (and ?v_144 (and ?v_194 ?v_195)))))))) (and ?v_76 (and ?v_196 (and ?v_197 (and ?v_59 (and ?v_77 (and ?v_190 (and ?v_144 (and ?v_194 ?v_201))))))))) (and ?v_76 (and ?v_196 (and ?v_197 (and ?v_189 (and ?v_59 (and ?v_193 (and ?v_190 (and ?v_144 (and ?v_194 ?v_202)))))))))) (and ?v_196 (and ?v_196 ?v_199))) (and ?v_197 (and ?v_197 ?v_199))) (and ?v_196 (and ?v_196 ?v_200))) (and ?v_197 (and ?v_197 ?v_200))) (and ?v_76 (and ?v_196 (and ?v_196 ?v_205)))) (and ?v_76 (and ?v_196 (and ?v_196 (and ?v_189 (and ?v_22 (and ?v_59 (and ?v_193 (and ?v_10 (and ?v_144 (and ?v_191 ?v_202))))))))))) (and ?v_204 (and ?v_76 (and ?v_196 (and ?v_196 (and ?v_189 ?v_203)))))) (and ?v_204 (and ?v_76 (and ?v_196 (and ?v_189 ?v_205))))) (and (or (or (or (or (or (or (or (or (or (or (or (or (or (and ?v_208 ?v_216) (and ?v_208 ?v_217)) (and ?v_208 (and ?v_22 (and ?v_59 (and ?v_56 (and ?v_14 (and ?v_144 (and ?v_210 ?v_213)))))))) (and ?v_208 (and ?v_22 (and ?v_59 (and ?v_56 (and ?v_209 (and ?v_144 (and ?v_212 ?v_213)))))))) (and ?v_76 (and ?v_13 (and ?v_214 (and ?v_59 (and ?v_7 (and ?v_209 (and ?v_144 (and ?v_212 ?v_219))))))))) (and ?v_76 (and ?v_13 (and ?v_214 (and ?v_208 (and ?v_59 (and ?v_56 (and ?v_209 (and ?v_144 (and ?v_212 ?v_220)))))))))) (and ?v_13 (and ?v_42 ?v_216))) (and ?v_218 (and ?v_214 ?v_216))) (and ?v_13 (and ?v_42 ?v_217))) (and ?v_218 (and ?v_214 ?v_217))) (and ?v_76 (and ?v_13 (and ?v_42 ?v_223)))) (and ?v_76 (and ?v_13 (and ?v_42 (and ?v_208 (and ?v_22 (and ?v_59 (and ?v_56 (and ?v_14 (and ?v_144 (and ?v_210 ?v_220))))))))))) (and ?v_222 (and ?v_76 (and ?v_13 (and ?v_42 (and ?v_208 ?v_221)))))) (and ?v_222 (and ?v_76 (and ?v_13 (and ?v_208 ?v_223))))) (or (or (or (or (or (or (or (or (or (or (or (or (or (and ?v_226 ?v_234) (and ?v_226 ?v_235)) (and ?v_226 (and ?v_22 (and ?v_59 (and ?v_73 (and ?v_19 (and ?v_144 (and ?v_228 ?v_231)))))))) (and ?v_226 (and ?v_22 (and ?v_59 (and ?v_73 (and ?v_227 (and ?v_144 (and ?v_230 ?v_231)))))))) (and ?v_76 (and ?v_46 (and ?v_232 (and ?v_59 (and ?v_31 (and ?v_227 (and ?v_144 (and ?v_230 ?v_237))))))))) (and ?v_76 (and ?v_46 (and ?v_232 (and ?v_226 (and ?v_59 (and ?v_73 (and ?v_227 (and ?v_144 (and ?v_230 ?v_238)))))))))) (and ?v_46 (and ?v_48 ?v_234))) (and ?v_236 (and ?v_232 ?v_234))) (and ?v_46 (and ?v_48 ?v_235))) (and ?v_236 (and ?v_232 ?v_235))) (and ?v_76 (and ?v_46 (and ?v_48 ?v_241)))) (and ?v_76 (and ?v_46 (and ?v_48 (and ?v_226 (and ?v_22 (and ?v_59 (and ?v_73 (and ?v_19 (and ?v_144 (and ?v_228 ?v_238))))))))))) (and ?v_240 (and ?v_76 (and ?v_46 (and ?v_48 (and ?v_226 ?v_239)))))) (and ?v_240 (and ?v_76 (and ?v_46 (and ?v_226 ?v_241))))))))) (and (and (and (and (and (and (and (and (and (and (and (and (and (and (or (and PRED_VAR__p_0 ?v_243) (and ?v_278 (not ?v_243))) (or (and PRED_VAR__p_1 ?v_245) (and ?v_269 (not ?v_245)))) (or (and PRED_VAR__p_2 ?v_146) (and (not PRED_VAR__p_2) (not ?v_146)))) (or (and PRED_VAR__p_3 ?v_145) (and ?v_274 ?v_158))) (or (and PRED_VAR__p_16 ?v_150) (and ?v_271 ?v_154))) (or (and PRED_VAR__p_11 ?v_144) (and (not PRED_VAR__p_11) (not ?v_144)))) (or (and PRED_VAR__p_8 ?v_251) (and ?v_270 (not ?v_251)))) (or (and PRED_VAR__p_9 ?v_257) (and ?v_277 (not ?v_257)))) (or (and PRED_VAR__p_14 ?v_67) (and ?v_273 ?v_153))) (or (and PRED_VAR__p_15 ?v_259) (and (not PRED_VAR__p_15) (not ?v_259)))) (or (and PRED_VAR__p_10 ?v_59) (and (not PRED_VAR__p_10) ?v_260))) (or (and PRED_VAR__p_12 ?v_262) (and (not PRED_VAR__p_12) (not ?v_262)))) (or (and PRED_VAR__p_18 ?v_263) (and ?v_268 (not ?v_263)))) (or (and PRED_VAR__p_19 ?v_143) (and ?v_267 ?v_148))) (or (and PRED_VAR__p_20 ?v_266) (and ?v_281 (not ?v_266)))))) (not (or (or (or (or (or (or (or (or (or (or (or (or (or (and ?v_267 ?v_280) (and ?v_267 ?v_282)) (and ?v_267 (and ?v_268 (and PRED_VAR__p_10 (and ?v_273 (and PRED_VAR__p_8 (and PRED_VAR__p_11 (and PRED_VAR__p_16 ?v_276)))))))) (and ?v_267 (and ?v_268 (and PRED_VAR__p_10 (and ?v_273 (and ?v_270 (and PRED_VAR__p_11 (and ?v_271 ?v_276)))))))) (and PRED_VAR__p_12 (and PRED_VAR__p_20 (and ?v_277 (and PRED_VAR__p_10 (and PRED_VAR__p_14 (and ?v_270 (and PRED_VAR__p_11 (and ?v_271 ?v_283))))))))) (and PRED_VAR__p_12 (and PRED_VAR__p_20 (and ?v_277 (and ?v_267 (and PRED_VAR__p_10 (and ?v_273 (and ?v_270 (and PRED_VAR__p_11 (and ?v_271 ?v_284)))))))))) (and PRED_VAR__p_20 (and PRED_VAR__p_9 ?v_280))) (and ?v_281 (and ?v_277 ?v_280))) (and PRED_VAR__p_20 (and PRED_VAR__p_9 ?v_282))) (and ?v_281 (and ?v_277 ?v_282))) (and PRED_VAR__p_12 (and PRED_VAR__p_20 (and PRED_VAR__p_9 ?v_286)))) (and PRED_VAR__p_12 (and PRED_VAR__p_20 (and PRED_VAR__p_9 (and ?v_267 (and ?v_268 (and PRED_VAR__p_10 (and ?v_273 (and PRED_VAR__p_8 (and PRED_VAR__p_11 (and PRED_VAR__p_16 ?v_284))))))))))) (and PRED_VAR__p_15 (and PRED_VAR__p_12 (and PRED_VAR__p_20 (and PRED_VAR__p_9 (and ?v_267 ?v_285)))))) (and PRED_VAR__p_15 (and PRED_VAR__p_12 (and PRED_VAR__p_20 (and ?v_267 ?v_286))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+(check-sat)
+(exit)
projects / cvc5.git / commitdiff