SMTInterpol regression: AssertionError in close

[PhilippWendler]

With JavaSMT 5.0.0 and SMTInterpol 2.5-1242-g5c50fb6d we get the following crash:

Exception in thread "main" java.lang.AssertionError
        at de.uni_freiburg.informatik.ultimate.smtinterpol.theory.cclosure.CCTerm.unshare(CCTerm.java:292)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.convert.Clausifier.pop(Clausifier.java:2343)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.pop(SMTInterpol.java:406)
        at org.sosy_lab.java_smt.solvers.smtinterpol.SmtInterpolAbstractProver.close(SmtInterpolAbstractProver.java:220)
        at org.sosy_lab.java_smt.basicimpl.withAssumptionsWrapper.BasicProverWithAssumptionsWrapper.close(BasicProverWithAssumptionsWrapper.java:117)
        at org.sosy_lab.cpachecker.util.predicates.smt.BasicProverEnvironmentView.close(BasicProverEnvironmentView.java:85)
        at org.sosy_lab.cpachecker.cpa.predicate.PredicateAbstractionManager.computeAbstraction(PredicateAbstractionManager.java:798)
        at org.sosy_lab.cpachecker.cpa.predicate.PredicateAbstractionManager.buildAbstraction(PredicateAbstractionManager.java:405)
        at org.sosy_lab.cpachecker.cpa.predicate.PredicatePrecisionAdjustment.computeAbstraction(PredicatePrecisionAdjustment.java:185)
        at org.sosy_lab.cpachecker.cpa.predicate.PredicatePrecisionAdjustment.prec(PredicatePrecisionAdjustment.java:96)
        at org.sosy_lab.cpachecker.cpa.composite.CompositePrecisionAdjustment.prec(CompositePrecisionAdjustment.java:68)
        at org.sosy_lab.cpachecker.cpa.arg.ARGPrecisionAdjustment.prec(ARGPrecisionAdjustment.java:88)
        at org.sosy_lab.cpachecker.cpa.arg.ARGPrecisionAdjustment.prec(ARGPrecisionAdjustment.java:58)
        at org.sosy_lab.cpachecker.core.algorithm.CPAAlgorithm.handleState(CPAAlgorithm.java:356)
        at org.sosy_lab.cpachecker.core.algorithm.CPAAlgorithm.run0(CPAAlgorithm.java:289)
        at org.sosy_lab.cpachecker.core.algorithm.CPAAlgorithm.run(CPAAlgorithm.java:260)
        at org.sosy_lab.cpachecker.core.algorithm.CEGARAlgorithm.run(CEGARAlgorithm.java:241)
        at org.sosy_lab.cpachecker.core.algorithm.CounterexampleStoreAlgorithm.run(CounterexampleStoreAlgorithm.java:58)
        at org.sosy_lab.cpachecker.core.CPAchecker.runAlgorithm(CPAchecker.java:489)
        at org.sosy_lab.cpachecker.core.CPAchecker.run(CPAchecker.java:357)
        at org.sosy_lab.cpachecker.cmdline.CPAMain.main(CPAMain.java:171)

This does not appear always, but in many hundred cases: 1,category(notIn())))&sort=0_cputime_1,asc), 2,category(notIn())))&sort=0_cputime_1,asc), 3,category(notIn())))) It seems to be deterministic.

Given that our code just calls close() as part of a try-with-resources block, this should be a bug in either JavaSMT or SMTInterpol.

[baierd]

So the problem is in line 220 in the SmtInterpolAbstractProver. I can not tell what the underlying problem is at this moment however. Removing this line avoids the error and the analysis returns True.

I could not yet determine a way of testing this. @daniel-raffler do you want to try and find a test and possibly a program to send to the SMTInterpol devs if we are not causing this?

@PhilippWendler do we need a hotfix version for this?

Based on debugging i found that:

• SMTInterpol might not count empty pushs of the assertion stack properly somehow, as we have 12 assertion levels with 1 empty level in the beginning and SMTInterpol has 11 internally, none being empty.
• The crash happens internally when SMTInterpol tries to clean the symbol |__ADDRESS_OF_ldv_init::var3@|.
• Using the debug mode i found that CPAchecker uses formulas not created in the original solver context in this configuration, but only strictly after the closing of the interpolation prover with the error. This might be fine for SMTInterpol however. See the following error message:

  
  Exception in thread "main" java.lang.IllegalArgumentException: Function was not declared in this context.
  (not PRED1)
  not in
  [(= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 16) 0)) 0), (let ((.cse4 (+ __ADDRESS_OF_ldv_current@ 1840))) (let ((.cse0 (+ (+ __ADDRESS_OF_ldv_current@ 104) 40)) (.cse1 (+ (+ __ADDRESS_OF_ldv_current@ 480) 0)) (.cse2 (+ __ADDRESS_OF_ldv_current@ 1824)) (.cse3 (+ .cse4 8))) (and (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 16) 0)) 0) (= (|*struct_list_head:next@1| (+ .cse0 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse0 8)) 0) (= (|*struct_list_head:next@1| (+ .cse1 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse1 8)) 0) (= (|*struct_list_head:next@1| (+ .cse2 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse2 8)) 0) (= (|*struct_list_head:next@1| (+ .cse3 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse3 8)) 0) (= (|*struct_list_head:next@1| (+ (+ .cse4 24) 0)) 0)))), (- __ADDRESS_OF_ldv_current@ 0), |ldv_undef_int::undef_int@6|, (let ((.cse0 (- |__ADDRESS_OF_ldv_init::var3@| 0))) (= .cse0 (* 4 (div .cse0 4)))), 1824, (and (= (|*int:global@2| |__ADDRESS_OF_ldv_init::var3@|) |ldv_undef_int::__retval__@2|) (let ((.cse0 (+ |__ADDRESS_OF_ldv_init::var1@| 0))) (= (|*int:global@2| .cse0) (|*int:global@1| .cse0)))), (div (- |__ADDRESS_OF_ldv_init::var3@| 0) 4), 80, (= (|*struct_list_head:prev@1| (+ (+ __ADDRESS_OF_ldv_current@ 2088) 8)) 0), (let ((.cse10 (+ __ADDRESS_OF_ldv_current@ 1840))) (let ((.cse0 (+ (+ __ADDRESS_OF_ldv_current@ 104) 40)) (.cse1 (+ (+ __ADDRESS_OF_ldv_current@ 480) 0)) (.cse2 (+ __ADDRESS_OF_ldv_current@ 1824)) (.cse3 (+ .cse10 8)) (.cse4 (+ .cse10 24)) (.cse5 (+ __ADDRESS_OF_ldv_current@ 2032)) (.cse6 (+ __ADDRESS_OF_ldv_current@ 2048)) (.cse7 (+ __ADDRESS_OF_ldv_current@ 2072)) (.cse8 (+ __ADDRESS_OF_ldv_current@ 2088)) (.cse9 (+ __ADDRESS_OF_ldv_current@ 2176))) (and (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 16) 0)) 0) (= (|*struct_list_head:next@1| (+ .cse0 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse0 8)) 0) (= (|*struct_list_head:next@1| (+ .cse1 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse1 8)) 0) (= (|*struct_list_head:next@1| (+ .cse2 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse2 8)) 0) (= (|*struct_list_head:next@1| (+ .cse3 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse3 8)) 0) (= (|*struct_list_head:next@1| (+ .cse4 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse4 8)) 0) (= (|*struct_list_head:next@1| (+ .cse5 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse5 8)) 0) (= (|*struct_list_head:next@1| (+ .cse6 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse6 8)) 0) (= (|*struct_list_head:next@1| (+ .cse7 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse7 8)) 0) (= (|*struct_list_head:next@1| (+ .cse8 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse8 8)) 0) (= (|*struct_list_head:next@1| (+ .cse9 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse9 8)) 0)))), (|*struct_list_head:prev@1| (+ (+ __ADDRESS_OF_ldv_current@ 2072) 8)), (= (|*struct_list_head:prev@1| (+ (+ __ADDRESS_OF_ldv_current@ 6184) 8)) 0), (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 10504) 0)) 0), (+ __ADDRESS_OF_ldv_current@ 16), (+ __ADDRESS_OF_ldv_current@ 2072), (+ (+ (+ __ADDRESS_OF_ldv_current@ 6224) 80) 0), (let ((.cse9 (+ __ADDRESS_OF_ldv_current@ 1840))) (let ((.cse0 (+ (+ __ADDRESS_OF_ldv_current@ 104) 40)) (.cse1 (+ (+ __ADDRESS_OF_ldv_current@ 480) 0)) (.cse2 (+ __ADDRESS_OF_ldv_current@ 1824)) (.cse3 (+ .cse9 8)) (.cse4 (+ .cse9 24)) (.cse5 (+ __ADDRESS_OF_ldv_current@ 2032)) (.cse6 (+ __ADDRESS_OF_ldv_current@ 2048)) (.cse7 (+ __ADDRESS_OF_ldv_current@ 2072)) (.cse8 (+ __ADDRESS_OF_ldv_current@ 2088))) (and (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 16) 0)) 0) (= (|*struct_list_head:next@1| (+ .cse0 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse0 8)) 0) (= (|*struct_list_head:next@1| (+ .cse1 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse1 8)) 0) (= (|*struct_list_head:next@1| (+ .cse2 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse2 8)) 0) (= (|*struct_list_head:next@1| (+ .cse3 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse3 8)) 0) (= (|*struct_list_head:next@1| (+ .cse4 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse4 8)) 0) (= (|*struct_list_head:next@1| (+ .cse5 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse5 8)) 0) (= (|*struct_list_head:next@1| (+ .cse6 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse6 8)) 0) (= (|*struct_list_head:next@1| (+ .cse7 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse7 8)) 0) (= (|*struct_list_head:next@1| (+ .cse8 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse8 8)) 0)))), (= |ldv_undef_int::__retval__@2| |ldv_undef_int::undef_int@3|), (= (|*struct_list_head:next@1| (+ (+ __ADDRESS_OF_ldv_current@ 6184) 0)) 0), __+Infinity__, 10504, (+ (+ __ADDRESS_OF_ldv_current@ 104) 40), (|*struct_list_head:prev@1| (+ (+ (+ __ADDRESS_OF_ldv_current@ 480) 0) 8)), (+ (+ __ADDRESS_OF_ldv_current@ 6472) 0), (|*struct_list_head:prev@1| (+ (+ __ADDRESS_OF_ldv_current@ 2048) 8)), (= |ldv_init::var2| |__ADDRESS_OF_ldv_init::var1@|), (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 10508) 0)), (+ (+ (+ __ADDRESS_OF_ldv_current@ 2376) (* 16 0)) 0), (|*struct_list_head:prev@1| (+ (+ __ADDRESS_OF_ldv_current@ 2176) 8)), (|*struct_list_head:next@1| (+ (+ (+ __ADDRESS_OF_ldv_current@ 1840) 24) 0)), (|*struct_list_head:next@1| (+ (+ __ADDRESS_OF_ldv_current@ 6392) 0)), (+ __ADDRESS_OF_ldv_current@ 1824), (= (|*struct_list_head:next@1| (+ (+ __ADDRESS_OF_ldv_current@ 2192) 0)) 0), (= (|*struct_list_head:next@1| (+ (+ __ADDRESS_OF_ldv_current@ 2072) 0)) 0), |__ADDRESS_OF_ldv_init::var1@|, (= (|*struct_list_head:next@1| (+ (+ __ADDRESS_OF_ldv_current@ 2032) 0)) 0), (|*int:global@2| |ldv_init::var2@1|), (and (= |ldv_init::var4@2| |__ADDRESS_OF_ldv_init::var3@|) (not (= (|*int:global@3| |ldv_init::var2@2|) (|*int:global@3| |__ADDRESS_OF_ldv_init::var1@|)))), (|*struct_list_head:next@1| (+ (+ (+ __ADDRESS_OF_ldv_current@ 2728) 0) 0)), (let ((.cse11 (+ __ADDRESS_OF_ldv_current@ 1840))) (let ((.cse0 (+ (+ __ADDRESS_OF_ldv_current@ 104) 40)) (.cse1 (+ (+ __ADDRESS_OF_ldv_current@ 480) 0)) (.cse2 (+ __ADDRESS_OF_ldv_current@ 1824)) (.cse3 (+ .cse11 8)) (.cse4 (+ .cse11 24)) (.cse5 (+ __ADDRESS_OF_ldv_current@ 2032)) (.cse6 (+ __ADDRESS_OF_ldv_current@ 2048)) (.cse7 (+ __ADDRESS_OF_ldv_current@ 2072)) (.cse8 (+ __ADDRESS_OF_ldv_current@ 2088)) (.cse9 (+ __ADDRESS_OF_ldv_current@ 2176)) (.cse10 (+ __ADDRESS_OF_ldv_current@ 2192))) (and (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 16) 0)) 0) (= (|*struct_list_head:next@1| (+ .cse0 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse0 8)) 0) (= (|*struct_list_head:next@1| (+ .cse1 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse1 8)) 0) (= (|*struct_list_head:next@1| (+ .cse2 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse2 8)) 0) (= (|*struct_list_head:next@1| (+ .cse3 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse3 8)) 0) (= (|*struct_list_head:next@1| (+ .cse4 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse4 8)) 0) (= (|*struct_list_head:next@1| (+ .cse5 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse5 8)) 0) (= (|*struct_list_head:next@1| (+ .cse6 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse6 8)) 0) (= (|*struct_list_head:next@1| (+ .cse7 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse7 8)) 0) (= (|*struct_list_head:next@1| (+ .cse8 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse8 8)) 0) (= (|*struct_list_head:next@1| (+ .cse9 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse9 8)) 0) (= (|*struct_list_head:next@1| (+ .cse10 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse10 8)) 0) (= (|*struct_list_head:next@1| (+ (+ (+ __ADDRESS_OF_ldv_current@ 2376) (* 16 0)) 0)) 0)))), (let ((.cse14 (+ __ADDRESS_OF_ldv_current@ 1840))) (let ((.cse0 (+ (+ __ADDRESS_OF_ldv_current@ 104) 40)) (.cse1 (+ (+ __ADDRESS_OF_ldv_current@ 480) 0)) (.cse2 (+ __ADDRESS_OF_ldv_current@ 1824)) (.cse3 (+ .cse14 8)) (.cse4 (+ .cse14 24)) (.cse5 (+ __ADDRESS_OF_ldv_current@ 2032)) (.cse6 (+ __ADDRESS_OF_ldv_current@ 2048)) (.cse7 (+ __ADDRESS_OF_ldv_current@ 2072)) (.cse8 (+ __ADDRESS_OF_ldv_current@ 2088)) (.cse9 (+ __ADDRESS_OF_ldv_current@ 2176)) (.cse10 (+ __ADDRESS_OF_ldv_current@ 2192)) (.cse11 (+ (+ __ADDRESS_OF_ldv_current@ 2376) (* 16 0))) (.cse12 (+ (+ __ADDRESS_OF_ldv_current@ 2728) 0)) (.cse13 (+ __ADDRESS_OF_ldv_current@ 6152))) (and (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 16) 0)) 0) (= (|*struct_list_head:next@1| (+ .cse0 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse0 8)) 0) (= (|*struct_list_head:next@1| (+ .cse1 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse1 8)) 0) (= (|*struct_list_head:next@1| (+ .cse2 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse2 8)) 0) (= (|*struct_list_head:next@1| (+ .cse3 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse3 8)) 0) (= (|*struct_list_head:next@1| (+ .cse4 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse4 8)) 0) (= (|*struct_list_head:next@1| (+ .cse5 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse5 8)) 0) (= (|*struct_list_head:next@1| (+ .cse6 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse6 8)) 0) (= (|*struct_list_head:next@1| (+ .cse7 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse7 8)) 0) (= (|*struct_list_head:next@1| (+ .cse8 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse8 8)) 0) (= (|*struct_list_head:next@1| (+ .cse9 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse9 8)) 0) (= (|*struct_list_head:next@1| (+ .cse10 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse10 8)) 0) (= (|*struct_list_head:next@1| (+ .cse11 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse11 8)) 0) (= (|*struct_list_head:next@1| (+ .cse12 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse12 8)) 0) (= (|*struct_list_head:next@1| (+ .cse13 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse13 8)) 0)))), (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 16) 0)), (let ((.cse13 (+ __ADDRESS_OF_ldv_current@ 1840))) (let ((.cse0 (+ (+ __ADDRESS_OF_ldv_current@ 104) 40)) (.cse1 (+ (+ __ADDRESS_OF_ldv_current@ 480) 0)) (.cse2 (+ __ADDRESS_OF_ldv_current@ 1824)) (.cse3 (+ .cse13 8)) (.cse4 (+ .cse13 24)) (.cse5 (+ __ADDRESS_OF_ldv_current@ 2032)) (.cse6 (+ __ADDRESS_OF_ldv_current@ 2048)) (.cse7 (+ __ADDRESS_OF_ldv_current@ 2072)) (.cse8 (+ __ADDRESS_OF_ldv_current@ 2088)) (.cse9 (+ __ADDRESS_OF_ldv_current@ 2176)) (.cse10 (+ __ADDRESS_OF_ldv_current@ 2192)) (.cse11 (+ (+ __ADDRESS_OF_ldv_current@ 2376) (* 16 0))) (.cse12 (+ (+ __ADDRESS_OF_ldv_current@ 2728) 0))) (and (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 16) 0)) 0) (= (|*struct_list_head:next@1| (+ .cse0 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse0 8)) 0) (= (|*struct_list_head:next@1| (+ .cse1 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse1 8)) 0) (= (|*struct_list_head:next@1| (+ .cse2 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse2 8)) 0) (= (|*struct_list_head:next@1| (+ .cse3 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse3 8)) 0) (= (|*struct_list_head:next@1| (+ .cse4 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse4 8)) 0) (= (|*struct_list_head:next@1| (+ .cse5 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse5 8)) 0) (= (|*struct_list_head:next@1| (+ .cse6 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse6 8)) 0) (= (|*struct_list_head:next@1| (+ .cse7 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse7 8)) 0) (= (|*struct_list_head:next@1| (+ .cse8 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse8 8)) 0) (= (|*struct_list_head:next@1| (+ .cse9 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse9 8)) 0) (= (|*struct_list_head:next@1| (+ .cse10 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse10 8)) 0) (= (|*struct_list_head:next@1| (+ .cse11 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse11 8)) 0) (= (|*struct_list_head:next@1| (+ .cse12 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse12 8)) 0) (= (|*struct_list_head:next@1| (+ (+ __ADDRESS_OF_ldv_current@ 6152) 0)) 0)))), (let ((.cse15 (+ __ADDRESS_OF_ldv_current@ 6224)) (.cse19 (+ __ADDRESS_OF_ldv_current@ 1840))) (let ((.cse0 (+ (+ __ADDRESS_OF_ldv_current@ 104) 40)) (.cse1 (+ (+ __ADDRESS_OF_ldv_current@ 480) 0)) (.cse2 (+ __ADDRESS_OF_ldv_current@ 1824)) (.cse3 (+ .cse19 8)) (.cse4 (+ .cse19 24)) (.cse5 (+ __ADDRESS_OF_ldv_current@ 2032)) (.cse6 (+ __ADDRESS_OF_ldv_current@ 2048)) (.cse7 (+ __ADDRESS_OF_ldv_current@ 2072)) (.cse8 (+ __ADDRESS_OF_ldv_current@ 2088)) (.cse9 (+ __ADDRESS_OF_ldv_current@ 2176)) (.cse10 (+ __ADDRESS_OF_ldv_current@ 2192)) (.cse11 (+ (+ __ADDRESS_OF_ldv_current@ 2376) (* 16 0))) (.cse12 (+ (+ __ADDRESS_OF_ldv_current@ 2728) 0)) (.cse13 (+ __ADDRESS_OF_ldv_current@ 6152)) (.cse14 (+ __ADDRESS_OF_ldv_current@ 6184)) (.cse16 (+ .cse15 80)) (.cse17 (+ __ADDRESS_OF_ldv_current@ 6392)) (.cse18 (+ __ADDRESS_OF_ldv_current@ 6472))) (and (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 16) 0)) 0) (= (|*struct_list_head:next@1| (+ .cse0 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse0 8)) 0) (= (|*struct_list_head:next@1| (+ .cse1 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse1 8)) 0) (= (|*struct_list_head:next@1| (+ .cse2 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse2 8)) 0) (= (|*struct_list_head:next@1| (+ .cse3 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse3 8)) 0) (= (|*struct_list_head:next@1| (+ .cse4 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse4 8)) 0) (= (|*struct_list_head:next@1| (+ .cse5 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse5 8)) 0) (= (|*struct_list_head:next@1| (+ .cse6 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse6 8)) 0) (= (|*struct_list_head:next@1| (+ .cse7 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse7 8)) 0) (= (|*struct_list_head:next@1| (+ .cse8 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse8 8)) 0) (= (|*struct_list_head:next@1| (+ .cse9 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse9 8)) 0) (= (|*struct_list_head:next@1| (+ .cse10 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse10 8)) 0) (= (|*struct_list_head:next@1| (+ .cse11 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse11 8)) 0) (= (|*struct_list_head:next@1| (+ .cse12 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse12 8)) 0) (= (|*struct_list_head:next@1| (+ .cse13 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse13 8)) 0) (= (|*struct_list_head:next@1| (+ .cse14 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse14 8)) 0) (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ .cse15 0) 0)) 0) (= (|*struct_list_head:next@1| (+ .cse16 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse16 8)) 0) (= (|*struct_list_head:next@1| (+ .cse17 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse17 8)) 0) (= (|*struct_list_head:next@1| (+ .cse18 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse18 8)) 0) (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 10504) 0)) 0)))), (* 8 (div (- __ADDRESS_OF_ldv_current@ 0) 8)), (+ __ADDRESS_OF_ldv_current@ 6224), |ldv_init::var4@2|, (let ((.cse15 (+ __ADDRESS_OF_ldv_current@ 1840))) (let ((.cse0 (+ (+ __ADDRESS_OF_ldv_current@ 104) 40)) (.cse1 (+ (+ __ADDRESS_OF_ldv_current@ 480) 0)) (.cse2 (+ __ADDRESS_OF_ldv_current@ 1824)) (.cse3 (+ .cse15 8)) (.cse4 (+ .cse15 24)) (.cse5 (+ __ADDRESS_OF_ldv_current@ 2032)) (.cse6 (+ __ADDRESS_OF_ldv_current@ 2048)) (.cse7 (+ __ADDRESS_OF_ldv_current@ 2072)) (.cse8 (+ __ADDRESS_OF_ldv_current@ 2088)) (.cse9 (+ __ADDRESS_OF_ldv_current@ 2176)) (.cse10 (+ __ADDRESS_OF_ldv_current@ 2192)) (.cse11 (+ (+ __ADDRESS_OF_ldv_current@ 2376) (* 16 0))) (.cse12 (+ (+ __ADDRESS_OF_ldv_current@ 2728) 0)) (.cse13 (+ __ADDRESS_OF_ldv_current@ 6152)) (.cse14 (+ __ADDRESS_OF_ldv_current@ 6184))) (and (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 16) 0)) 0) (= (|*struct_list_head:next@1| (+ .cse0 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse0 8)) 0) (= (|*struct_list_head:next@1| (+ .cse1 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse1 8)) 0) (= (|*struct_list_head:next@1| (+ .cse2 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse2 8)) 0) (= (|*struct_list_head:next@1| (+ .cse3 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse3 8)) 0) (= (|*struct_list_head:next@1| (+ .cse4 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse4 8)) 0) (= (|*struct_list_head:next@1| (+ .cse5 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse5 8)) 0) (= (|*struct_list_head:next@1| (+ .cse6 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse6 8)) 0) (= (|*struct_list_head:next@1| (+ .cse7 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse7 8)) 0) (= (|*struct_list_head:next@1| (+ .cse8 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse8 8)) 0) (= (|*struct_list_head:next@1| (+ .cse9 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse9 8)) 0) (= (|*struct_list_head:next@1| (+ .cse10 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse10 8)) 0) (= (|*struct_list_head:next@1| (+ .cse11 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse11 8)) 0) (= (|*struct_list_head:next@1| (+ .cse12 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse12 8)) 0) (= (|*struct_list_head:next@1| (+ .cse13 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse13 8)) 0) (= (|*struct_list_head:next@1| (+ .cse14 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse14 8)) 0)))), (+ |__ADDRESS_OF_ldv_init::var1@| 4), (> |__ADDRESS_OF_ldv_init::var3@| (+ |__ADDRESS_OF_ldv_init::var1@| 4)), (|*struct_list_head:prev@1| (+ (+ (+ __ADDRESS_OF_ldv_current@ 1840) 24) 8)), (|*struct_list_head:next@1| (+ (+ (+ __ADDRESS_OF_ldv_current@ 2376) (* 16 0)) 0)), (let ((.cse15 (+ __ADDRESS_OF_ldv_current@ 6224)) (.cse17 (+ __ADDRESS_OF_ldv_current@ 1840))) (let ((.cse0 (+ (+ __ADDRESS_OF_ldv_current@ 104) 40)) (.cse1 (+ (+ __ADDRESS_OF_ldv_current@ 480) 0)) (.cse2 (+ __ADDRESS_OF_ldv_current@ 1824)) (.cse3 (+ .cse17 8)) (.cse4 (+ .cse17 24)) (.cse5 (+ __ADDRESS_OF_ldv_current@ 2032)) (.cse6 (+ __ADDRESS_OF_ldv_current@ 2048)) (.cse7 (+ __ADDRESS_OF_ldv_current@ 2072)) (.cse8 (+ __ADDRESS_OF_ldv_current@ 2088)) (.cse9 (+ __ADDRESS_OF_ldv_current@ 2176)) (.cse10 (+ __ADDRESS_OF_ldv_current@ 2192)) (.cse11 (+ (+ __ADDRESS_OF_ldv_current@ 2376) (* 16 0))) (.cse12 (+ (+ __ADDRESS_OF_ldv_current@ 2728) 0)) (.cse13 (+ __ADDRESS_OF_ldv_current@ 6152)) (.cse14 (+ __ADDRESS_OF_ldv_current@ 6184)) (.cse16 (+ .cse15 80))) (and (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 16) 0)) 0) (= (|*struct_list_head:next@1| (+ .cse0 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse0 8)) 0) (= (|*struct_list_head:next@1| (+ .cse1 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse1 8)) 0) (= (|*struct_list_head:next@1| (+ .cse2 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse2 8)) 0) (= (|*struct_list_head:next@1| (+ .cse3 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse3 8)) 0) (= (|*struct_list_head:next@1| (+ .cse4 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse4 8)) 0) (= (|*struct_list_head:next@1| (+ .cse5 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse5 8)) 0) (= (|*struct_list_head:next@1| (+ .cse6 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse6 8)) 0) (= (|*struct_list_head:next@1| (+ .cse7 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse7 8)) 0) (= (|*struct_list_head:next@1| (+ .cse8 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse8 8)) 0) (= (|*struct_list_head:next@1| (+ .cse9 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse9 8)) 0) (= (|*struct_list_head:next@1| (+ .cse10 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse10 8)) 0) (= (|*struct_list_head:next@1| (+ .cse11 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse11 8)) 0) (= (|*struct_list_head:next@1| (+ .cse12 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse12 8)) 0) (= (|*struct_list_head:next@1| (+ .cse13 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse13 8)) 0) (= (|*struct_list_head:next@1| (+ .cse14 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse14 8)) 0) (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ .cse15 0) 0)) 0) (= (|*struct_list_head:next@1| (+ .cse16 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse16 8)) 0)))), (= (|*struct_list_head:next@1| (+ (+ (+ __ADDRESS_OF_ldv_current@ 1840) 8) 0)) 0), (let ((.cse5 (+ __ADDRESS_OF_ldv_current@ 1840))) (let ((.cse0 (+ (+ __ADDRESS_OF_ldv_current@ 104) 40)) (.cse1 (+ (+ __ADDRESS_OF_ldv_current@ 480) 0)) (.cse2 (+ __ADDRESS_OF_ldv_current@ 1824)) (.cse3 (+ .cse5 8)) (.cse4 (+ .cse5 24))) (and (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 16) 0)) 0) (= (|*struct_list_head:next@1| (+ .cse0 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse0 8)) 0) (= (|*struct_list_head:next@1| (+ .cse1 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse1 8)) 0) (= (|*struct_list_head:next@1| (+ .cse2 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse2 8)) 0) (= (|*struct_list_head:next@1| (+ .cse3 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse3 8)) 0) (= (|*struct_list_head:next@1| (+ .cse4 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse4 8)) 0) (= (|*struct_list_head:next@1| (+ (+ __ADDRESS_OF_ldv_current@ 2032) 0)) 0)))), (|*struct_list_head:next@1| (+ (+ __ADDRESS_OF_ldv_current@ 2072) 0)), (= |ldv_undef_int::__retval__@3| |ldv_undef_int::undef_int@6|), (+ (+ __ADDRESS_OF_ldv_current@ 6184) 8), (let ((.cse0 (+ (+ __ADDRESS_OF_ldv_current@ 104) 40)) (.cse1 (+ (+ __ADDRESS_OF_ldv_current@ 480) 0))) (and (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 16) 0)) 0) (= (|*struct_list_head:next@1| (+ .cse0 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse0 8)) 0) (= (|*struct_list_head:next@1| (+ .cse1 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse1 8)) 0))), (= (|*struct_list_head:prev@1| (+ (+ __ADDRESS_OF_ldv_current@ 2072) 8)) 0), (|*struct_list_head:prev@1| (+ (+ __ADDRESS_OF_ldv_current@ 2088) 8)), ldv_initialize@, (= (|*struct_list_head:prev@1| (+ (+ __ADDRESS_OF_ldv_current@ 6152) 8)) 0), __VERIFIER_nondet_int!3@, (+ (+ (+ __ADDRESS_OF_ldv_current@ 2376) (* 16 0)) 8), (+ __ADDRESS_OF_ldv_current@ 10508), (|*struct_list_head:prev@1| (+ (+ (+ __ADDRESS_OF_ldv_current@ 104) 40) 8)), 104, 2376, 2032, (+ __ADDRESS_OF_ldv_current@ 104), (|*struct_list_head:next@1| (+ (+ __ADDRESS_OF_ldv_current@ 2032) 0)), (let ((.cse15 (+ __ADDRESS_OF_ldv_current@ 6224)) (.cse19 (+ __ADDRESS_OF_ldv_current@ 1840))) (let ((.cse0 (+ (+ __ADDRESS_OF_ldv_current@ 104) 40)) (.cse1 (+ (+ __ADDRESS_OF_ldv_current@ 480) 0)) (.cse2 (+ __ADDRESS_OF_ldv_current@ 1824)) (.cse3 (+ .cse19 8)) (.cse4 (+ .cse19 24)) (.cse5 (+ __ADDRESS_OF_ldv_current@ 2032)) (.cse6 (+ __ADDRESS_OF_ldv_current@ 2048)) (.cse7 (+ __ADDRESS_OF_ldv_current@ 2072)) (.cse8 (+ __ADDRESS_OF_ldv_current@ 2088)) (.cse9 (+ __ADDRESS_OF_ldv_current@ 2176)) (.cse10 (+ __ADDRESS_OF_ldv_current@ 2192)) (.cse11 (+ (+ __ADDRESS_OF_ldv_current@ 2376) (* 16 0))) (.cse12 (+ (+ __ADDRESS_OF_ldv_current@ 2728) 0)) (.cse13 (+ __ADDRESS_OF_ldv_current@ 6152)) (.cse14 (+ __ADDRESS_OF_ldv_current@ 6184)) (.cse16 (+ .cse15 80)) (.cse17 (+ __ADDRESS_OF_ldv_current@ 6392)) (.cse18 (+ __ADDRESS_OF_ldv_current@ 6472))) (and (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 16) 0)) 0) (= (|*struct_list_head:next@1| (+ .cse0 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse0 8)) 0) (= (|*struct_list_head:next@1| (+ .cse1 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse1 8)) 0) (= (|*struct_list_head:next@1| (+ .cse2 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse2 8)) 0) (= (|*struct_list_head:next@1| (+ .cse3 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse3 8)) 0) (= (|*struct_list_head:next@1| (+ .cse4 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse4 8)) 0) (= (|*struct_list_head:next@1| (+ .cse5 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse5 8)) 0) (= (|*struct_list_head:next@1| (+ .cse6 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse6 8)) 0) (= (|*struct_list_head:next@1| (+ .cse7 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse7 8)) 0) (= (|*struct_list_head:next@1| (+ .cse8 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse8 8)) 0) (= (|*struct_list_head:next@1| (+ .cse9 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse9 8)) 0) (= (|*struct_list_head:next@1| (+ .cse10 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse10 8)) 0) (= (|*struct_list_head:next@1| (+ .cse11 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse11 8)) 0) (= (|*struct_list_head:next@1| (+ .cse12 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse12 8)) 0) (= (|*struct_list_head:next@1| (+ .cse13 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse13 8)) 0) (= (|*struct_list_head:next@1| (+ .cse14 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse14 8)) 0) (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ .cse15 0) 0)) 0) (= (|*struct_list_head:next@1| (+ .cse16 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse16 8)) 0) (= (|*struct_list_head:next@1| (+ .cse17 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse17 8)) 0) (= (|*struct_list_head:next@1| (+ .cse18 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse18 8)) 0)))), (+ (+ (+ __ADDRESS_OF_ldv_current@ 2728) 0) 0), 8, (|*struct_list_head:next@1| (+ (+ __ADDRESS_OF_ldv_current@ 2192) 0)), (+ (+ __ADDRESS_OF_ldv_current@ 6472) 8), (let ((.cse13 (+ __ADDRESS_OF_ldv_current@ 1840))) (let ((.cse0 (+ (+ __ADDRESS_OF_ldv_current@ 104) 40)) (.cse1 (+ (+ __ADDRESS_OF_ldv_current@ 480) 0)) (.cse2 (+ __ADDRESS_OF_ldv_current@ 1824)) (.cse3 (+ .cse13 8)) (.cse4 (+ .cse13 24)) (.cse5 (+ __ADDRESS_OF_ldv_current@ 2032)) (.cse6 (+ __ADDRESS_OF_ldv_current@ 2048)) (.cse7 (+ __ADDRESS_OF_ldv_current@ 2072)) (.cse8 (+ __ADDRESS_OF_ldv_current@ 2088)) (.cse9 (+ __ADDRESS_OF_ldv_current@ 2176)) (.cse10 (+ __ADDRESS_OF_ldv_current@ 2192)) (.cse11 (+ (+ __ADDRESS_OF_ldv_current@ 2376) (* 16 0))) (.cse12 (+ (+ __ADDRESS_OF_ldv_current@ 2728) 0))) (and (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 16) 0)) 0) (= (|*struct_list_head:next@1| (+ .cse0 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse0 8)) 0) (= (|*struct_list_head:next@1| (+ .cse1 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse1 8)) 0) (= (|*struct_list_head:next@1| (+ .cse2 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse2 8)) 0) (= (|*struct_list_head:next@1| (+ .cse3 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse3 8)) 0) (= (|*struct_list_head:next@1| (+ .cse4 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse4 8)) 0) (= (|*struct_list_head:next@1| (+ .cse5 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse5 8)) 0) (= (|*struct_list_head:next@1| (+ .cse6 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse6 8)) 0) (= (|*struct_list_head:next@1| (+ .cse7 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse7 8)) 0) (= (|*struct_list_head:next@1| (+ .cse8 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse8 8)) 0) (= (|*struct_list_head:next@1| (+ .cse9 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse9 8)) 0) (= (|*struct_list_head:next@1| (+ .cse10 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse10 8)) 0) (= (|*struct_list_head:next@1| (+ .cse11 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse11 8)) 0) (= (|*struct_list_head:next@1| (+ .cse12 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse12 8)) 0)))), (not (= (|*int:global@3| |ldv_init::var2@2|) (|*int:global@3| |__ADDRESS_OF_ldv_init::var1@|))), |ldv_undef_int::__retval__@2|, (+ (+ __ADDRESS_OF_ldv_current@ 2176) 0), (let ((.cse15 (+ __ADDRESS_OF_ldv_current@ 6224)) (.cse17 (+ __ADDRESS_OF_ldv_current@ 1840))) (let ((.cse0 (+ (+ __ADDRESS_OF_ldv_current@ 104) 40)) (.cse1 (+ (+ __ADDRESS_OF_ldv_current@ 480) 0)) (.cse2 (+ __ADDRESS_OF_ldv_current@ 1824)) (.cse3 (+ .cse17 8)) (.cse4 (+ .cse17 24)) (.cse5 (+ __ADDRESS_OF_ldv_current@ 2032)) (.cse6 (+ __ADDRESS_OF_ldv_current@ 2048)) (.cse7 (+ __ADDRESS_OF_ldv_current@ 2072)) (.cse8 (+ __ADDRESS_OF_ldv_current@ 2088)) (.cse9 (+ __ADDRESS_OF_ldv_current@ 2176)) (.cse10 (+ __ADDRESS_OF_ldv_current@ 2192)) (.cse11 (+ (+ __ADDRESS_OF_ldv_current@ 2376) (* 16 0))) (.cse12 (+ (+ __ADDRESS_OF_ldv_current@ 2728) 0)) (.cse13 (+ __ADDRESS_OF_ldv_current@ 6152)) (.cse14 (+ __ADDRESS_OF_ldv_current@ 6184)) (.cse16 (+ .cse15 80))) (and (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 16) 0)) 0) (= (|*struct_list_head:next@1| (+ .cse0 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse0 8)) 0) (= (|*struct_list_head:next@1| (+ .cse1 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse1 8)) 0) (= (|*struct_list_head:next@1| (+ .cse2 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse2 8)) 0) (= (|*struct_list_head:next@1| (+ .cse3 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse3 8)) 0) (= (|*struct_list_head:next@1| (+ .cse4 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse4 8)) 0) (= (|*struct_list_head:next@1| (+ .cse5 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse5 8)) 0) (= (|*struct_list_head:next@1| (+ .cse6 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse6 8)) 0) (= (|*struct_list_head:next@1| (+ .cse7 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse7 8)) 0) (= (|*struct_list_head:next@1| (+ .cse8 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse8 8)) 0) (= (|*struct_list_head:next@1| (+ .cse9 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse9 8)) 0) (= (|*struct_list_head:next@1| (+ .cse10 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse10 8)) 0) (= (|*struct_list_head:next@1| (+ .cse11 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse11 8)) 0) (= (|*struct_list_head:next@1| (+ .cse12 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse12 8)) 0) (= (|*struct_list_head:next@1| (+ .cse13 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse13 8)) 0) (= (|*struct_list_head:next@1| (+ .cse14 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse14 8)) 0) (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ .cse15 0) 0)) 0) (= (|*struct_list_head:next@1| (+ .cse16 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse16 8)) 0) (= (|*struct_list_head:next@1| (+ (+ __ADDRESS_OF_ldv_current@ 6392) 0)) 0)))), (let ((.cse0 (+ (+ __ADDRESS_OF_ldv_current@ 104) 40))) (and (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 16) 0)) 0) (= (|*struct_list_head:next@1| (+ .cse0 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse0 8)) 0))), (+ |__ADDRESS_OF_ldv_init::var1@| 0), (let ((.cse6 (+ __ADDRESS_OF_ldv_current@ 1840))) (let ((.cse0 (+ (+ __ADDRESS_OF_ldv_current@ 104) 40)) (.cse1 (+ (+ __ADDRESS_OF_ldv_current@ 480) 0)) (.cse2 (+ __ADDRESS_OF_ldv_current@ 1824)) (.cse3 (+ .cse6 8)) (.cse4 (+ .cse6 24)) (.cse5 (+ __ADDRESS_OF_ldv_current@ 2032))) (and (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 16) 0)) 0) (= (|*struct_list_head:next@1| (+ .cse0 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse0 8)) 0) (= (|*struct_list_head:next@1| (+ .cse1 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse1 8)) 0) (= (|*struct_list_head:next@1| (+ .cse2 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse2 8)) 0) (= (|*struct_list_head:next@1| (+ .cse3 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse3 8)) 0) (= (|*struct_list_head:next@1| (+ .cse4 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse4 8)) 0) (= (|*struct_list_head:next@1| (+ .cse5 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse5 8)) 0)))), (+ (+ __ADDRESS_OF_ldv_current@ 10508) 0), (* 16 0), (> |__ADDRESS_OF_ldv_init::var1@| (+ __ADDRESS_OF_ldv_current@ 10608)), (|*int:global@2| (+ |__ADDRESS_OF_ldv_init::var1@| 0)), (+ __ADDRESS_OF_ldv_current@ 1840), (= (|*struct_list_head:next@1| (+ (+ (+ __ADDRESS_OF_ldv_current@ 2728) 0) 0)) 0), (+ __ADDRESS_OF_ldv_current@ 2032), (+ __ADDRESS_OF_ldv_current@ 2088), true, (+ __ADDRESS_OF_ldv_current@ 2176), (+ (+ __ADDRESS_OF_ldv_current@ 10504) 0), (let ((.cse10 (+ __ADDRESS_OF_ldv_current@ 1840))) (let ((.cse0 (+ (+ __ADDRESS_OF_ldv_current@ 104) 40)) (.cse1 (+ (+ __ADDRESS_OF_ldv_current@ 480) 0)) (.cse2 (+ __ADDRESS_OF_ldv_current@ 1824)) (.cse3 (+ .cse10 8)) (.cse4 (+ .cse10 24)) (.cse5 (+ __ADDRESS_OF_ldv_current@ 2032)) (.cse6 (+ __ADDRESS_OF_ldv_current@ 2048)) (.cse7 (+ __ADDRESS_OF_ldv_current@ 2072)) (.cse8 (+ __ADDRESS_OF_ldv_current@ 2088)) (.cse9 (+ __ADDRESS_OF_ldv_current@ 2176))) (and (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 16) 0)) 0) (= (|*struct_list_head:next@1| (+ .cse0 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse0 8)) 0) (= (|*struct_list_head:next@1| (+ .cse1 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse1 8)) 0) (= (|*struct_list_head:next@1| (+ .cse2 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse2 8)) 0) (= (|*struct_list_head:next@1| (+ .cse3 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse3 8)) 0) (= (|*struct_list_head:next@1| (+ .cse4 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse4 8)) 0) (= (|*struct_list_head:next@1| (+ .cse5 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse5 8)) 0) (= (|*struct_list_head:next@1| (+ .cse6 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse6 8)) 0) (= (|*struct_list_head:next@1| (+ .cse7 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse7 8)) 0) (= (|*struct_list_head:next@1| (+ .cse8 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse8 8)) 0) (= (|*struct_list_head:next@1| (+ .cse9 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse9 8)) 0) (= (|*struct_list_head:next@1| (+ (+ __ADDRESS_OF_ldv_current@ 2192) 0)) 0)))), (+ (+ (+ __ADDRESS_OF_ldv_current@ 480) 0) 8), (|*struct_list_head:prev@1| (+ (+ (+ __ADDRESS_OF_ldv_current@ 6224) 80) 8)), (+ __ADDRESS_OF_ldv_current@ 2728), (let ((.cse1 (+ |__ADDRESS_OF_ldv_init::var1@| 4))) (and (> |__ADDRESS_OF_ldv_init::var1@| (+ __ADDRESS_OF_ldv_current@ 10608)) (let ((.cse0 (- |__ADDRESS_OF_ldv_init::var1@| 0))) (= .cse0 (* 4 (div .cse0 4)))) (> .cse1 0) (> |__ADDRESS_OF_ldv_init::var3@| .cse1) (let ((.cse2 (- |__ADDRESS_OF_ldv_init::var3@| 0))) (= .cse2 (* 4 (div .cse2 4)))) (> (+ |__ADDRESS_OF_ldv_init::var3@| 4) 0))), 1, 16, (= |ldv_undef_int::undef_int@6| __VERIFIER_nondet_int!3@), (|*int:global@3| |__ADDRESS_OF_ldv_init::var3@|), (|*struct_list_head:prev@1| (+ (+ __ADDRESS_OF_ldv_current@ 6392) 8)), (|*int:global@3| (+ |__ADDRESS_OF_ldv_init::var1@| 0)), (+ (+ __ADDRESS_OF_ldv_current@ 2176) 8), (|*struct_list_head:prev@1| (+ (+ __ADDRESS_OF_ldv_current@ 6184) 8)), (div (- |__ADDRESS_OF_ldv_init::var1@| 0) 4), (= (|*struct_list_head:prev@1| (+ (+ __ADDRESS_OF_ldv_current@ 2032) 8)) 0), (= (|*struct_list_head:next@1| (+ (+ __ADDRESS_OF_ldv_current@ 2048) 0)) 0), (> (+ |__ADDRESS_OF_ldv_init::var1@| 4) 0), (let ((.cse5 (+ __ADDRESS_OF_ldv_current@ 1840))) (let ((.cse0 (+ (+ __ADDRESS_OF_ldv_current@ 104) 40)) (.cse1 (+ (+ __ADDRESS_OF_ldv_current@ 480) 0)) (.cse2 (+ __ADDRESS_OF_ldv_current@ 1824)) (.cse3 (+ .cse5 8)) (.cse4 (+ .cse5 24))) (and (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 16) 0)) 0) (= (|*struct_list_head:next@1| (+ .cse0 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse0 8)) 0) (= (|*struct_list_head:next@1| (+ .cse1 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse1 8)) 0) (= (|*struct_list_head:next@1| (+ .cse2 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse2 8)) 0) (= (|*struct_list_head:next@1| (+ .cse3 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse3 8)) 0) (= (|*struct_list_head:next@1| (+ .cse4 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse4 8)) 0)))), (|*struct_list_head:next@1| (+ (+ __ADDRESS_OF_ldv_current@ 2048) 0)), (= (|*struct_list_head:prev@1| (+ (+ (+ __ADDRESS_OF_ldv_current@ 2376) (* 16 0)) 8)) 0), 6184, (|*struct_list_head:next@1| (+ (+ (+ __ADDRESS_OF_ldv_current@ 1840) 8) 0)), (|*struct_list_head:next@1| (+ (+ __ADDRESS_OF_ldv_current@ 2176) 0)), false, (+ (+ __ADDRESS_OF_ldv_current@ 6224) 0), (let ((.cse15 (+ __ADDRESS_OF_ldv_current@ 1840))) (let ((.cse0 (+ (+ __ADDRESS_OF_ldv_current@ 104) 40)) (.cse1 (+ (+ __ADDRESS_OF_ldv_current@ 480) 0)) (.cse2 (+ __ADDRESS_OF_ldv_current@ 1824)) (.cse3 (+ .cse15 8)) (.cse4 (+ .cse15 24)) (.cse5 (+ __ADDRESS_OF_ldv_current@ 2032)) (.cse6 (+ __ADDRESS_OF_ldv_current@ 2048)) (.cse7 (+ __ADDRESS_OF_ldv_current@ 2072)) (.cse8 (+ __ADDRESS_OF_ldv_current@ 2088)) (.cse9 (+ __ADDRESS_OF_ldv_current@ 2176)) (.cse10 (+ __ADDRESS_OF_ldv_current@ 2192)) (.cse11 (+ (+ __ADDRESS_OF_ldv_current@ 2376) (* 16 0))) (.cse12 (+ (+ __ADDRESS_OF_ldv_current@ 2728) 0)) (.cse13 (+ __ADDRESS_OF_ldv_current@ 6152)) (.cse14 (+ __ADDRESS_OF_ldv_current@ 6184))) (and (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 16) 0)) 0) (= (|*struct_list_head:next@1| (+ .cse0 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse0 8)) 0) (= (|*struct_list_head:next@1| (+ .cse1 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse1 8)) 0) (= (|*struct_list_head:next@1| (+ .cse2 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse2 8)) 0) (= (|*struct_list_head:next@1| (+ .cse3 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse3 8)) 0) (= (|*struct_list_head:next@1| (+ .cse4 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse4 8)) 0) (= (|*struct_list_head:next@1| (+ .cse5 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse5 8)) 0) (= (|*struct_list_head:next@1| (+ .cse6 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse6 8)) 0) (= (|*struct_list_head:next@1| (+ .cse7 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse7 8)) 0) (= (|*struct_list_head:next@1| (+ .cse8 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse8 8)) 0) (= (|*struct_list_head:next@1| (+ .cse9 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse9 8)) 0) (= (|*struct_list_head:next@1| (+ .cse10 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse10 8)) 0) (= (|*struct_list_head:next@1| (+ .cse11 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse11 8)) 0) (= (|*struct_list_head:next@1| (+ .cse12 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse12 8)) 0) (= (|*struct_list_head:next@1| (+ .cse13 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse13 8)) 0) (= (|*struct_list_head:next@1| (+ .cse14 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse14 8)) 0) (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ (+ __ADDRESS_OF_ldv_current@ 6224) 0) 0)) 0)))), (+ (+ __ADDRESS_OF_ldv_current@ 2088) 0), (= (|*struct_list_head:prev@1| (+ (+ __ADDRESS_OF_ldv_current@ 1824) 8)) 0), (+ (+ __ADDRESS_OF_ldv_current@ 6224) 80), (+ (+ (+ __ADDRESS_OF_ldv_current@ 1840) 24) 0), (> __ADDRESS_OF_ldv_current@ 0), (+ (+ __ADDRESS_OF_ldv_current@ 6392) 0), (+ (+ __ADDRESS_OF_ldv_current@ 6392) 8), (|*struct_list_head:prev@1| (+ (+ (+ __ADDRESS_OF_ldv_current@ 1840) 8) 8)), __-Infinity__, (+ (+ (+ __ADDRESS_OF_ldv_current@ 104) 40) 8), (|*struct_list_head:prev@1| (+ (+ __ADDRESS_OF_ldv_current@ 2192) 8)), (= |ldv_init::var4@2| |__ADDRESS_OF_ldv_init::var3@|), ldv_is_memory_alloc_failures@3, (+ (+ __ADDRESS_OF_ldv_current@ 6152) 8), (+ (+ (+ __ADDRESS_OF_ldv_current@ 104) 40) 0), (+ __ADDRESS_OF_ldv_current@ 6152), (= (|*struct_list_head:next@1| (+ (+ __ADDRESS_OF_ldv_current@ 6472) 0)) 0), (= (|*struct_list_head:prev@1| (+ (+ (+ __ADDRESS_OF_ldv_current@ 2728) 0) 8)) 0), (and (> |__ADDRESS_OF_ldv_init::var3@| (+ |__ADDRESS_OF_ldv_init::var1@| 4)) (let ((.cse0 (- |__ADDRESS_OF_ldv_init::var3@| 0))) (= .cse0 (* 4 (div .cse0 4)))) (> (+ |__ADDRESS_OF_ldv_init::var3@| 4) 0)), (= (|*int:global@2| |ldv_init::var2@1|) (|*int:global@2| |__ADDRESS_OF_ldv_init::var1@|)), 480, (let ((.cse8 (+ __ADDRESS_OF_ldv_current@ 1840))) (let ((.cse0 (+ (+ __ADDRESS_OF_ldv_current@ 104) 40)) (.cse1 (+ (+ __ADDRESS_OF_ldv_current@ 480) 0)) (.cse2 (+ __ADDRESS_OF_ldv_current@ 1824)) (.cse3 (+ .cse8 8)) (.cse4 (+ .cse8 24)) (.cse5 (+ __ADDRESS_OF_ldv_current@ 2032)) (.cse6 (+ __ADDRESS_OF_ldv_current@ 2048)) (.cse7 (+ __ADDRESS_OF_ldv_current@ 2072))) (and (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 16) 0)) 0) (= (|*struct_list_head:next@1| (+ .cse0 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse0 8)) 0) (= (|*struct_list_head:next@1| (+ .cse1 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse1 8)) 0) (= (|*struct_list_head:next@1| (+ .cse2 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse2 8)) 0) (= (|*struct_list_head:next@1| (+ .cse3 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse3 8)) 0) (= (|*struct_list_head:next@1| (+ .cse4 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse4 8)) 0) (= (|*struct_list_head:next@1| (+ .cse5 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse5 8)) 0) (= (|*struct_list_head:next@1| (+ .cse6 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse6 8)) 0) (= (|*struct_list_head:next@1| (+ .cse7 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse7 8)) 0)))), (|*struct_list_head:next@1| (+ (+ __ADDRESS_OF_ldv_current@ 2088) 0)), (= (|*struct_list_head:prev@1| (+ (+ __ADDRESS_OF_ldv_current@ 2192) 8)) 0), (+ __ADDRESS_OF_ldv_current@ 6184), 2072, (+ (+ __ADDRESS_OF_ldv_current@ 2048) 0), (+ (+ (+ __ADDRESS_OF_ldv_current@ 6224) 0) 0), (+ __ADDRESS_OF_ldv_current@ 10504), 2048, (= (|*int:global@3| |ldv_init::var2@2|) (|*int:global@3| |__ADDRESS_OF_ldv_init::var1@|)), |ldv_init::var2|, (|*int:global@1| (+ |__ADDRESS_OF_ldv_init::var1@| 0)), 6224, (+ (+ __ADDRESS_OF_ldv_current@ 1840) 24), (let ((.cse7 (+ __ADDRESS_OF_ldv_current@ 1840))) (let ((.cse0 (+ (+ __ADDRESS_OF_ldv_current@ 104) 40)) (.cse1 (+ (+ __ADDRESS_OF_ldv_current@ 480) 0)) (.cse2 (+ __ADDRESS_OF_ldv_current@ 1824)) (.cse3 (+ .cse7 8)) (.cse4 (+ .cse7 24)) (.cse5 (+ __ADDRESS_OF_ldv_current@ 2032)) (.cse6 (+ __ADDRESS_OF_ldv_current@ 2048))) (and (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 16) 0)) 0) (= (|*struct_list_head:next@1| (+ .cse0 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse0 8)) 0) (= (|*struct_list_head:next@1| (+ .cse1 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse1 8)) 0) (= (|*struct_list_head:next@1| (+ .cse2 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse2 8)) 0) (= (|*struct_list_head:next@1| (+ .cse3 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse3 8)) 0) (= (|*struct_list_head:next@1| (+ .cse4 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse4 8)) 0) (= (|*struct_list_head:next@1| (+ .cse5 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse5 8)) 0) (= (|*struct_list_head:next@1| (+ .cse6 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse6 8)) 0) (= (|*struct_list_head:next@1| (+ (+ __ADDRESS_OF_ldv_current@ 2072) 0)) 0)))), (|*struct_list_head:prev@1| (+ (+ __ADDRESS_OF_ldv_current@ 6152) 8)), (and (> |__ADDRESS_OF_ldv_init::var1@| (+ __ADDRESS_OF_ldv_current@ 10608)) (let ((.cse0 (- |__ADDRESS_OF_ldv_init::var1@| 0))) (= .cse0 (* 4 (div .cse0 4)))) (> (+ |__ADDRESS_OF_ldv_init::var1@| 4) 0)), (let ((.cse12 (+ __ADDRESS_OF_ldv_current@ 1840))) (let ((.cse0 (+ (+ __ADDRESS_OF_ldv_current@ 104) 40)) (.cse1 (+ (+ __ADDRESS_OF_ldv_current@ 480) 0)) (.cse2 (+ __ADDRESS_OF_ldv_current@ 1824)) (.cse3 (+ .cse12 8)) (.cse4 (+ .cse12 24)) (.cse5 (+ __ADDRESS_OF_ldv_current@ 2032)) (.cse6 (+ __ADDRESS_OF_ldv_current@ 2048)) (.cse7 (+ __ADDRESS_OF_ldv_current@ 2072)) (.cse8 (+ __ADDRESS_OF_ldv_current@ 2088)) (.cse9 (+ __ADDRESS_OF_ldv_current@ 2176)) (.cse10 (+ __ADDRESS_OF_ldv_current@ 2192)) (.cse11 (+ (+ __ADDRESS_OF_ldv_current@ 2376) (* 16 0)))) (and (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 16) 0)) 0) (= (|*struct_list_head:next@1| (+ .cse0 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse0 8)) 0) (= (|*struct_list_head:next@1| (+ .cse1 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse1 8)) 0) (= (|*struct_list_head:next@1| (+ .cse2 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse2 8)) 0) (= (|*struct_list_head:next@1| (+ .cse3 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse3 8)) 0) (= (|*struct_list_head:next@1| (+ .cse4 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse4 8)) 0) (= (|*struct_list_head:next@1| (+ .cse5 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse5 8)) 0) (= (|*struct_list_head:next@1| (+ .cse6 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse6 8)) 0) (= (|*struct_list_head:next@1| (+ .cse7 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse7 8)) 0) (= (|*struct_list_head:next@1| (+ .cse8 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse8 8)) 0) (= (|*struct_list_head:next@1| (+ .cse9 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse9 8)) 0) (= (|*struct_list_head:next@1| (+ .cse10 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse10 8)) 0) (= (|*struct_list_head:next@1| (+ .cse11 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse11 8)) 0) (= (|*struct_list_head:next@1| (+ (+ (+ __ADDRESS_OF_ldv_current@ 2728) 0) 0)) 0)))), (|*struct_list_head:prev@1| (+ (+ __ADDRESS_OF_ldv_current@ 1824) 8)), (> (+ |__ADDRESS_OF_ldv_init::var3@| 4) 0), (+ (+ __ADDRESS_OF_ldv_current@ 2032) 0), (= (|*struct_list_head:prev@1| (+ (+ __ADDRESS_OF_ldv_current@ 6472) 8)) 0), (and (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 16) 0)) 0) (= (|*struct_list_head:next@1| (+ (+ (+ __ADDRESS_OF_ldv_current@ 104) 40) 0)) 0)), PRED1, (+ (+ __ADDRESS_OF_ldv_current@ 480) 0), |__ADDRESS_OF_ldv_init::var3@|, __VERIFIER_error@, (= (|*int:global@2| |__ADDRESS_OF_ldv_init::var1@|) |ldv_undef_int::__retval__@2|), (+ (+ __ADDRESS_OF_ldv_current@ 2072) 0), (= (|*struct_list_head:next@1| (+ (+ (+ __ADDRESS_OF_ldv_current@ 1840) 24) 0)) 0), (+ (+ __ADDRESS_OF_ldv_current@ 2072) 8), (and (= (|*int:global@3| |__ADDRESS_OF_ldv_init::var3@|) |ldv_undef_int::__retval__@3|) (let ((.cse0 (+ |__ADDRESS_OF_ldv_init::var1@| 0))) (= (|*int:global@3| .cse0) (|*int:global@2| .cse0)))), 2728, (let ((.cse15 (+ __ADDRESS_OF_ldv_current@ 6224)) (.cse20 (+ __ADDRESS_OF_ldv_current@ 1840))) (let ((.cse0 (+ (+ __ADDRESS_OF_ldv_current@ 104) 40)) (.cse1 (+ (+ __ADDRESS_OF_ldv_current@ 480) 0)) (.cse2 (+ __ADDRESS_OF_ldv_current@ 1824)) (.cse3 (+ .cse20 8)) (.cse4 (+ .cse20 24)) (.cse5 (+ __ADDRESS_OF_ldv_current@ 2032)) (.cse6 (+ __ADDRESS_OF_ldv_current@ 2048)) (.cse7 (+ __ADDRESS_OF_ldv_current@ 2072)) (.cse8 (+ __ADDRESS_OF_ldv_current@ 2088)) (.cse9 (+ __ADDRESS_OF_ldv_current@ 2176)) (.cse10 (+ __ADDRESS_OF_ldv_current@ 2192)) (.cse11 (+ (+ __ADDRESS_OF_ldv_current@ 2376) (* 16 0))) (.cse12 (+ (+ __ADDRESS_OF_ldv_current@ 2728) 0)) (.cse13 (+ __ADDRESS_OF_ldv_current@ 6152)) (.cse14 (+ __ADDRESS_OF_ldv_current@ 6184)) (.cse16 (+ .cse15 80)) (.cse17 (+ __ADDRESS_OF_ldv_current@ 6392)) (.cse18 (+ __ADDRESS_OF_ldv_current@ 6472))) (and (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 16) 0)) 0) (= (|*struct_list_head:next@1| (+ .cse0 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse0 8)) 0) (= (|*struct_list_head:next@1| (+ .cse1 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse1 8)) 0) (= (|*struct_list_head:next@1| (+ .cse2 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse2 8)) 0) (= (|*struct_list_head:next@1| (+ .cse3 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse3 8)) 0) (= (|*struct_list_head:next@1| (+ .cse4 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse4 8)) 0) (= (|*struct_list_head:next@1| (+ .cse5 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse5 8)) 0) (= (|*struct_list_head:next@1| (+ .cse6 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse6 8)) 0) (= (|*struct_list_head:next@1| (+ .cse7 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse7 8)) 0) (= (|*struct_list_head:next@1| (+ .cse8 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse8 8)) 0) (= (|*struct_list_head:next@1| (+ .cse9 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse9 8)) 0) (= (|*struct_list_head:next@1| (+ .cse10 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse10 8)) 0) (= (|*struct_list_head:next@1| (+ .cse11 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse11 8)) 0) (= (|*struct_list_head:next@1| (+ .cse12 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse12 8)) 0) (= (|*struct_list_head:next@1| (+ .cse13 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse13 8)) 0) (= (|*struct_list_head:next@1| (+ .cse14 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse14 8)) 0) (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ .cse15 0) 0)) 0) (= (|*struct_list_head:next@1| (+ .cse16 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse16 8)) 0) (= (|*struct_list_head:next@1| (+ .cse17 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse17 8)) 0) (= (|*struct_list_head:next@1| (+ .cse18 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse18 8)) 0) (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 10504) 0)) 0) (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 10508) 0)) 0) (> __ADDRESS_OF_ldv_current@ 0) (let ((.cse19 (- __ADDRESS_OF_ldv_current@ 0))) (= .cse19 (* 8 (div .cse19 8)))) (> (+ __ADDRESS_OF_ldv_current@ 10608) 0) (= ldv_is_memory_alloc_failures@3 1)))), (let ((.cse0 (- |__ADDRESS_OF_ldv_init::var1@| 0))) (= .cse0 (* 4 (div .cse0 4)))), __VERIFIER_nondet_int!2@, (|*struct_list_head:next@1| (+ (+ __ADDRESS_OF_ldv_current@ 1824) 0)), (let ((.cse14 (+ __ADDRESS_OF_ldv_current@ 1840))) (let ((.cse0 (+ (+ __ADDRESS_OF_ldv_current@ 104) 40)) (.cse1 (+ (+ __ADDRESS_OF_ldv_current@ 480) 0)) (.cse2 (+ __ADDRESS_OF_ldv_current@ 1824)) (.cse3 (+ .cse14 8)) (.cse4 (+ .cse14 24)) (.cse5 (+ __ADDRESS_OF_ldv_current@ 2032)) (.cse6 (+ __ADDRESS_OF_ldv_current@ 2048)) (.cse7 (+ __ADDRESS_OF_ldv_current@ 2072)) (.cse8 (+ __ADDRESS_OF_ldv_current@ 2088)) (.cse9 (+ __ADDRESS_OF_ldv_current@ 2176)) (.cse10 (+ __ADDRESS_OF_ldv_current@ 2192)) (.cse11 (+ (+ __ADDRESS_OF_ldv_current@ 2376) (* 16 0))) (.cse12 (+ (+ __ADDRESS_OF_ldv_current@ 2728) 0)) (.cse13 (+ __ADDRESS_OF_ldv_current@ 6152))) (and (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 16) 0)) 0) (= (|*struct_list_head:next@1| (+ .cse0 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse0 8)) 0) (= (|*struct_list_head:next@1| (+ .cse1 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse1 8)) 0) (= (|*struct_list_head:next@1| (+ .cse2 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse2 8)) 0) (= (|*struct_list_head:next@1| (+ .cse3 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse3 8)) 0) (= (|*struct_list_head:next@1| (+ .cse4 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse4 8)) 0) (= (|*struct_list_head:next@1| (+ .cse5 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse5 8)) 0) (= (|*struct_list_head:next@1| (+ .cse6 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse6 8)) 0) (= (|*struct_list_head:next@1| (+ .cse7 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse7 8)) 0) (= (|*struct_list_head:next@1| (+ .cse8 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse8 8)) 0) (= (|*struct_list_head:next@1| (+ .cse9 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse9 8)) 0) (= (|*struct_list_head:next@1| (+ .cse10 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse10 8)) 0) (= (|*struct_list_head:next@1| (+ .cse11 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse11 8)) 0) (= (|*struct_list_head:next@1| (+ .cse12 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse12 8)) 0) (= (|*struct_list_head:next@1| (+ .cse13 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse13 8)) 0) (= (|*struct_list_head:next@1| (+ (+ __ADDRESS_OF_ldv_current@ 6184) 0)) 0)))), (* 4 (div (- |__ADDRESS_OF_ldv_init::var3@| 0) 4)), (let ((.cse0 (+ (+ __ADDRESS_OF_ldv_current@ 104) 40)) (.cse1 (+ (+ __ADDRESS_OF_ldv_current@ 480) 0)) (.cse2 (+ __ADDRESS_OF_ldv_current@ 1824))) (and (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 16) 0)) 0) (= (|*struct_list_head:next@1| (+ .cse0 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse0 8)) 0) (= (|*struct_list_head:next@1| (+ .cse1 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse1 8)) 0) (= (|*struct_list_head:next@1| (+ .cse2 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse2 8)) 0) (= (|*struct_list_head:next@1| (+ (+ (+ __ADDRESS_OF_ldv_current@ 1840) 8) 0)) 0))), (> (+ __ADDRESS_OF_ldv_current@ 10608) 0), (+ __ADDRESS_OF_ldv_current@ 2048), (ite (not (= (|*int:global@2| |ldv_init::var2@1|) (|*int:global@2| |__ADDRESS_OF_ldv_init::var1@|))) 1 0), (let ((.cse0 (+ (+ __ADDRESS_OF_ldv_current@ 104) 40))) (and (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 16) 0)) 0) (= (|*struct_list_head:next@1| (+ .cse0 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse0 8)) 0) (= (|*struct_list_head:next@1| (+ (+ (+ __ADDRESS_OF_ldv_current@ 480) 0) 0)) 0))), 10608, (|*struct_list_head:prev@1| (+ (+ (+ __ADDRESS_OF_ldv_current@ 2728) 0) 8)), __ADDRESS_OF_ldv_current@, 1840, 6392, (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ (+ __ADDRESS_OF_ldv_current@ 6224) 0) 0)), (+ (+ __ADDRESS_OF_ldv_current@ 2192) 8), (|*struct_list_head:prev@1| (+ (+ (+ __ADDRESS_OF_ldv_current@ 2376) (* 16 0)) 8)), (|*struct_list_head:prev@1| (+ (+ __ADDRESS_OF_ldv_current@ 2032) 8)), (+ (+ __ADDRESS_OF_ldv_current@ 2048) 8), (= |ldv_undef_int::undef_int@3| __VERIFIER_nondet_int!2@), (+ (+ (+ __ADDRESS_OF_ldv_current@ 2728) 0) 8), (let ((.cse7 (+ __ADDRESS_OF_ldv_current@ 1840))) (let ((.cse0 (+ (+ __ADDRESS_OF_ldv_current@ 104) 40)) (.cse1 (+ (+ __ADDRESS_OF_ldv_current@ 480) 0)) (.cse2 (+ __ADDRESS_OF_ldv_current@ 1824)) (.cse3 (+ .cse7 8)) (.cse4 (+ .cse7 24)) (.cse5 (+ __ADDRESS_OF_ldv_current@ 2032)) (.cse6 (+ __ADDRESS_OF_ldv_current@ 2048))) (and (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 16) 0)) 0) (= (|*struct_list_head:next@1| (+ .cse0 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse0 8)) 0) (= (|*struct_list_head:next@1| (+ .cse1 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse1 8)) 0) (= (|*struct_list_head:next@1| (+ .cse2 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse2 8)) 0) (= (|*struct_list_head:next@1| (+ .cse3 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse3 8)) 0) (= (|*struct_list_head:next@1| (+ .cse4 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse4 8)) 0) (= (|*struct_list_head:next@1| (+ .cse5 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse5 8)) 0) (= (|*struct_list_head:next@1| (+ .cse6 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse6 8)) 0)))), (= (|*struct_list_head:next@1| (+ (+ __ADDRESS_OF_ldv_current@ 6152) 0)) 0), (|*int:global@2| |__ADDRESS_OF_ldv_init::var3@|), (let ((.cse16 (+ __ADDRESS_OF_ldv_current@ 1840))) (let ((.cse0 (+ (+ __ADDRESS_OF_ldv_current@ 104) 40)) (.cse1 (+ (+ __ADDRESS_OF_ldv_current@ 480) 0)) (.cse2 (+ __ADDRESS_OF_ldv_current@ 1824)) (.cse3 (+ .cse16 8)) (.cse4 (+ .cse16 24)) (.cse5 (+ __ADDRESS_OF_ldv_current@ 2032)) (.cse6 (+ __ADDRESS_OF_ldv_current@ 2048)) (.cse7 (+ __ADDRESS_OF_ldv_current@ 2072)) (.cse8 (+ __ADDRESS_OF_ldv_current@ 2088)) (.cse9 (+ __ADDRESS_OF_ldv_current@ 2176)) (.cse10 (+ __ADDRESS_OF_ldv_current@ 2192)) (.cse11 (+ (+ __ADDRESS_OF_ldv_current@ 2376) (* 16 0))) (.cse12 (+ (+ __ADDRESS_OF_ldv_current@ 2728) 0)) (.cse13 (+ __ADDRESS_OF_ldv_current@ 6152)) (.cse14 (+ __ADDRESS_OF_ldv_current@ 6184)) (.cse15 (+ __ADDRESS_OF_ldv_current@ 6224))) (and (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 16) 0)) 0) (= (|*struct_list_head:next@1| (+ .cse0 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse0 8)) 0) (= (|*struct_list_head:next@1| (+ .cse1 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse1 8)) 0) (= (|*struct_list_head:next@1| (+ .cse2 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse2 8)) 0) (= (|*struct_list_head:next@1| (+ .cse3 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse3 8)) 0) (= (|*struct_list_head:next@1| (+ .cse4 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse4 8)) 0) (= (|*struct_list_head:next@1| (+ .cse5 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse5 8)) 0) (= (|*struct_list_head:next@1| (+ .cse6 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse6 8)) 0) (= (|*struct_list_head:next@1| (+ .cse7 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse7 8)) 0) (= (|*struct_list_head:next@1| (+ .cse8 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse8 8)) 0) (= (|*struct_list_head:next@1| (+ .cse9 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse9 8)) 0) (= (|*struct_list_head:next@1| (+ .cse10 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse10 8)) 0) (= (|*struct_list_head:next@1| (+ .cse11 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse11 8)) 0) (= (|*struct_list_head:next@1| (+ .cse12 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse12 8)) 0) (= (|*struct_list_head:next@1| (+ .cse13 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse13 8)) 0) (= (|*struct_list_head:next@1| (+ .cse14 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse14 8)) 0) (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ .cse15 0) 0)) 0) (= (|*struct_list_head:next@1| (+ (+ .cse15 80) 0)) 0)))), (- |__ADDRESS_OF_ldv_init::var3@| 0), (= (|*struct_list_head:prev@1| (+ (+ (+ __ADDRESS_OF_ldv_current@ 104) 40) 8)) 0), (- |__ADDRESS_OF_ldv_init::var1@| 0), (let ((.cse0 (+ (+ __ADDRESS_OF_ldv_current@ 104) 40)) (.cse1 (+ (+ __ADDRESS_OF_ldv_current@ 480) 0))) (and (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 16) 0)) 0) (= (|*struct_list_head:next@1| (+ .cse0 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse0 8)) 0) (= (|*struct_list_head:next@1| (+ .cse1 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse1 8)) 0) (= (|*struct_list_head:next@1| (+ (+ __ADDRESS_OF_ldv_current@ 1824) 0)) 0))), (= (|*struct_list_head:next@1| (+ (+ __ADDRESS_OF_ldv_current@ 6392) 0)) 0), |ldv_undef_int::__retval__@3|, (= (|*struct_list_head:prev@1| (+ (+ (+ __ADDRESS_OF_ldv_current@ 1840) 24) 8)) 0), (= (|*struct_list_head:next@1| (+ (+ (+ __ADDRESS_OF_ldv_current@ 480) 0) 0)) 0), (= (|*struct_list_head:next@1| (+ (+ (+ __ADDRESS_OF_ldv_current@ 6224) 80) 0)) 0), 10508, (+ __ADDRESS_OF_ldv_current@ 2192), (= (|*struct_list_head:next@1| (+ (+ (+ __ADDRESS_OF_ldv_current@ 104) 40) 0)) 0), (+ (+ __ADDRESS_OF_ldv_current@ 2376) (* 16 0)), (|*int:global@3| |__ADDRESS_OF_ldv_init::var1@|), (let ((.cse15 (+ __ADDRESS_OF_ldv_current@ 6224)) (.cse18 (+ __ADDRESS_OF_ldv_current@ 1840))) (let ((.cse0 (+ (+ __ADDRESS_OF_ldv_current@ 104) 40)) (.cse1 (+ (+ __ADDRESS_OF_ldv_current@ 480) 0)) (.cse2 (+ __ADDRESS_OF_ldv_current@ 1824)) (.cse3 (+ .cse18 8)) (.cse4 (+ .cse18 24)) (.cse5 (+ __ADDRESS_OF_ldv_current@ 2032)) (.cse6 (+ __ADDRESS_OF_ldv_current@ 2048)) (.cse7 (+ __ADDRESS_OF_ldv_current@ 2072)) (.cse8 (+ __ADDRESS_OF_ldv_current@ 2088)) (.cse9 (+ __ADDRESS_OF_ldv_current@ 2176)) (.cse10 (+ __ADDRESS_OF_ldv_current@ 2192)) (.cse11 (+ (+ __ADDRESS_OF_ldv_current@ 2376) (* 16 0))) (.cse12 (+ (+ __ADDRESS_OF_ldv_current@ 2728) 0)) (.cse13 (+ __ADDRESS_OF_ldv_current@ 6152)) (.cse14 (+ __ADDRESS_OF_ldv_current@ 6184)) (.cse16 (+ .cse15 80)) (.cse17 (+ __ADDRESS_OF_ldv_current@ 6392))) (and (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 16) 0)) 0) (= (|*struct_list_head:next@1| (+ .cse0 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse0 8)) 0) (= (|*struct_list_head:next@1| (+ .cse1 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse1 8)) 0) (= (|*struct_list_head:next@1| (+ .cse2 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse2 8)) 0) (= (|*struct_list_head:next@1| (+ .cse3 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse3 8)) 0) (= (|*struct_list_head:next@1| (+ .cse4 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse4 8)) 0) (= (|*struct_list_head:next@1| (+ .cse5 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse5 8)) 0) (= (|*struct_list_head:next@1| (+ .cse6 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse6 8)) 0) (= (|*struct_list_head:next@1| (+ .cse7 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse7 8)) 0) (= (|*struct_list_head:next@1| (+ .cse8 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse8 8)) 0) (= (|*struct_list_head:next@1| (+ .cse9 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse9 8)) 0) (= (|*struct_list_head:next@1| (+ .cse10 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse10 8)) 0) (= (|*struct_list_head:next@1| (+ .cse11 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse11 8)) 0) (= (|*struct_list_head:next@1| (+ .cse12 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse12 8)) 0) (= (|*struct_list_head:next@1| (+ .cse13 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse13 8)) 0) (= (|*struct_list_head:next@1| (+ .cse14 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse14 8)) 0) (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ .cse15 0) 0)) 0) (= (|*struct_list_head:next@1| (+ .cse16 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse16 8)) 0) (= (|*struct_list_head:next@1| (+ .cse17 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse17 8)) 0)))), (+ (+ __ADDRESS_OF_ldv_current@ 6152) 0), (+ |__ADDRESS_OF_ldv_init::var3@| 4), (+ (+ (+ __ADDRESS_OF_ldv_current@ 1840) 8) 0), (ite (not (= (|*int:global@3| |ldv_init::var2@2|) (|*int:global@3| |__ADDRESS_OF_ldv_init::var1@|))) 1 0), (+ (+ __ADDRESS_OF_ldv_current@ 1840) 8), (+ __ADDRESS_OF_ldv_current@ 2376), (|*struct_list_head:next@1| (+ (+ (+ __ADDRESS_OF_ldv_current@ 104) 40) 0)), (= (|*struct_list_head:next@1| (+ (+ __ADDRESS_OF_ldv_current@ 2176) 0)) 0), 2176, (let ((.cse15 (+ __ADDRESS_OF_ldv_current@ 6224)) (.cse20 (+ __ADDRESS_OF_ldv_current@ 1840))) (let ((.cse0 (+ (+ __ADDRESS_OF_ldv_current@ 104) 40)) (.cse1 (+ (+ __ADDRESS_OF_ldv_current@ 480) 0)) (.cse2 (+ __ADDRESS_OF_ldv_current@ 1824)) (.cse3 (+ .cse20 8)) (.cse4 (+ .cse20 24)) (.cse5 (+ __ADDRESS_OF_ldv_current@ 2032)) (.cse6 (+ __ADDRESS_OF_ldv_current@ 2048)) (.cse7 (+ __ADDRESS_OF_ldv_current@ 2072)) (.cse8 (+ __ADDRESS_OF_ldv_current@ 2088)) (.cse9 (+ __ADDRESS_OF_ldv_current@ 2176)) (.cse10 (+ __ADDRESS_OF_ldv_current@ 2192)) (.cse11 (+ (+ __ADDRESS_OF_ldv_current@ 2376) (* 16 0))) (.cse12 (+ (+ __ADDRESS_OF_ldv_current@ 2728) 0)) (.cse13 (+ __ADDRESS_OF_ldv_current@ 6152)) (.cse14 (+ __ADDRESS_OF_ldv_current@ 6184)) (.cse16 (+ .cse15 80)) (.cse17 (+ __ADDRESS_OF_ldv_current@ 6392)) (.cse18 (+ __ADDRESS_OF_ldv_current@ 6472))) (and (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 16) 0)) 0) (= (|*struct_list_head:next@1| (+ .cse0 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse0 8)) 0) (= (|*struct_list_head:next@1| (+ .cse1 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse1 8)) 0) (= (|*struct_list_head:next@1| (+ .cse2 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse2 8)) 0) (= (|*struct_list_head:next@1| (+ .cse3 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse3 8)) 0) (= (|*struct_list_head:next@1| (+ .cse4 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse4 8)) 0) (= (|*struct_list_head:next@1| (+ .cse5 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse5 8)) 0) (= (|*struct_list_head:next@1| (+ .cse6 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse6 8)) 0) (= (|*struct_list_head:next@1| (+ .cse7 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse7 8)) 0) (= (|*struct_list_head:next@1| (+ .cse8 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse8 8)) 0) (= (|*struct_list_head:next@1| (+ .cse9 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse9 8)) 0) (= (|*struct_list_head:next@1| (+ .cse10 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse10 8)) 0) (= (|*struct_list_head:next@1| (+ .cse11 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse11 8)) 0) (= (|*struct_list_head:next@1| (+ .cse12 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse12 8)) 0) (= (|*struct_list_head:next@1| (+ .cse13 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse13 8)) 0) (= (|*struct_list_head:next@1| (+ .cse14 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse14 8)) 0) (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ .cse15 0) 0)) 0) (= (|*struct_list_head:next@1| (+ .cse16 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse16 8)) 0) (= (|*struct_list_head:next@1| (+ .cse17 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse17 8)) 0) (= (|*struct_list_head:next@1| (+ .cse18 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse18 8)) 0) (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 10504) 0)) 0) (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 10508) 0)) 0) (> __ADDRESS_OF_ldv_current@ 0) (let ((.cse19 (- __ADDRESS_OF_ldv_current@ 0))) (= .cse19 (* 8 (div .cse19 8)))) (> (+ __ADDRESS_OF_ldv_current@ 10608) 0)))), (= PRED1 (= |ldv_init::var2| |__ADDRESS_OF_ldv_init::var1@|)), (|*struct_list_head:next@1| (+ (+ __ADDRESS_OF_ldv_current@ 6472) 0)), (let ((.cse0 (+ |__ADDRESS_OF_ldv_init::var1@| 0))) (= (|*int:global@2| .cse0) (|*int:global@1| .cse0))), (+ (+ __ADDRESS_OF_ldv_current@ 6184) 0), (+ __ADDRESS_OF_ldv_current@ 10608), (|*struct_list_head:prev@1| (+ (+ __ADDRESS_OF_ldv_current@ 6472) 8)), (= (|*struct_list_head:next@1| (+ (+ __ADDRESS_OF_ldv_current@ 1824) 0)) 0), (+ (+ __ADDRESS_OF_ldv_current@ 1824) 8), (+ (+ __ADDRESS_OF_ldv_current@ 1824) 0), (let ((.cse8 (+ __ADDRESS_OF_ldv_current@ 1840))) (let ((.cse0 (+ (+ __ADDRESS_OF_ldv_current@ 104) 40)) (.cse1 (+ (+ __ADDRESS_OF_ldv_current@ 480) 0)) (.cse2 (+ __ADDRESS_OF_ldv_current@ 1824)) (.cse3 (+ .cse8 8)) (.cse4 (+ .cse8 24)) (.cse5 (+ __ADDRESS_OF_ldv_current@ 2032)) (.cse6 (+ __ADDRESS_OF_ldv_current@ 2048)) (.cse7 (+ __ADDRESS_OF_ldv_current@ 2072))) (and (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 16) 0)) 0) (= (|*struct_list_head:next@1| (+ .cse0 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse0 8)) 0) (= (|*struct_list_head:next@1| (+ .cse1 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse1 8)) 0) (= (|*struct_list_head:next@1| (+ .cse2 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse2 8)) 0) (= (|*struct_list_head:next@1| (+ .cse3 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse3 8)) 0) (= (|*struct_list_head:next@1| (+ .cse4 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse4 8)) 0) (= (|*struct_list_head:next@1| (+ .cse5 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse5 8)) 0) (= (|*struct_list_head:next@1| (+ .cse6 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse6 8)) 0) (= (|*struct_list_head:next@1| (+ .cse7 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse7 8)) 0) (= (|*struct_list_head:next@1| (+ (+ __ADDRESS_OF_ldv_current@ 2088) 0)) 0)))), (let ((.cse6 (+ __ADDRESS_OF_ldv_current@ 1840))) (let ((.cse0 (+ (+ __ADDRESS_OF_ldv_current@ 104) 40)) (.cse1 (+ (+ __ADDRESS_OF_ldv_current@ 480) 0)) (.cse2 (+ __ADDRESS_OF_ldv_current@ 1824)) (.cse3 (+ .cse6 8)) (.cse4 (+ .cse6 24)) (.cse5 (+ __ADDRESS_OF_ldv_current@ 2032))) (and (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 16) 0)) 0) (= (|*struct_list_head:next@1| (+ .cse0 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse0 8)) 0) (= (|*struct_list_head:next@1| (+ .cse1 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse1 8)) 0) (= (|*struct_list_head:next@1| (+ .cse2 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse2 8)) 0) (= (|*struct_list_head:next@1| (+ .cse3 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse3 8)) 0) (= (|*struct_list_head:next@1| (+ .cse4 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse4 8)) 0) (= (|*struct_list_head:next@1| (+ .cse5 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse5 8)) 0) (= (|*struct_list_head:next@1| (+ (+ __ADDRESS_OF_ldv_current@ 2048) 0)) 0)))), |ldv_undef_int::undef_int@3|, (and (= |ldv_undef_int::undef_int@6| __VERIFIER_nondet_int!3@) (= |ldv_undef_int::__retval__@3| |ldv_undef_int::undef_int@6|)), (+ __ADDRESS_OF_ldv_current@ 6392), (= (|*struct_list_head:prev@1| (+ (+ __ADDRESS_OF_ldv_current@ 6392) 8)) 0), (= (|*struct_list_head:prev@1| (+ (+ (+ __ADDRESS_OF_ldv_current@ 1840) 8) 8)) 0), (let ((.cse9 (+ __ADDRESS_OF_ldv_current@ 1840))) (let ((.cse0 (+ (+ __ADDRESS_OF_ldv_current@ 104) 40)) (.cse1 (+ (+ __ADDRESS_OF_ldv_current@ 480) 0)) (.cse2 (+ __ADDRESS_OF_ldv_current@ 1824)) (.cse3 (+ .cse9 8)) (.cse4 (+ .cse9 24)) (.cse5 (+ __ADDRESS_OF_ldv_current@ 2032)) (.cse6 (+ __ADDRESS_OF_ldv_current@ 2048)) (.cse7 (+ __ADDRESS_OF_ldv_current@ 2072)) (.cse8 (+ __ADDRESS_OF_ldv_current@ 2088))) (and (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 16) 0)) 0) (= (|*struct_list_head:next@1| (+ .cse0 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse0 8)) 0) (= (|*struct_list_head:next@1| (+ .cse1 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse1 8)) 0) (= (|*struct_list_head:next@1| (+ .cse2 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse2 8)) 0) (= (|*struct_list_head:next@1| (+ .cse3 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse3 8)) 0) (= (|*struct_list_head:next@1| (+ .cse4 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse4 8)) 0) (= (|*struct_list_head:next@1| (+ .cse5 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse5 8)) 0) (= (|*struct_list_head:next@1| (+ .cse6 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse6 8)) 0) (= (|*struct_list_head:next@1| (+ .cse7 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse7 8)) 0) (= (|*struct_list_head:next@1| (+ .cse8 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse8 8)) 0) (= (|*struct_list_head:next@1| (+ (+ __ADDRESS_OF_ldv_current@ 2176) 0)) 0)))), (let ((.cse0 (- __ADDRESS_OF_ldv_current@ 0))) (= .cse0 (* 8 (div .cse0 8)))), (+ (+ (+ __ADDRESS_OF_ldv_current@ 6224) 80) 8), 24, (|*struct_list_head:next@1| (+ (+ __ADDRESS_OF_ldv_current@ 6152) 0)), (= (|*int:global@3| |__ADDRESS_OF_ldv_init::var3@|) |ldv_undef_int::__retval__@3|), (let ((.cse12 (+ __ADDRESS_OF_ldv_current@ 1840))) (let ((.cse0 (+ (+ __ADDRESS_OF_ldv_current@ 104) 40)) (.cse1 (+ (+ __ADDRESS_OF_ldv_current@ 480) 0)) (.cse2 (+ __ADDRESS_OF_ldv_current@ 1824)) (.cse3 (+ .cse12 8)) (.cse4 (+ .cse12 24)) (.cse5 (+ __ADDRESS_OF_ldv_current@ 2032)) (.cse6 (+ __ADDRESS_OF_ldv_current@ 2048)) (.cse7 (+ __ADDRESS_OF_ldv_current@ 2072)) (.cse8 (+ __ADDRESS_OF_ldv_current@ 2088)) (.cse9 (+ __ADDRESS_OF_ldv_current@ 2176)) (.cse10 (+ __ADDRESS_OF_ldv_current@ 2192)) (.cse11 (+ (+ __ADDRESS_OF_ldv_current@ 2376) (* 16 0)))) (and (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 16) 0)) 0) (= (|*struct_list_head:next@1| (+ .cse0 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse0 8)) 0) (= (|*struct_list_head:next@1| (+ .cse1 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse1 8)) 0) (= (|*struct_list_head:next@1| (+ .cse2 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse2 8)) 0) (= (|*struct_list_head:next@1| (+ .cse3 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse3 8)) 0) (= (|*struct_list_head:next@1| (+ .cse4 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse4 8)) 0) (= (|*struct_list_head:next@1| (+ .cse5 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse5 8)) 0) (= (|*struct_list_head:next@1| (+ .cse6 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse6 8)) 0) (= (|*struct_list_head:next@1| (+ .cse7 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse7 8)) 0) (= (|*struct_list_head:next@1| (+ .cse8 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse8 8)) 0) (= (|*struct_list_head:next@1| (+ .cse9 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse9 8)) 0) (= (|*struct_list_head:next@1| (+ .cse10 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse10 8)) 0) (= (|*struct_list_head:next@1| (+ .cse11 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse11 8)) 0)))), (= (|*struct_list_head:next@1| (+ (+ (+ __ADDRESS_OF_ldv_current@ 2376) (* 16 0)) 0)) 0), (+ (+ (+ __ADDRESS_OF_ldv_current@ 1840) 24) 8), (let ((.cse15 (+ __ADDRESS_OF_ldv_current@ 6224)) (.cse19 (+ __ADDRESS_OF_ldv_current@ 1840))) (let ((.cse0 (+ (+ __ADDRESS_OF_ldv_current@ 104) 40)) (.cse1 (+ (+ __ADDRESS_OF_ldv_current@ 480) 0)) (.cse2 (+ __ADDRESS_OF_ldv_current@ 1824)) (.cse3 (+ .cse19 8)) (.cse4 (+ .cse19 24)) (.cse5 (+ __ADDRESS_OF_ldv_current@ 2032)) (.cse6 (+ __ADDRESS_OF_ldv_current@ 2048)) (.cse7 (+ __ADDRESS_OF_ldv_current@ 2072)) (.cse8 (+ __ADDRESS_OF_ldv_current@ 2088)) (.cse9 (+ __ADDRESS_OF_ldv_current@ 2176)) (.cse10 (+ __ADDRESS_OF_ldv_current@ 2192)) (.cse11 (+ (+ __ADDRESS_OF_ldv_current@ 2376) (* 16 0))) (.cse12 (+ (+ __ADDRESS_OF_ldv_current@ 2728) 0)) (.cse13 (+ __ADDRESS_OF_ldv_current@ 6152)) (.cse14 (+ __ADDRESS_OF_ldv_current@ 6184)) (.cse16 (+ .cse15 80)) (.cse17 (+ __ADDRESS_OF_ldv_current@ 6392)) (.cse18 (+ __ADDRESS_OF_ldv_current@ 6472))) (and (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 16) 0)) 0) (= (|*struct_list_head:next@1| (+ .cse0 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse0 8)) 0) (= (|*struct_list_head:next@1| (+ .cse1 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse1 8)) 0) (= (|*struct_list_head:next@1| (+ .cse2 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse2 8)) 0) (= (|*struct_list_head:next@1| (+ .cse3 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse3 8)) 0) (= (|*struct_list_head:next@1| (+ .cse4 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse4 8)) 0) (= (|*struct_list_head:next@1| (+ .cse5 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse5 8)) 0) (= (|*struct_list_head:next@1| (+ .cse6 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse6 8)) 0) (= (|*struct_list_head:next@1| (+ .cse7 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse7 8)) 0) (= (|*struct_list_head:next@1| (+ .cse8 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse8 8)) 0) (= (|*struct_list_head:next@1| (+ .cse9 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse9 8)) 0) (= (|*struct_list_head:next@1| (+ .cse10 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse10 8)) 0) (= (|*struct_list_head:next@1| (+ .cse11 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse11 8)) 0) (= (|*struct_list_head:next@1| (+ .cse12 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse12 8)) 0) (= (|*struct_list_head:next@1| (+ .cse13 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse13 8)) 0) (= (|*struct_list_head:next@1| (+ .cse14 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse14 8)) 0) (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ .cse15 0) 0)) 0) (= (|*struct_list_head:next@1| (+ .cse16 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse16 8)) 0) (= (|*struct_list_head:next@1| (+ .cse17 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse17 8)) 0) (= (|*struct_list_head:next@1| (+ .cse18 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse18 8)) 0) (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 10504) 0)) 0) (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 10508) 0)) 0)))), (= (|*struct_list_head:prev@1| (+ (+ (+ __ADDRESS_OF_ldv_current@ 480) 0) 8)) 0), 2192, (and (= |ldv_init::var4@2| |__ADDRESS_OF_ldv_init::var3@|) (= (|*int:global@2| |ldv_init::var2@1|) (|*int:global@2| |__ADDRESS_OF_ldv_init::var1@|))), (= (|*struct_list_head:prev@1| (+ (+ (+ __ADDRESS_OF_ldv_current@ 6224) 80) 8)) 0), 2088, (|*int:global@2| |__ADDRESS_OF_ldv_init::var1@|), (+ (+ __ADDRESS_OF_ldv_current@ 2192) 0), (and (= |ldv_init::var2@2| |__ADDRESS_OF_ldv_init::var1@|) (> |__ADDRESS_OF_ldv_init::var3@| (+ |__ADDRESS_OF_ldv_init::var1@| 4)) (let ((.cse0 (- |__ADDRESS_OF_ldv_init::var3@| 0))) (= .cse0 (* 4 (div .cse0 4)))) (> (+ |__ADDRESS_OF_ldv_init::var3@| 4) 0)), (and (= |ldv_init::var4@2| |__ADDRESS_OF_ldv_init::var3@|) (not (= (|*int:global@2| |ldv_init::var2@1|) (|*int:global@2| |__ADDRESS_OF_ldv_init::var1@|)))), (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 10504) 0)), __NaN__, (= ldv_is_memory_alloc_failures@3 1), (+ (+ __ADDRESS_OF_ldv_current@ 16) 0), (+ (+ __ADDRESS_OF_ldv_current@ 2728) 0), 0.0, 40, (+ (+ (+ __ADDRESS_OF_ldv_current@ 1840) 8) 8), (let ((.cse0 (+ (+ __ADDRESS_OF_ldv_current@ 104) 40)) (.cse1 (+ (+ __ADDRESS_OF_ldv_current@ 480) 0)) (.cse2 (+ __ADDRESS_OF_ldv_current@ 1824)) (.cse3 (+ (+ __ADDRESS_OF_ldv_current@ 1840) 8))) (and (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 16) 0)) 0) (= (|*struct_list_head:next@1| (+ .cse0 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse0 8)) 0) (= (|*struct_list_head:next@1| (+ .cse1 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse1 8)) 0) (= (|*struct_list_head:next@1| (+ .cse2 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse2 8)) 0) (= (|*struct_list_head:next@1| (+ .cse3 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse3 8)) 0))), (let ((.cse15 (+ __ADDRESS_OF_ldv_current@ 6224)) (.cse18 (+ __ADDRESS_OF_ldv_current@ 1840))) (let ((.cse0 (+ (+ __ADDRESS_OF_ldv_current@ 104) 40)) (.cse1 (+ (+ __ADDRESS_OF_ldv_current@ 480) 0)) (.cse2 (+ __ADDRESS_OF_ldv_current@ 1824)) (.cse3 (+ .cse18 8)) (.cse4 (+ .cse18 24)) (.cse5 (+ __ADDRESS_OF_ldv_current@ 2032)) (.cse6 (+ __ADDRESS_OF_ldv_current@ 2048)) (.cse7 (+ __ADDRESS_OF_ldv_current@ 2072)) (.cse8 (+ __ADDRESS_OF_ldv_current@ 2088)) (.cse9 (+ __ADDRESS_OF_ldv_current@ 2176)) (.cse10 (+ __ADDRESS_OF_ldv_current@ 2192)) (.cse11 (+ (+ __ADDRESS_OF_ldv_current@ 2376) (* 16 0))) (.cse12 (+ (+ __ADDRESS_OF_ldv_current@ 2728) 0)) (.cse13 (+ __ADDRESS_OF_ldv_current@ 6152)) (.cse14 (+ __ADDRESS_OF_ldv_current@ 6184)) (.cse16 (+ .cse15 80)) (.cse17 (+ __ADDRESS_OF_ldv_current@ 6392))) (and (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 16) 0)) 0) (= (|*struct_list_head:next@1| (+ .cse0 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse0 8)) 0) (= (|*struct_list_head:next@1| (+ .cse1 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse1 8)) 0) (= (|*struct_list_head:next@1| (+ .cse2 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse2 8)) 0) (= (|*struct_list_head:next@1| (+ .cse3 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse3 8)) 0) (= (|*struct_list_head:next@1| (+ .cse4 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse4 8)) 0) (= (|*struct_list_head:next@1| (+ .cse5 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse5 8)) 0) (= (|*struct_list_head:next@1| (+ .cse6 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse6 8)) 0) (= (|*struct_list_head:next@1| (+ .cse7 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse7 8)) 0) (= (|*struct_list_head:next@1| (+ .cse8 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse8 8)) 0) (= (|*struct_list_head:next@1| (+ .cse9 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse9 8)) 0) (= (|*struct_list_head:next@1| (+ .cse10 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse10 8)) 0) (= (|*struct_list_head:next@1| (+ .cse11 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse11 8)) 0) (= (|*struct_list_head:next@1| (+ .cse12 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse12 8)) 0) (= (|*struct_list_head:next@1| (+ .cse13 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse13 8)) 0) (= (|*struct_list_head:next@1| (+ .cse14 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse14 8)) 0) (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ .cse15 0) 0)) 0) (= (|*struct_list_head:next@1| (+ .cse16 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse16 8)) 0) (= (|*struct_list_head:next@1| (+ .cse17 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse17 8)) 0) (= (|*struct_list_head:next@1| (+ (+ __ADDRESS_OF_ldv_current@ 6472) 0)) 0)))), 4, (+ (+ __ADDRESS_OF_ldv_current@ 2088) 8), PRED0, (let ((.cse0 (+ (+ __ADDRESS_OF_ldv_current@ 104) 40)) (.cse1 (+ (+ __ADDRESS_OF_ldv_current@ 480) 0)) (.cse2 (+ __ADDRESS_OF_ldv_current@ 1824))) (and (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 16) 0)) 0) (= (|*struct_list_head:next@1| (+ .cse0 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse0 8)) 0) (= (|*struct_list_head:next@1| (+ .cse1 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse1 8)) 0) (= (|*struct_list_head:next@1| (+ .cse2 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse2 8)) 0))), 6472, 6152, (and (= |ldv_undef_int::undef_int@3| __VERIFIER_nondet_int!2@) (= |ldv_undef_int::__retval__@2| |ldv_undef_int::undef_int@3|)), (+ __ADDRESS_OF_ldv_current@ 6472), (+ (+ (+ __ADDRESS_OF_ldv_current@ 480) 0) 0), (div (- __ADDRESS_OF_ldv_current@ 0) 8), |ldv_init::var2@2|, (not (= (|*int:global@2| |ldv_init::var2@1|) (|*int:global@2| |__ADDRESS_OF_ldv_init::var1@|))), (= (|*struct_list_head:prev@1| (+ (+ __ADDRESS_OF_ldv_current@ 2048) 8)) 0), (= |ldv_init::var2@2| |__ADDRESS_OF_ldv_init::var1@|), (|*struct_list_head:next@1| (+ (+ (+ __ADDRESS_OF_ldv_current@ 480) 0) 0)), (|*struct_list_head:next@1| (+ (+ __ADDRESS_OF_ldv_current@ 6184) 0)), (|*int:global@3| |ldv_init::var2@2|), (|*struct_list_head:next@1| (+ (+ (+ __ADDRESS_OF_ldv_current@ 6224) 80) 0)), (and (> __ADDRESS_OF_ldv_current@ 0) (let ((.cse0 (- __ADDRESS_OF_ldv_current@ 0))) (= .cse0 (* 8 (div .cse0 8)))) (> (+ __ADDRESS_OF_ldv_current@ 10608) 0)), (+ __ADDRESS_OF_ldv_current@ 480), (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 10508) 0)) 0), (= (|*int:global@2| |__ADDRESS_OF_ldv_init::var3@|) |ldv_undef_int::__retval__@2|), (let ((.cse0 (+ |__ADDRESS_OF_ldv_init::var1@| 0))) (= (|*int:global@3| .cse0) (|*int:global@2| .cse0))), (= (|*struct_list_head:prev@1| (+ (+ __ADDRESS_OF_ldv_current@ 2176) 8)) 0), (= (|*struct_list_head:next@1| (+ (+ __ADDRESS_OF_ldv_current@ 2088) 0)) 0), (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ (+ __ADDRESS_OF_ldv_current@ 6224) 0) 0)) 0), |ldv_init::var2@1|, (let ((.cse11 (+ __ADDRESS_OF_ldv_current@ 1840))) (let ((.cse0 (+ (+ __ADDRESS_OF_ldv_current@ 104) 40)) (.cse1 (+ (+ __ADDRESS_OF_ldv_current@ 480) 0)) (.cse2 (+ __ADDRESS_OF_ldv_current@ 1824)) (.cse3 (+ .cse11 8)) (.cse4 (+ .cse11 24)) (.cse5 (+ __ADDRESS_OF_ldv_current@ 2032)) (.cse6 (+ __ADDRESS_OF_ldv_current@ 2048)) (.cse7 (+ __ADDRESS_OF_ldv_current@ 2072)) (.cse8 (+ __ADDRESS_OF_ldv_current@ 2088)) (.cse9 (+ __ADDRESS_OF_ldv_current@ 2176)) (.cse10 (+ __ADDRESS_OF_ldv_current@ 2192))) (and (= (|*struct___anonstruct_atomic_t_145:counter@1| (+ (+ __ADDRESS_OF_ldv_current@ 16) 0)) 0) (= (|*struct_list_head:next@1| (+ .cse0 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse0 8)) 0) (= (|*struct_list_head:next@1| (+ .cse1 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse1 8)) 0) (= (|*struct_list_head:next@1| (+ .cse2 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse2 8)) 0) (= (|*struct_list_head:next@1| (+ .cse3 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse3 8)) 0) (= (|*struct_list_head:next@1| (+ .cse4 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse4 8)) 0) (= (|*struct_list_head:next@1| (+ .cse5 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse5 8)) 0) (= (|*struct_list_head:next@1| (+ .cse6 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse6 8)) 0) (= (|*struct_list_head:next@1| (+ .cse7 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse7 8)) 0) (= (|*struct_list_head:next@1| (+ .cse8 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse8 8)) 0) (= (|*struct_list_head:next@1| (+ .cse9 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse9 8)) 0) (= (|*struct_list_head:next@1| (+ .cse10 0)) 0) (= (|*struct_list_head:prev@1| (+ .cse10 8)) 0)))), (* 4 (div (- |__ADDRESS_OF_ldv_init::var1@| 0) 4)), (+ (+ __ADDRESS_OF_ldv_current@ 2032) 8), 0]

[PhilippWendler]

So the problem is in line 220 in the SmtInterpolAbstractProver. I can not tell what the underlying problem is at this moment however. Removing this line avoids the error and the analysis returns True.

But that leaks all the memory, wouldn't it? So it only confirms the problem but is not a fix.

I could not yet determine a way of testing this. @daniel-raffler do you want to try and find a test and possibly a program to send to the SMTInterpol devs if we are not causing this?

If your assumption below about empty pushes is correct, this should be easy to replicate, shouldn't it?

@PhilippWendler do we need a hotfix version for this?

Well, depends. It would certainly be nice if SMTInterpol would be usable in CPAchecker without having to wait for several months or so.

[baierd]

So the problem is in line 220 in the SmtInterpolAbstractProver. I can not tell what the underlying problem is at this moment however. Removing this line avoids the error and the analysis returns True.

But that leaks all the memory, wouldn't it? So it only confirms the problem but is not a fix.

Yes. But there is API in SMTInterpol for that with exit() to close a solver completely or reset() and resetAssertions() to reset it and clean up the references. But i need to take a look at how we implemented the prover for SMTInterpol. This might actually be a proper solution compared to what we do currently.

I could not yet determine a way of testing this. @daniel-raffler do you want to try and find a test and possibly a program to send to the SMTInterpol devs if we are not causing this?

If your assumption below about empty pushes is correct, this should be easy to replicate, shouldn't it?

I of course tried this, but it is not that trivial ;D

@PhilippWendler do we need a hotfix version for this?

Well, depends. It would certainly be nice if SMTInterpol would be usable in CPAchecker without having to wait for several months or so.

I guess we can do a release once we sorted this and #406 out.

[daniel-raffler]

@daniel-raffler do you want to try and find a test and possibly a program to send to the SMTInterpol devs if we are not causing this?

I've had a look at it and it seems that the issue has been around for some time. It was introduced in 999c8d59cc54feb64117db3a62c8f37201c0bf6c, which moved a lot of the bookkeeping for the assertion stack from the solver backends to their base class AbstractProver. The commit also changed close() in SMTInterpolAbstractProver from its old version:

public void close() {
  if (!closed) {
    assertedFormulas.clear();
    annotatedTerms.clear();
    env.pop(assertedFormulas.size());
  }
  super.close();
}

to

@Override
public void close() {
  if (!closed) {
    annotatedTerms.clear();
    env.pop(size());
  }
  super.close();
}

Note that the old version is actually broken as env.pop(assertedFormulas.size()); is called after assertedFormulas was just cleared. Because of this pop would only ever get called with 0 as its argument. If we change the order and call pop first the crash can be replicated even with the old version.

I think it should be safe to simply remove the line for now as this will just gets us back to the behavior of JavaSMT 4.0.2 before the version was updated in CPAchecker. There might still be a SMTInterpol bug here, but this will need some more work: The line env.pop(assertedFormulas.size()); was last changed in cd14da11f383d300c7d2767ddd5c4e1263e1fcf0 which is about adding support for multiple prover stacks to SMTInterpol. Before that only one prover would be allowed at a time and the assertion stack would have to be cleared before another prover is opened (internally the stack would simply be reused). It's possible that there are still some problems when formulas are shared across prover stacks, and those provers are then closed in the "wrong" order. I'll see if I can find a test case for that.

[baierd]

I fixed it using the proper cleanup API of SMTInterpol in 72b06914cf9bd126930d32d37161a8895683abba.

I also tested this with CPAchecker and it works fine now.

@daniel-raffler if you want to find a minimal example to use as a test you can try. But don't spend to much time on it as it should be fixed for good now.