MathSAT5 Returns Null for msat_model_create_iterator()

[baierd]

I found a problem when asking for a model iterator in Mathsat5 using CPAchecker.
It takes about 600s to get to the error and this was executed using this branch and commit 7273036c8b6c3540acd15f45681b26cbd429038f.

Possibly related to #208 ?

bin/cpachecker --heap 10000M --benchmark --timelimit '900 s' --symbolicExecution-Cegar --option analysis.traversal.order=dfs --stats --spec test/sv-benchmarks/c/properties/unreach-call.prp --32 test/sv-benchmarks/c/hardness-nfm22/hardness_variablewrapping_wrapper-ap_file-14.i


--------------------------------------------------------------------------------


Running CPAchecker with Java heap of size 10000M.
Running CPAchecker with default stack size (1024k). Specify a larger value with --stack if needed.
Language C detected and set for analysis (CPAMain.detectFrontendLanguageIfNecessary, INFO)

Using the following resource limits: CPU-time limit of 900s (ResourceLimitChecker.fromConfiguration, INFO)

CPAchecker 4.0-668-g7273036c8b / symbolicExecution-Cegar (OpenJDK 64-Bit Server VM 21.0.6) started (CPAchecker.run, INFO)

Parsing CFA from file(s) "test/sv-benchmarks/c/hardness-nfm22/hardness_variablewrapping_wrapper-ap_file-14.i" (CPAchecker.parse, INFO)

line 136: Dead code detected: return 0; (CFACreationUtils.addEdgeToCFA, INFO)

Starting analysis ... (CPAchecker.runAlgorithm, INFO)

// ... removed some useless info ...

Error path found, starting counterexample check with CPACHECKER. (CounterexampleCheckAlgorithm.checkCounterexample, INFO)

Using predicate analysis with MathSAT5 version 5.6.10 (9293adc746be) (May 31 2023 12:38:06, gmp 6.2.0, gcc 7.5.0, 64-bit, reentrant). (CounterexampleCheck:PredicateCPA:PredicateCPA.<init>, INFO)

Error path found but identified as infeasible. (CounterexampleCheckAlgorithm.checkCounterexample, INFO)

Another infeasible counterexample found which could not be removed from the ARG. (ExceptionHandlingAlgorithm.handleExceptionWithErrorPath, INFO)

(not (bvslt ((_ sign_extend 16) (select *short_int@1 |signed_short_int_Array_0_arraysigned_short_int_Array_0Var3_Pointer#13@1|)) ((_ zero_extend 16) (select *short_int@1 |unsigned_short_int_Array_0_arrayunsigned_short_int_Array_0Var0_Pointer#14@1|))))
(bvslt |step::__CPAchecker_TMP_2#661@1| ((_ sign_extend 16) (select *short_int@1 |signed_short_int_Array_0_arraysigned_short_int_Array_0Var1_Pointer#11@1|)))
(= |signed_short_int_Array_0_arraysigned_short_int_Array_0Var1_Pointer#11@1| #b00000000000000000000000000000000)
(= #b00000000000000000000000000000010 ((_ zero_extend 16) (select *short_int@1 |unsigned_short_int_Array_0_arrayunsigned_short_int_Array_0Var0_Pointer#14@1|)))
(= |step::__CPAchecker_TMP_2#661@1| #b00000000000000000000000000000010)
(= (select *short_int@1 #b00000000000000000000000000000000) #b0000000000000010)
(= (select *short_int@1 |signed_short_int_Array_0_arraysigned_short_int_Array_0Var3_Pointer#13@1|) #b0000000000000010)
(= #b00000000000000000000000000000010 ((_ sign_extend 16) (select *short_int@1 #b00000000000000000000000000000000)))
Exception in thread "main" java.lang.IllegalArgumentException: MathSAT returned null
	at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_model_create_iterator(Native Method)
	at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5Model.asList(Mathsat5Model.java:56)
	at org.sosy_lab.java_smt.basicimpl.CachingModel.asList(CachingModel.java:40)
	at org.sosy_lab.java_smt.api.BasicProverEnvironment.getModelAssignments(BasicProverEnvironment.java:112)
	at org.sosy_lab.cpachecker.util.predicates.smt.BasicProverEnvironmentView.getModelAssignments(BasicProverEnvironmentView.java:71)
	at org.sosy_lab.cpachecker.cpa.constraints.domain.ConstraintsSolver.checkUnsat(ConstraintsSolver.java:267)
	at org.sosy_lab.cpachecker.cpa.constraints.ConstraintsTransferRelation.getIfSatisfiable(ConstraintsTransferRelation.java:335)
	at org.sosy_lab.cpachecker.cpa.constraints.ConstraintsTransferRelation$ValueAnalysisStrengthenOperator.strengthen(ConstraintsTransferRelation.java:386)
	at org.sosy_lab.cpachecker.cpa.constraints.ConstraintsTransferRelation.strengthen(ConstraintsTransferRelation.java:303)
	at org.sosy_lab.cpachecker.cpa.value.symbolic.refiner.ValueTransferBasedStrongestPostOperator.strengthenConstraintsState(ValueTransferBasedStrongestPostOperator.java:204)
	at org.sosy_lab.cpachecker.cpa.value.symbolic.refiner.ValueTransferBasedStrongestPostOperator.getStrongestPost(ValueTransferBasedStrongestPostOperator.java:111)
	at org.sosy_lab.cpachecker.cpa.value.symbolic.refiner.ValueTransferBasedStrongestPostOperator.getStrongestPost(ValueTransferBasedStrongestPostOperator.java:43)
	at org.sosy_lab.cpachecker.util.refinement.StrongestPostOperator.step(StrongestPostOperator.java:88)
	at org.sosy_lab.cpachecker.util.refinement.GenericFeasibilityChecker.isFeasible(GenericFeasibilityChecker.java:94)
	at org.sosy_lab.cpachecker.util.refinement.GenericFeasibilityChecker.isFeasible(GenericFeasibilityChecker.java:80)
	at org.sosy_lab.cpachecker.util.refinement.GenericFeasibilityChecker.isFeasible(GenericFeasibilityChecker.java:32)
	at org.sosy_lab.cpachecker.cpa.value.symbolic.refiner.ElementTestingSymbolicEdgeInterpolator.isPathFeasible(ElementTestingSymbolicEdgeInterpolator.java:182)
	at org.sosy_lab.cpachecker.cpa.value.symbolic.refiner.ElementTestingSymbolicEdgeInterpolator$ValuesOnlyReducer.reduce(ElementTestingSymbolicEdgeInterpolator.java:210)
	at org.sosy_lab.cpachecker.cpa.value.symbolic.refiner.ElementTestingSymbolicEdgeInterpolator$ConstraintsFirstReducer.reduce(ElementTestingSymbolicEdgeInterpolator.java:262)
	at org.sosy_lab.cpachecker.cpa.value.symbolic.refiner.ElementTestingSymbolicEdgeInterpolator$AvoidConstraintsReducer.reduce(ElementTestingSymbolicEdgeInterpolator.java:288)
	at org.sosy_lab.cpachecker.cpa.value.symbolic.refiner.ElementTestingSymbolicEdgeInterpolator.deriveInterpolant(ElementTestingSymbolicEdgeInterpolator.java:167)
	at org.sosy_lab.cpachecker.cpa.value.symbolic.refiner.ElementTestingSymbolicEdgeInterpolator.deriveInterpolant(ElementTestingSymbolicEdgeInterpolator.java:46)
	at org.sosy_lab.cpachecker.util.refinement.GenericPathInterpolator.performEdgeBasedInterpolation(GenericPathInterpolator.java:209)
	at org.sosy_lab.cpachecker.util.refinement.GenericPathInterpolator.performInterpolation(GenericPathInterpolator.java:133)
	at org.sosy_lab.cpachecker.util.refinement.GenericRefiner.performPathInterpolation(GenericRefiner.java:260)
	at org.sosy_lab.cpachecker.util.refinement.GenericRefiner.obtainInterpolants(GenericRefiner.java:222)
	at org.sosy_lab.cpachecker.util.refinement.GenericRefiner.performRefinementForPath(GenericRefiner.java:203)
	at org.sosy_lab.cpachecker.cpa.value.symbolic.refiner.SymbolicValueAnalysisRefiner.performRefinementForPath(SymbolicValueAnalysisRefiner.java:250)
	at org.sosy_lab.cpachecker.cpa.arg.AbstractARGBasedRefiner.performRefinementForPath(AbstractARGBasedRefiner.java:158)
	at org.sosy_lab.cpachecker.cpa.arg.AbstractARGBasedRefiner.performRefinement(AbstractARGBasedRefiner.java:104)
	at org.sosy_lab.cpachecker.core.algorithm.CEGARAlgorithm.refine(CEGARAlgorithm.java:307)
	at org.sosy_lab.cpachecker.core.algorithm.CEGARAlgorithm.run(CEGARAlgorithm.java:253)
	at org.sosy_lab.cpachecker.core.algorithm.counterexamplecheck.CounterexampleCheckAlgorithm.run(CounterexampleCheckAlgorithm.java:144)
	at org.sosy_lab.cpachecker.core.algorithm.ExceptionHandlingAlgorithm.run(ExceptionHandlingAlgorithm.java:147)
	at org.sosy_lab.cpachecker.core.algorithm.CounterexampleStoreAlgorithm.run(CounterexampleStoreAlgorithm.java:58)
	at org.sosy_lab.cpachecker.core.CPAchecker.runAlgorithm(CPAchecker.java:534)
	at org.sosy_lab.cpachecker.core.CPAchecker.run0(CPAchecker.java:393)
	at org.sosy_lab.cpachecker.core.CPAchecker.run(CPAchecker.java:302)
	at org.sosy_lab.cpachecker.cmdline.CPAMain.main(CPAMain.java:170)

[baierd]

Note: this is hard to pin down currently. Also, these model_iterator problems occur regularly (but not at an alarming rate).

Would it be helpful to actually catch this exception and throw a checked exception, i.e. SolverException or ModelException instead @kfriedberger ? (Provided that the prover/context is still usable)

[kfriedberger]

We discussed that topic with the MathSAT developers years ago and I thought that they fixed the issue. It was some bug in evaluating UFs and arrays in the model. It was quite hard to find the matching API calls to trigger the problem.

Returning NULL does not invalidate the solver context, so we could wrap the NullPointer in a SolverException, or even ignore it, aka return a partial model and continue.

[daniel-raffler]

Here is a run to trigger to trigger the bug more quickly (< 20s):

bin/cpachecker --svcomp25 --option solver.solver=mathsat5 --spec test/programs/benchmarks/properties/unreach-call.prp test/programs/benchmarks/hardness-nfm22/hardness_variablewrapping_wrapper-p_file-33.i
...
Exception in thread "main" java.lang.IllegalArgumentException: MathSAT returned null
	at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_model_eval(Native Method)
	at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5Model.evalImpl(Mathsat5Model.java:140)
	at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5Model.evalImpl(Mathsat5Model.java:35)
	at org.sosy_lab.java_smt.basicimpl.AbstractEvaluator.evaluateImpl(AbstractEvaluator.java:127)
	at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5Model.getArrayAssignments(Mathsat5Model.java:110)
	at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5Model.asList(Mathsat5Model.java:65)
	at org.sosy_lab.java_smt.basicimpl.CachingModel.asList(CachingModel.java:40)
	at org.sosy_lab.java_smt.api.BasicProverEnvironment.getModelAssignments(BasicProverEnvironment.java:112)
	at org.sosy_lab.cpachecker.util.predicates.smt.BasicProverEnvironmentView.getModelAssignments(BasicProverEnvironmentView.java:71)
	at org.sosy_lab.cpachecker.core.algorithm.bmc.ProverEnvironmentWithFallback.getModelAssignments(ProverEnvironmentWithFallback.java:215)
	at org.sosy_lab.cpachecker.core.algorithm.bmc.KInductionProver.check(KInductionProver.java:487)
	at org.sosy_lab.cpachecker.core.algorithm.bmc.AbstractBMCAlgorithm.checkStepCase(AbstractBMCAlgorithm.java:591)
	at org.sosy_lab.cpachecker.core.algorithm.bmc.AbstractBMCAlgorithm.run(AbstractBMCAlgorithm.java:524)
	at org.sosy_lab.cpachecker.core.algorithm.bmc.BMCAlgorithm.run(BMCAlgorithm.java:130)
	at org.sosy_lab.cpachecker.core.algorithm.ParallelAlgorithm.runParallelAnalysis(ParallelAlgorithm.java:385)
	at org.sosy_lab.cpachecker.core.algorithm.ParallelAlgorithm.lambda$createParallelAnalysis$4(ParallelAlgorithm.java:312)
	at com.google.common.util.concurrent.TrustedListenableFutureTask$TrustedFutureInterruptibleTask.runInterruptibly(TrustedListenableFutureTask.java:128)
	at com.google.common.util.concurrent.InterruptibleTask.run(InterruptibleTask.java:74)
	at com.google.common.util.concurrent.TrustedListenableFutureTask.run(TrustedListenableFutureTask.java:80)
	at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1144)
	at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:642)
	at java.base/java.lang.Thread.run(Thread.java:1583)

There may also be a related issue where MathSAT does return a valid iterator, but then can't get some elements from it:

bin/cpachecker --svcomp25 --option solver.solver=mathsat5 --spec test/programs/benchmarks/properties/unreach-call.prp test/programs/benchmarks/hardness-nfm22/hardness_variablewrapping_wrapper-sp_file-7.i
...
Exception in thread "main" java.util.NoSuchElementException
	at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5Model.asList(Mathsat5Model.java:61)
	at org.sosy_lab.java_smt.basicimpl.CachingModel.asList(CachingModel.java:40)
	at org.sosy_lab.java_smt.api.BasicProverEnvironment.getModelAssignments(BasicProverEnvironment.java:112)
	at org.sosy_lab.cpachecker.util.predicates.smt.BasicProverEnvironmentView.getModelAssignments(BasicProverEnvironmentView.java:71)
	at org.sosy_lab.cpachecker.core.algorithm.bmc.ProverEnvironmentWithFallback.getModelAssignments(ProverEnvironmentWithFallback.java:215)
	at org.sosy_lab.cpachecker.core.algorithm.bmc.KInductionProver.check(KInductionProver.java:487)
	at org.sosy_lab.cpachecker.core.algorithm.bmc.AbstractBMCAlgorithm.checkStepCase(AbstractBMCAlgorithm.java:591)
	at org.sosy_lab.cpachecker.core.algorithm.bmc.AbstractBMCAlgorithm.run(AbstractBMCAlgorithm.java:524)
	at org.sosy_lab.cpachecker.core.algorithm.bmc.BMCAlgorithm.run(BMCAlgorithm.java:130)
	at org.sosy_lab.cpachecker.core.algorithm.ParallelAlgorithm.runParallelAnalysis(ParallelAlgorithm.java:385)
	at org.sosy_lab.cpachecker.core.algorithm.ParallelAlgorithm.lambda$createParallelAnalysis$4(ParallelAlgorithm.java:312)
	at com.google.common.util.concurrent.TrustedListenableFutureTask$TrustedFutureInterruptibleTask.runInterruptibly(TrustedListenableFutureTask.java:128)
	at com.google.common.util.concurrent.InterruptibleTask.run(InterruptibleTask.java:74)
	at com.google.common.util.concurrent.TrustedListenableFutureTask.run(TrustedListenableFutureTask.java:80)
	at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1144)
	at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:642)
	at java.base/java.lang.Thread.run(Thread.java:1583)

When running the svcomp25 set (just SV-COMP25_unreach-call, and with a 60s time limit) I get 10 of these crashes:

The runs were done with the java-smt-update branch of CPAchecker, but I think the outcome should be the same with master. CVC5 has no issues with the same runs, but it still crashes if MathSAT is used as the main solver and CVC5 only for interpolation. The crashes I've seen are limited to hardness-nfm22 and the formulas always seem to use arrays, and often floating-point values (but not for the initial example). Maybe that's a good place to get started?

[baierd]

Thank you both for your input!

I guess it's best to wrap the error in an SolverException and possibly add our information about the problem to the description. I will implement it this week.

Additionally, we should try to find a easy to run/trigger case that we can send to the developers. @daniel-raffler would you be so kind and try to find a minimal example in SMT2? (Let me know if you need help!)

[daniel-raffler]

I found another instance of this bug:

bin/cpachecker --lassoRankerAnalysis --spec test/programs/benchmarks/properties/termination.prp test/programs/benchmarks/termination-crafted/NonTermination3-1.c
Running CPAchecker with default heap size (1200M). Specify a larger value with --heap if you have more RAM.
Running CPAchecker with default stack size (1024k). Specify a larger value with --stack if needed.
Language C detected and set for analysis (CPAMain.detectFrontendLanguageIfNecessary, INFO)

CPAchecker 4.0-1863-g3f8349df22+ (OpenJDK 64-Bit Server VM 21.0.8) started (CPAchecker.run, INFO)

Parsing CFA from file(s) "test/programs/benchmarks/termination-crafted/NonTermination3-1.c" (CPAchecker.parse, INFO)

Using predicate analysis with MathSAT5 version 5.6.11 (1a1154baf0ab) (Aug  9 2024 08:45:22, gmp 6.2.0, gcc 7.5.0, 64-bit, reentrant) and JFactory 1.21. (PredicateCPA:PredicateCPA.<init>, INFO)

Using refinement for predicate analysis with PredicateAbstractionRefinementStrategy strategy. (PredicateCPA:PredicateCPARefiner.<init>, INFO)

Using unsound approximation of ints with unbounded integers and floats with rationals for encoding program semantics. (FormulaManagerView.<init>, WARNING)

The following configuration options were specified but are not used:
 counterexample.checker.config
 counterexample.checker 
 (CPAchecker.printConfigurationWarnings, WARNING)

Starting analysis ... (CPAchecker.runAlgorithm, INFO)

Starting termination algorithm. (TerminationAlgorithm.run0, INFO)

Warning: Could not extract lasso (Loop with heads [N7]
  incoming: [lines 13-15:	N6 -{int n = 0;}-> N7]
  outgoing: [line 13:	N7 -{[!(n < 10)]}-> N10]
  nodes:    [N7, N8, N9, N11]
). (Unknown sort in equality) (InequalityConverter.convert, WARNING)

Could not synthesize a termination or non-termination argument. (TerminationAlgorithm.proveLoopTermination, WARNING)

(not (<= |__ADDRESS_OF_main::a@| 0))
(= |__ADDRESS_OF_main::a@| 0)
Exception in thread "main" java.lang.IllegalArgumentException: MathSAT returned null
	at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_model_create_iterator(Native Method)
	at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5Model.asList(Mathsat5Model.java:56)
	at org.sosy_lab.java_smt.basicimpl.CachingModel.asList(CachingModel.java:40)
	at org.sosy_lab.java_smt.api.BasicProverEnvironment.getModelAssignments(BasicProverEnvironment.java:112)
	at org.sosy_lab.cpachecker.util.predicates.smt.BasicProverEnvironmentView.getModelAssignments(BasicProverEnvironmentView.java:71)
	at org.sosy_lab.cpachecker.util.predicates.PathChecker.getModel(PathChecker.java:369)
	at org.sosy_lab.cpachecker.util.predicates.PathChecker.createCounterexample(PathChecker.java:228)
	at org.sosy_lab.cpachecker.util.predicates.PathChecker.handleFeasibleCounterexample(PathChecker.java:179)
	at org.sosy_lab.cpachecker.cpa.predicate.PredicateCPARefiner.performRefinementForPath(PredicateCPARefiner.java:314)
	at org.sosy_lab.cpachecker.cpa.predicate.PredicateStaticRefiner.performRefinementForPath(PredicateStaticRefiner.java:183)
	at org.sosy_lab.cpachecker.cpa.arg.AbstractARGBasedRefiner.performRefinementForPath(AbstractARGBasedRefiner.java:158)
	at org.sosy_lab.cpachecker.cpa.arg.AbstractARGBasedRefiner.performRefinement(AbstractARGBasedRefiner.java:104)
	at org.sosy_lab.cpachecker.core.algorithm.CEGARAlgorithm.refine(CEGARAlgorithm.java:307)
	at org.sosy_lab.cpachecker.core.algorithm.CEGARAlgorithm.run(CEGARAlgorithm.java:253)
	at org.sosy_lab.cpachecker.core.algorithm.termination.TerminationAlgorithm.proveLoopTermination(TerminationAlgorithm.java:306)
	at org.sosy_lab.cpachecker.core.algorithm.termination.TerminationAlgorithm.run0(TerminationAlgorithm.java:259)
	at org.sosy_lab.cpachecker.core.algorithm.termination.TerminationAlgorithm.run(TerminationAlgorithm.java:223)
	at org.sosy_lab.cpachecker.core.CPAchecker.runAlgorithm(CPAchecker.java:533)
	at org.sosy_lab.cpachecker.core.CPAchecker.run0(CPAchecker.java:392)
	at org.sosy_lab.cpachecker.core.CPAchecker.run(CPAchecker.java:301)
	at org.sosy_lab.cpachecker.cmdline.CPAMain.main(CPAMain.java:170)

This time the program is actually quite small, and it looks like this:

extern int __VERIFIER_nondet_int();

int main() {
    int i = __VERIFIER_nondet_int();
    int a[10];

    for (int n = 0; n < 10; ++n) {
        a[n] = __VERIFIER_nondet_int();
    }

    while (0 <= i && i < 10 && a[i] >= 0) {
        i = __VERIFIER_nondet_int();
        /* possible invalid dereference */
        a[i] = 0;
    }
    return 0;
}

I printed the formula that is being checked just before MathSAT crashes:

(set-logic ALL)
(set-option :produce-models true)

(declare-fun __VERIFIER_nondet_int!2@ () Int)
(declare-fun |main::i@3| () Int)
(declare-fun |__ADDRESS_OF_main::a@| () Int)
(declare-fun *int@1 () (Array Int Int))
(declare-fun |main::n@2| () Int)
(declare-fun __VERIFIER_nondet_int!3@ () Int)
(declare-fun *int@2 () (Array Int Int))
(declare-fun *int@3 () (Array Int Int))
(declare-fun *int@4 () (Array Int Int))
(declare-fun *int@5 () (Array Int Int))
(declare-fun *int@6 () (Array Int Int))
(declare-fun *int@7 () (Array Int Int))
(declare-fun *int@8 () (Array Int Int))
(declare-fun *int@9 () (Array Int Int))
(declare-fun *int@10 () (Array Int Int))
(declare-fun *int@11 () (Array Int Int))
(declare-fun __VERIFIER_nondet_int!4@ () Int)
(declare-fun |main::i@4| () Int)
(declare-fun *int@12 () (Array Int Int))
(declare-fun |main::n@3| () Int)
(declare-fun __VERIFIER_nondet_int!5@ () Int)
(declare-fun __VERIFIER_nondet_int!6@ () Int)
(declare-fun |main::n@4| () Int)
(declare-fun __VERIFIER_nondet_int!7@ () Int)
(declare-fun |main::n@5| () Int)
(declare-fun __VERIFIER_nondet_int!8@ () Int)
(declare-fun |main::n@6| () Int)
(declare-fun __VERIFIER_nondet_int!9@ () Int)
(declare-fun |main::n@7| () Int)
(declare-fun __VERIFIER_nondet_int!10@ () Int)
(declare-fun |main::n@8| () Int)
(declare-fun __VERIFIER_nondet_int!11@ () Int)
(declare-fun |main::n@9| () Int)
(declare-fun __VERIFIER_nondet_int!12@ () Int)
(declare-fun |main::n@10| () Int)
(declare-fun __VERIFIER_nondet_int!13@ () Int)
(declare-fun |main::n@11| () Int)
(declare-fun |main::n@12| () Int)
(assert (let ((.def_201 (* 4 |main::n@2|)))
(let ((.def_202 (+ |__ADDRESS_OF_main::a@| .def_201)))
(let ((.def_303 (store *int@1 .def_202 __VERIFIER_nondet_int!3@)))
(let ((.def_304 (= *int@2 .def_303)))
(let ((.def_76 (= |main::n@2| 0)))
(let ((.def_20 ((_ divisible 4) (- |__ADDRESS_OF_main::a@| 0))))
(let ((.def_18 (<= |__ADDRESS_OF_main::a@| 0)))
(let ((.def_19 (not .def_18)))
(let ((.def_50 (and .def_19 .def_20)))
(let ((.def_23 (<= |__ADDRESS_OF_main::a@| (- 40))))
(let ((.def_24 (not .def_23)))
(let ((.def_51 (and .def_24 .def_50)))
(let ((.def_15 (= __VERIFIER_nondet_int!2@ |main::i@3|)))
(let ((.def_52 (and .def_15 .def_51)))
(let ((.def_301 (and .def_52 .def_76)))
(let ((.def_163 (<= 10 |main::n@2|)))
(let ((.def_164 (not .def_163)))
(let ((.def_302 (and .def_164 .def_301)))
(let ((.def_305 (and .def_302 .def_304)))
(let ((.def_213 (* (- 1) |main::n@3|)))
(let ((.def_214 (+ |main::n@2| .def_213)))
(let ((.def_215 (= .def_214 (- 1))))
(let ((.def_306 (and .def_215 .def_305)))
(let ((.def_223 (<= 10 |main::n@3|)))
(let ((.def_224 (not .def_223)))
(let ((.def_8710 (and .def_224 .def_306)))
(let ((.def_340 (* 4 |main::n@3|)))
(let ((.def_341 (+ |__ADDRESS_OF_main::a@| .def_340)))
(let ((.def_1269 (store *int@2 .def_341 __VERIFIER_nondet_int!4@)))
(let ((.def_1270 (= *int@3 .def_1269)))
(let ((.def_8711 (and .def_1270 .def_8710)))
(let ((.def_351 (* (- 1) |main::n@4|)))
(let ((.def_352 (+ |main::n@3| .def_351)))
(let ((.def_353 (= .def_352 (- 1))))
(let ((.def_8712 (and .def_353 .def_8711)))
(let ((.def_1292 (<= 10 |main::n@4|)))
(let ((.def_1293 (not .def_1292)))
(let ((.def_8713 (and .def_1293 .def_8712)))
(let ((.def_1830 (* 4 |main::n@4|)))
(let ((.def_1831 (+ |__ADDRESS_OF_main::a@| .def_1830)))
(let ((.def_1832 (store *int@3 .def_1831 __VERIFIER_nondet_int!5@)))
(let ((.def_1833 (= *int@4 .def_1832)))
(let ((.def_8714 (and .def_1833 .def_8713)))
(let ((.def_1837 (* (- 1) |main::n@5|)))
(let ((.def_1838 (+ |main::n@4| .def_1837)))
(let ((.def_1839 (= .def_1838 (- 1))))
(let ((.def_8715 (and .def_1839 .def_8714)))
(let ((.def_1872 (<= 10 |main::n@5|)))
(let ((.def_1873 (not .def_1872)))
(let ((.def_8716 (and .def_1873 .def_8715)))
(let ((.def_2464 (* 4 |main::n@5|)))
(let ((.def_2465 (+ |__ADDRESS_OF_main::a@| .def_2464)))
(let ((.def_2466 (store *int@4 .def_2465 __VERIFIER_nondet_int!6@)))
(let ((.def_2467 (= *int@5 .def_2466)))
(let ((.def_8717 (and .def_2467 .def_8716)))
(let ((.def_2471 (* (- 1) |main::n@6|)))
(let ((.def_2472 (+ |main::n@5| .def_2471)))
(let ((.def_2473 (= .def_2472 (- 1))))
(let ((.def_8718 (and .def_2473 .def_8717)))
(let ((.def_2518 (<= 10 |main::n@6|)))
(let ((.def_2519 (not .def_2518)))
(let ((.def_8719 (and .def_2519 .def_8718)))
(let ((.def_3146 (* 4 |main::n@6|)))
(let ((.def_3147 (+ |__ADDRESS_OF_main::a@| .def_3146)))
(let ((.def_3148 (store *int@5 .def_3147 __VERIFIER_nondet_int!7@)))
(let ((.def_3149 (= *int@6 .def_3148)))
(let ((.def_8720 (and .def_3149 .def_8719)))
(let ((.def_3153 (* (- 1) |main::n@7|)))
(let ((.def_3154 (+ |main::n@6| .def_3153)))
(let ((.def_3155 (= .def_3154 (- 1))))
(let ((.def_8721 (and .def_3155 .def_8720)))
(let ((.def_3212 (<= 10 |main::n@7|)))
(let ((.def_3213 (not .def_3212)))
(let ((.def_8722 (and .def_3213 .def_8721)))
(let ((.def_3907 (* 4 |main::n@7|)))
(let ((.def_3908 (+ |__ADDRESS_OF_main::a@| .def_3907)))
(let ((.def_3909 (store *int@6 .def_3908 __VERIFIER_nondet_int!8@)))
(let ((.def_3910 (= *int@7 .def_3909)))
(let ((.def_8723 (and .def_3910 .def_8722)))
(let ((.def_3914 (* (- 1) |main::n@8|)))
(let ((.def_3915 (+ |main::n@7| .def_3914)))
(let ((.def_3916 (= .def_3915 (- 1))))
(let ((.def_8724 (and .def_3916 .def_8723)))
(let ((.def_3985 (<= 10 |main::n@8|)))
(let ((.def_3986 (not .def_3985)))
(let ((.def_8725 (and .def_3986 .def_8724)))
(let ((.def_4778 (* 4 |main::n@8|)))
(let ((.def_4779 (+ |__ADDRESS_OF_main::a@| .def_4778)))
(let ((.def_4780 (store *int@7 .def_4779 __VERIFIER_nondet_int!9@)))
(let ((.def_4781 (= *int@8 .def_4780)))
(let ((.def_8726 (and .def_4781 .def_8725)))
(let ((.def_4785 (* (- 1) |main::n@9|)))
(let ((.def_4786 (+ |main::n@8| .def_4785)))
(let ((.def_4787 (= .def_4786 (- 1))))
(let ((.def_8727 (and .def_4787 .def_8726)))
(let ((.def_4868 (<= 10 |main::n@9|)))
(let ((.def_4869 (not .def_4868)))
(let ((.def_8728 (and .def_4869 .def_8727)))
(let ((.def_5732 (* 4 |main::n@9|)))
(let ((.def_5733 (+ |__ADDRESS_OF_main::a@| .def_5732)))
(let ((.def_5734 (store *int@8 .def_5733 __VERIFIER_nondet_int!10@)))
(let ((.def_5735 (= *int@9 .def_5734)))
(let ((.def_8729 (and .def_5735 .def_8728)))
(let ((.def_5739 (* (- 1) |main::n@10|)))
(let ((.def_5740 (+ |main::n@9| .def_5739)))
(let ((.def_5741 (= .def_5740 (- 1))))
(let ((.def_8730 (and .def_5741 .def_8729)))
(let ((.def_5834 (<= 10 |main::n@10|)))
(let ((.def_5835 (not .def_5834)))
(let ((.def_8731 (and .def_5835 .def_8730)))
(let ((.def_6772 (* 4 |main::n@10|)))
(let ((.def_6773 (+ |__ADDRESS_OF_main::a@| .def_6772)))
(let ((.def_6774 (store *int@9 .def_6773 __VERIFIER_nondet_int!11@)))
(let ((.def_6775 (= *int@10 .def_6774)))
(let ((.def_8732 (and .def_6775 .def_8731)))
(let ((.def_6779 (* (- 1) |main::n@11|)))
(let ((.def_6780 (+ |main::n@10| .def_6779)))
(let ((.def_6781 (= .def_6780 (- 1))))
(let ((.def_8733 (and .def_6781 .def_8732)))
(let ((.def_6886 (<= 10 |main::n@11|)))
(let ((.def_6887 (not .def_6886)))
(let ((.def_8734 (and .def_6887 .def_8733)))
(let ((.def_7887 (* 4 |main::n@11|)))
(let ((.def_7888 (+ |__ADDRESS_OF_main::a@| .def_7887)))
(let ((.def_7889 (store *int@10 .def_7888 __VERIFIER_nondet_int!12@)))
(let ((.def_7890 (= *int@11 .def_7889)))
(let ((.def_8735 (and .def_7890 .def_8734)))
(let ((.def_7894 (* (- 1) |main::n@12|)))
(let ((.def_7895 (+ |main::n@11| .def_7894)))
(let ((.def_7896 (= .def_7895 (- 1))))
(let ((.def_8736 (and .def_7896 .def_8735)))
(let ((.def_8013 (<= 10 |main::n@12|)))
(let ((.def_8737 (and .def_8013 .def_8736)))
(let ((.def_170 (<= 0 |main::i@3|)))
(let ((.def_8738 (and .def_170 .def_8737)))
(let ((.def_173 (<= 10 |main::i@3|)))
(let ((.def_174 (not .def_173)))
(let ((.def_8739 (and .def_174 .def_8738)))
(let ((.def_179 (* 4 |main::i@3|)))
(let ((.def_181 (+ .def_179 |__ADDRESS_OF_main::a@|)))
(let ((.def_365 (select *int@11 .def_181)))
(let ((.def_366 (<= 0 .def_365)))
(let ((.def_8740 (and .def_366 .def_8739)))
(let ((.def_6964 (= |main::i@4| __VERIFIER_nondet_int!13@)))
(let ((.def_8741 (and .def_6964 .def_8740)))
(let ((.def_196 (* 4 |main::i@4|)))
(let ((.def_197 (+ |__ADDRESS_OF_main::a@| .def_196)))
(let ((.def_376 (store *int@11 .def_197 0)))
(let ((.def_377 (= *int@12 .def_376)))
(let ((.def_8742 (and .def_377 .def_8741)))
.def_8742)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
(get-model)

When I copy it into a file and run MathSAT from the command it will print the model just fine

There are two things that seem a little odd about the log:

• Why does MathSAT print the formulas (not (<= |__ADDRESS_OF_main::a@| 0)) and (= |__ADDRESS_OF_main::a@| 0) to the screen? This happens immediately after the call to Mathsat5NativeApi.msat_model_create_iterator that causes the exception (as MathSAT returns null for the iterator). Has anybody seen this before?
• Lasso prints a warning message about an "unknown sort" in one of the equalities. Is this normal? Or could this be a hint that there is something wrong with the terms we're using in MathSAT? I'm getting the same message with CVC5/Z3, so this is probably alright

[daniel-raffler]

I've reduced the test program a little further:

extern int __VERIFIER_nondet_int();

int main() {
  int i = __VERIFIER_nondet_int();
  int a[2];

  a[0] = __VERIFIER_nondet_int();
  a[1] = __VERIFIER_nondet_int();

  while (0 <= i && i < 2 && a[i] >= 0) {
    a[i] = 0;
    i = __VERIFIER_nondet_int();
  }
  return 0;
}

The exception will then be thrown while checking the counterexample:

bin/cpachecker --lassoRankerAnalysis --option solver.solver=mathsat5 --spec test/programs/benchmarks/properties/termination.prp test/programs/benchmarks/termination-crafted/NonTermination3-2.c
...
(not (<= |__ADDRESS_OF_main::a@| 0))
(= |__ADDRESS_OF_main::a@| 0)
Exception in thread "main" java.lang.IllegalArgumentException: MathSAT returned null
	at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_model_create_iterator(Native Method)
	at org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5Model.asList(Mathsat5Model.java:56)
	at org.sosy_lab.java_smt.basicimpl.CachingModel.asList(CachingModel.java:40)
	at org.sosy_lab.java_smt.api.BasicProverEnvironment.getModelAssignments(BasicProverEnvironment.java:112)
	at org.sosy_lab.cpachecker.util.predicates.smt.BasicProverEnvironmentView.getModelAssignments(BasicProverEnvironmentView.java:71)
	at org.sosy_lab.cpachecker.util.predicates.PathChecker.getModel(PathChecker.java:368)
	at org.sosy_lab.cpachecker.util.predicates.PathChecker.createCounterexample(PathChecker.java:227)
	at org.sosy_lab.cpachecker.util.predicates.PathChecker.handleFeasibleCounterexample(PathChecker.java:179)
	at org.sosy_lab.cpachecker.cpa.predicate.PredicateStaticRefiner.performStaticRefinementForPath(PredicateStaticRefiner.java:267)
	at org.sosy_lab.cpachecker.cpa.predicate.PredicateStaticRefiner.performRefinementForPath(PredicateStaticRefiner.java:200)
	at org.sosy_lab.cpachecker.cpa.arg.AbstractARGBasedRefiner.performRefinementForPath(AbstractARGBasedRefiner.java:158)
	at org.sosy_lab.cpachecker.cpa.arg.AbstractARGBasedRefiner.performRefinement(AbstractARGBasedRefiner.java:104)
	at org.sosy_lab.cpachecker.core.algorithm.CEGARAlgorithm.refine(CEGARAlgorithm.java:307)
	at org.sosy_lab.cpachecker.core.algorithm.CEGARAlgorithm.run(CEGARAlgorithm.java:253)
	at org.sosy_lab.cpachecker.core.algorithm.termination.TerminationAlgorithm.proveLoopTermination(TerminationAlgorithm.java:306)
	at org.sosy_lab.cpachecker.core.algorithm.termination.TerminationAlgorithm.run0(TerminationAlgorithm.java:259)
	at org.sosy_lab.cpachecker.core.algorithm.termination.TerminationAlgorithm.run(TerminationAlgorithm.java:223)
	at org.sosy_lab.cpachecker.core.CPAchecker.runAlgorithm(CPAchecker.java:533)
	at org.sosy_lab.cpachecker.core.CPAchecker.run0(CPAchecker.java:392)
	at org.sosy_lab.cpachecker.core.CPAchecker.run(CPAchecker.java:301)
	at org.sosy_lab.cpachecker.cmdline.CPAMain.main(CPAMain.java:170)

Here is the code for PathChecker.createCounterexample, the last method before we try to get the model:

private CounterexampleInfo createCounterexample(
      final ARGPath precisePath, final CounterexampleTraceInfo pInfo) throws InterruptedException {

    try (ProverEnvironment prover = solver.newProverEnvironment(ProverOptions.GENERATE_MODELS)) {

      Pair<PathFormula, List<SSAMap>> replayedPath = createPrecisePathFormula(precisePath);
      List<SSAMap> ssaMaps = replayedPath.getSecond();
      BooleanFormula pathFormula = replayedPath.getFirstNotNull().getFormula();

      prover.push(pathFormula);

      if (prover.isUnsat()) {
        logger.log(
            Level.WARNING,
            "Inconsistent replayed error path! No variable values will be available.");
        return createImpreciseCounterexample(precisePath, pInfo);
      }

      ImmutableList<ValueAssignment> model = getModel(prover); 
      ....

The exception is thrown in the last line as MathSAT can't produce the model. What's interesting is that we're actually using a new solver stack with pathFormula as the only assertion. I've tried printing pathFormula and it looks like this:

(declare-fun __VERIFIER_nondet_int!2@ () Int)
(declare-fun |main::i@3| () Int)
(declare-fun |__ADDRESS_OF_main::a@| () Int)
(declare-fun *int@1 () (Array Int Int))
(declare-fun __VERIFIER_nondet_int!3@ () Int)
(declare-fun *int@2 () (Array Int Int))
(declare-fun __VERIFIER_nondet_int!4@ () Int)
(declare-fun *int@3 () (Array Int Int))
(declare-fun __VERIFIER_nondet_int!5@ () Int)
(declare-fun *int@4 () (Array Int Int))
(declare-fun |main::i@4| () Int)
(assert (let ((.def_256 (= __VERIFIER_nondet_int!5@ |main::i@4|)))
(let ((.def_82 (<= 0 |main::i@3|)))
(let ((.def_39 (+ |__ADDRESS_OF_main::a@| 4)))
(let ((.def_40 (store *int@2 .def_39 __VERIFIER_nondet_int!4@)))
(let ((.def_41 (= *int@3 .def_40)))
(let ((.def_33 (store *int@1 |__ADDRESS_OF_main::a@| __VERIFIER_nondet_int!3@)))
(let ((.def_34 (= *int@2 .def_33)))
(let ((.def_20 ((_ divisible 4) (- |__ADDRESS_OF_main::a@| 0))))
(let ((.def_18 (<= |__ADDRESS_OF_main::a@| 0)))
(let ((.def_19 (not .def_18)))
(let ((.def_28 (and .def_19 .def_20)))
(let ((.def_23 (<= |__ADDRESS_OF_main::a@| (- 8))))
(let ((.def_24 (not .def_23)))
(let ((.def_29 (and .def_24 .def_28)))
(let ((.def_15 (= __VERIFIER_nondet_int!2@ |main::i@3|)))
(let ((.def_30 (and .def_15 .def_29)))
(let ((.def_36 (and .def_30 .def_34)))
(let ((.def_43 (and .def_36 .def_41)))
(let ((.def_252 (and .def_43 .def_82)))
(let ((.def_90 (<= 2 |main::i@3|)))
(let ((.def_91 (not .def_90)))
(let ((.def_253 (and .def_91 .def_252)))
(let ((.def_98 (* 4 |main::i@3|)))
(let ((.def_100 (+ .def_98 |__ADDRESS_OF_main::a@|)))
(let ((.def_107 (select *int@3 .def_100)))
(let ((.def_108 (<= 0 .def_107)))
(let ((.def_254 (and .def_108 .def_253)))
(let ((.def_126 (store *int@3 .def_100 0)))
(let ((.def_127 (= *int@4 .def_126)))
(let ((.def_255 (and .def_127 .def_254)))
(let ((.def_257 (and .def_255 .def_256)))
.def_257))))))))))))))))))))))))))))))))

When I try to solve this formula in a different project with MathSat everything works fine and the model can be printed. However, in createCounterexample it will crash, even if I don't use pathFormula, but recreate the entire formula from scratch:

private CounterexampleInfo createCounterexample(
      final ARGPath precisePath, final CounterexampleTraceInfo pInfo) throws InterruptedException {

    try (ProverEnvironment prover = solver.newProverEnvironment(ProverOptions.GENERATE_MODELS)) {

      Pair<PathFormula, List<SSAMap>> replayedPath = createPrecisePathFormula(precisePath);
      List<SSAMap> ssaMaps = replayedPath.getSecond();
      BooleanFormula pathFormula = replayedPath.getFirstNotNull().getFormula();

      IntegerFormulaManagerView imgr = solver.getFormulaManager().getIntegerFormulaManager();
      ArrayFormulaManagerView amgr = solver.getFormulaManager().getArrayFormulaManager();
      BooleanFormulaManagerView bmgr = solver.getFormulaManager().getBooleanFormulaManager();

      IntegerFormula nd2 = imgr.makeVariable("__VERIFIER_nondet_int!2@");
      IntegerFormula nd3 = imgr.makeVariable("__VERIFIER_nondet_int!3@");
      IntegerFormula nd4 = imgr.makeVariable("__VERIFIER_nondet_int!4@");
      IntegerFormula nd5 = imgr.makeVariable("__VERIFIER_nondet_int!5@");

      IntegerFormula i3 = imgr.makeVariable("main::i@3");
      IntegerFormula i4 = imgr.makeVariable("main::i@4");

      IntegerFormula a = imgr.makeVariable("__ADDRESS_OF_main::a@");

      ArrayFormula<IntegerFormula, IntegerFormula> int1 = amgr.makeArray("*int@1", FormulaType.getArrayType(FormulaType.IntegerType, FormulaType.IntegerType));
      ArrayFormula<IntegerFormula, IntegerFormula> int2 = amgr.makeArray("*int@2", FormulaType.getArrayType(FormulaType.IntegerType, FormulaType.IntegerType));
      ArrayFormula<IntegerFormula, IntegerFormula> int3 = amgr.makeArray("*int@3", FormulaType.getArrayType(FormulaType.IntegerType, FormulaType.IntegerType));
      ArrayFormula<IntegerFormula, IntegerFormula> int4 = amgr.makeArray("*int@4", FormulaType.getArrayType(FormulaType.IntegerType, FormulaType.IntegerType));

      BooleanFormula def256 = imgr.equal(nd5, i4);
      BooleanFormula def82 = imgr.lessOrEquals(imgr.makeNumber(0), i3);
      IntegerFormula def39 = imgr.add(a, imgr.makeNumber(4));
      ArrayFormula<IntegerFormula, IntegerFormula> def40 = amgr.store(int2, def39, nd4);
      BooleanFormula def41 = amgr.equivalence(int3, def40);
      ArrayFormula<IntegerFormula, IntegerFormula> def33 = amgr.store(int1, a, nd3);
      BooleanFormula def34 = amgr.equivalence(int2, def33);
      BooleanFormula def20 = imgr.modularCongruence(a, imgr.makeNumber(0), 4);
      BooleanFormula def18 = imgr.lessOrEquals(a, imgr.makeNumber(0));
      BooleanFormula def19 = bmgr.not(def18);
      BooleanFormula def28 = bmgr.and(def19, def20);
      BooleanFormula def23 = imgr.lessOrEquals(a, imgr.makeNumber(-8));
      BooleanFormula def24 = bmgr.not(def23);
      BooleanFormula def29 = bmgr.and(def24, def28);
      BooleanFormula def15 = imgr.equal(nd2, i3);
      BooleanFormula def30 = bmgr.and(def15, def29);
      BooleanFormula def36 = bmgr.and(def30, def34);
      BooleanFormula def43 = bmgr.and(def36, def41);
      BooleanFormula def252 = bmgr.and(def43, def82);
      BooleanFormula def90 = imgr.lessOrEquals(imgr.makeNumber(2), i3);
      BooleanFormula def91 = bmgr.not(def90);
      BooleanFormula def253 = bmgr.and(def91, def252);
      IntegerFormula def98 = imgr.multiply(imgr.makeNumber(4), i3);
      IntegerFormula def100 = imgr.add(def98, a);
      IntegerFormula def107 = amgr.select(int3, def100);
      BooleanFormula def108 = imgr.lessOrEquals(imgr.makeNumber(0), def107);
      BooleanFormula def254 = bmgr.and(def108, def253);
      ArrayFormula<IntegerFormula, IntegerFormula> def126 = amgr.store(int3, def100, imgr.makeNumber(0));
      BooleanFormula def127 = amgr.equivalence(int4, def126);
      BooleanFormula def255 = bmgr.and(def127, def254);
      BooleanFormula def257 = bmgr.and(def255, def256);

      prover.push(def257);

      // prover.push(pathFormula);

      if (prover.isUnsat()) {
        logger.log(
            Level.WARNING,
            "Inconsistent replayed error path! No variable values will be available.");
        return createImpreciseCounterexample(precisePath, pInfo);
      }

      ImmutableList<ValueAssignment> model = getModel(prover); // Still crashes
      ...

However, when I rename the variable __ADDRESS_OF_main::a@ to something else that will suddenly fix the issue. This makes some sort of sense as MathSAT does dump two formulas about __ADDRESS_OF_main::a@ when crashing: (not (<= |__ADDRESS_OF_main::a@| 0)) and (= |__ADDRESS_OF_main::a@| 0). The first one is from our assertions, but I've no idea where it gets the second formula. Since we created a new prover just for this formula, there really shouldn't be any other constraints on the solver stack.

On the other hand creating a new solver instance to check the formula also seems to fix the issue:

  private CounterexampleInfo createCounterexample(
      final ARGPath precisePath, final CounterexampleTraceInfo pInfo) throws InterruptedException {

    Solver solver1;
    try {
      solver1 =
          Solver.create(
              Configuration.defaultConfiguration(), logger, ShutdownNotifier.createDummy());
    } catch (InvalidConfigurationException pE) {
      throw new RuntimeException(pE);
    }

    try (ProverEnvironment prover = solver1.newProverEnvironment(ProverOptions.GENERATE_MODELS)) {

      Pair<PathFormula, List<SSAMap>> replayedPath = createPrecisePathFormula(precisePath);
      List<SSAMap> ssaMaps = replayedPath.getSecond();
      BooleanFormula pathFormula = replayedPath.getFirstNotNull().getFormula();

      // prover.push(pathFormula);
      
      FormulaManagerView fmgr = solver.getFormulaManager();
      FormulaManagerView fmgr1 = solver1.getFormulaManager();

      // Move the formula to the new context and then push it
      prover.push(fmgr1.parse(fmgr.dumpFormula(pathFormula).toString()));

      if (prover.isUnsat()) {
        logger.log(
            Level.WARNING,
            "Inconsistent replayed error path! No variable values will be available.");
        return createImpreciseCounterexample(precisePath, pInfo);
      }

      ImmutableList<ValueAssignment> model = getModel(prover); // Now it works
      ...   

Note that just recreating the formula with prover.push(fmgr1.parse(fmgr.dumpFormula(pathFormula).toString())); on the same solver is not enough. We need a completely new solver instance as MathSAT otherwise seems to "remember" some constraints from earlier, even if we use a whole new solver stack.

Does anybody have an idea how to debug this further? The example I have is reproducible, but it's very hard to trigger the issue outside of CPAchecker.

[PhilippWendler]

We shouldn't debug this at all, this is a waste of time IMO. It is clearly a bug in MathSAT, and its source code is closed, so even if we would know more we couldn't do anything about it. The only reasonable thing is to report the bug to the MathSAT developers, ideally with a way to reproduce it outside of CPAchecker, if that is possible with acceptable effort (otherwise they can still debug it from within CPAchecker). In this case, if the bug is not reproducible with an .smt2 file, it seems easy to just write a C program that creates the formula and triggers it.

[baierd]

This is a very similar issue to the tainted environment we encountered when continuing after some interpolation errors in 2022 here!

2 Things we should do:

• Find the initial cause (e.g. when does this occur. In the interpolation issue it only happened after some some special message) and report this to the MathSAT5 devs, as well as add docu for us and our users!
• CPAchecker can use the same trick i implemented back-then and just export the query as SMTLIB2, build a new context, import the problem and continue. (We might even want to add options to 1. always build a distinct context for CEX and 2. maybe even give the option to choose a distinct solver?). But this should be discussed in CPAchecker!

[daniel-raffler]

I've tried running it with --option solver.logAllQueries=true, which produces two .smt2 files. However, both work fine on the command line, and MathSAT will print a model without crashing

I've also not been able to find any previous errors that were caught by the analysis. Whatever has corrupted the solver context only seems to get noticed when the model is generated

[daniel-raffler]

I've finally been able to reproduce the bug in JavaSMT:

package example;

import com.google.common.collect.ImmutableList;
import org.sosy_lab.common.ShutdownNotifier;
import org.sosy_lab.common.configuration.Configuration;
import org.sosy_lab.common.configuration.InvalidConfigurationException;
import org.sosy_lab.common.log.LogManager;
import org.sosy_lab.java_smt.SolverContextFactory;
import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
import org.sosy_lab.java_smt.api.*;

import java.math.BigInteger;

public class MathsatModelBug {
    public static void main(String[] args) throws InvalidConfigurationException, SolverException, InterruptedException {
        Configuration config = Configuration.defaultConfiguration();
        LogManager logger = LogManager.createNullLogManager();
        ShutdownNotifier notifier = ShutdownNotifier.createDummy();

        try (SolverContext context = SolverContextFactory.createSolverContext(config, logger, notifier, Solvers.MATHSAT5)) {
            FormulaManager mgr = context.getFormulaManager();
            var f1 = mgr.getUFManager().declareUF("_&_", FormulaType.IntegerType, ImmutableList.of(FormulaType.IntegerType, FormulaType.IntegerType));
            var f2 = mgr.getUFManager().declareUF("_!!_", FormulaType.IntegerType, ImmutableList.of(FormulaType.IntegerType, FormulaType.IntegerType));
            var f3 = mgr.getUFManager().declareUF("_^_", FormulaType.IntegerType, ImmutableList.of(FormulaType.IntegerType, FormulaType.IntegerType));
            var f4 = mgr.getUFManager().declareUF("_~_", FormulaType.IntegerType, ImmutableList.of(FormulaType.IntegerType));
            var f5 = mgr.getUFManager().declareUF("_<<_", FormulaType.IntegerType, ImmutableList.of(FormulaType.IntegerType, FormulaType.IntegerType));
            var f6 = mgr.getUFManager().declareUF("_>>_", FormulaType.IntegerType, ImmutableList.of(FormulaType.IntegerType, FormulaType.IntegerType));
            var f7 = mgr.getUFManager().declareUF("_%_", FormulaType.IntegerType, ImmutableList.of(FormulaType.IntegerType, FormulaType.IntegerType));

            var d57624756 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d713898436 = mgr.getBooleanFormulaManager().makeTrue();
            var d102318785 = mgr.getBooleanFormulaManager().makeFalse();
            var d1599823012 = mgr.getBooleanFormulaManager().and(d713898436, d713898436);
            var d742568993 = mgr.getBooleanFormulaManager().and(d713898436, d713898436);
            var d7346738 = mgr.getBooleanFormulaManager().and(d713898436, d713898436);
            var d1940912369 = mgr.getBooleanFormulaManager().and(d713898436, d713898436);
            var d943666520 = mgr.getIntegerFormulaManager().makeNumber(4);
            var d688988404 = mgr.getBooleanFormulaManager().and(d713898436, d713898436);
            var d1098568947 = mgr.getBooleanFormulaManager().and(d688988404, d713898436);
            var d795594631 = mgr.getBooleanFormulaManager().and(d713898436, d1098568947);
            var d1299145277 = mgr.getIntegerFormulaManager().makeVariable("__VERIFIER_nondet_int!2@");
            var d800456240 = mgr.getIntegerFormulaManager().makeVariable("main::i@3");
            var d1164699452 = mgr.getIntegerFormulaManager().equal(d800456240, d1299145277);
            var d594916129 = mgr.getBooleanFormulaManager().and(d713898436, d1164699452);
            var d1537912396 = mgr.getBooleanFormulaManager().and(d594916129, d713898436);
            var d1533972343 = mgr.getBooleanFormulaManager().and(d795594631, d1537912396);
            var d1329897103 = mgr.getIntegerFormulaManager().makeNumber(8);
            var d1091736037 = mgr.getIntegerFormulaManager().makeVariable("__ADDRESS_OF_main::a@");
            var d1848163207 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d435175610 = mgr.getIntegerFormulaManager().greaterThan(d1091736037, d1848163207);
            var d1923810797 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d669200356 = mgr.getIntegerFormulaManager().modularCongruence(d1091736037, d1923810797, new BigInteger("4"));
            var d205278236 = mgr.getIntegerFormulaManager().makeNumber(8);
            var d399653041 = mgr.getIntegerFormulaManager().add(d1091736037, d205278236);
            var d1031586763 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d56510351 = mgr.getIntegerFormulaManager().greaterThan(d399653041, d1031586763);
            var d1803361784 = mgr.getIntegerFormulaManager().makeVariable("__ADDRESS_OF_main::a@");
            var d1243102466 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d1519911160 = mgr.getIntegerFormulaManager().makeNumber(4);
            var d339581587 = mgr.getIntegerFormulaManager().multiply(d1519911160, d1243102466);
            var d1075996552 = mgr.getIntegerFormulaManager().add(d1803361784, d339581587);
            var d1047477166 = mgr.getArrayFormulaManager().makeArray("*int@1", FormulaType.IntegerType, FormulaType.IntegerType);
            var d749693202 = mgr.getArrayFormulaManager().makeArray("*int@1", FormulaType.IntegerType, FormulaType.IntegerType);
            var d1943444495 = mgr.getArrayFormulaManager().equivalence(d749693202, d1047477166);
            var d874740624 = mgr.getBooleanFormulaManager().and(d713898436, d713898436);
            var d486662053 = mgr.getBooleanFormulaManager().not(d713898436);
            var d1244775150 = mgr.getBooleanFormulaManager().and(d486662053, d1943444495);
            var d222300483 = mgr.getBooleanFormulaManager().or(d874740624, d1244775150);
            var d571481216 = mgr.getBooleanFormulaManager().and(d713898436, d222300483);
            var d838800272 = mgr.getIntegerFormulaManager().makeNumber(1);
            var d1973256691 = mgr.getIntegerFormulaManager().makeNumber(4);
            var d2015007762 = mgr.getIntegerFormulaManager().multiply(d1973256691, d838800272);
            var d1514955661 = mgr.getIntegerFormulaManager().add(d1803361784, d2015007762);
            var d333879495 = mgr.getArrayFormulaManager().makeArray("*int@1", FormulaType.IntegerType, FormulaType.IntegerType);
            var d183304529 = mgr.getArrayFormulaManager().makeArray("*int@1", FormulaType.IntegerType, FormulaType.IntegerType);
            var d645643802 = mgr.getArrayFormulaManager().equivalence(d183304529, d333879495);
            var d521331027 = mgr.getBooleanFormulaManager().and(d713898436, d713898436);
            var d949314262 = mgr.getBooleanFormulaManager().not(d713898436);
            var d1511004956 = mgr.getBooleanFormulaManager().and(d949314262, d645643802);
            var d559998250 = mgr.getBooleanFormulaManager().or(d521331027, d1511004956);
            var d703627308 = mgr.getBooleanFormulaManager().and(d571481216, d559998250);
            var d979420182 = mgr.getBooleanFormulaManager().and(d713898436, d703627308);
            var d1626529981 = mgr.getBooleanFormulaManager().and(d435175610, d713898436);
            var d1184694332 = mgr.getBooleanFormulaManager().and(d669200356, d1626529981);
            var d1799424291 = mgr.getBooleanFormulaManager().and(d56510351, d1184694332);
            var d1472012329 = mgr.getBooleanFormulaManager().and(d979420182, d1799424291);
            var d540923243 = mgr.getBooleanFormulaManager().and(d1533972343, d1472012329);
            var d1835316563 = mgr.getIntegerFormulaManager().makeVariable("__ADDRESS_OF_main::a@");
            var d1399225534 = mgr.getIntegerFormulaManager().makeNumber(new BigInteger("0"));
            var d1857007886 = mgr.getIntegerFormulaManager().makeNumber(4);
            var d648630181 = mgr.getIntegerFormulaManager().multiply(d1857007886, d1399225534);
            var d1179272258 = mgr.getIntegerFormulaManager().add(d1835316563, d648630181);
            var d678680178 = mgr.getIntegerFormulaManager().makeVariable("__VERIFIER_nondet_int!3@");
            var d1124317168 = mgr.getArrayFormulaManager().makeArray("*int@1", FormulaType.IntegerType, FormulaType.IntegerType);
            var d1970612644 = mgr.getArrayFormulaManager().makeArray("*int@2", FormulaType.IntegerType, FormulaType.IntegerType);
            var d2006835220 = mgr.getArrayFormulaManager().store(d1124317168, d1179272258, d678680178);
            var d1547817015 = mgr.getArrayFormulaManager().equivalence(d1970612644, d2006835220);
            var d35864696 = mgr.getArrayFormulaManager().makeArray("*int@1", FormulaType.IntegerType, FormulaType.IntegerType);
            var d1590129041 = mgr.getArrayFormulaManager().makeArray("*int@2", FormulaType.IntegerType, FormulaType.IntegerType);
            var d1178777373 = mgr.getArrayFormulaManager().equivalence(d1590129041, d35864696);
            var d340789130 = mgr.getBooleanFormulaManager().and(d713898436, d1547817015);
            var d208184824 = mgr.getBooleanFormulaManager().not(d713898436);
            var d1774589469 = mgr.getBooleanFormulaManager().and(d208184824, d1178777373);
            var d988786279 = mgr.getBooleanFormulaManager().or(d340789130, d1774589469);
            var d773296871 = mgr.getBooleanFormulaManager().and(d713898436, d988786279);
            var d1729734072 = mgr.getBooleanFormulaManager().and(d773296871, d713898436);
            var d1052127672 = mgr.getBooleanFormulaManager().and(d540923243, d1729734072);
            var d1811880447 = mgr.getIntegerFormulaManager().makeVariable("__ADDRESS_OF_main::a@");
            var d1105282397 = mgr.getIntegerFormulaManager().makeNumber(new BigInteger("1"));
            var d1314228008 = mgr.getIntegerFormulaManager().makeNumber(4);
            var d1590481849 = mgr.getIntegerFormulaManager().multiply(d1314228008, d1105282397);
            var d1299126654 = mgr.getIntegerFormulaManager().add(d1811880447, d1590481849);
            var d116356643 = mgr.getIntegerFormulaManager().makeVariable("__VERIFIER_nondet_int!4@");
            var d1692523793 = mgr.getArrayFormulaManager().makeArray("*int@2", FormulaType.IntegerType, FormulaType.IntegerType);
            var d1544067887 = mgr.getArrayFormulaManager().makeArray("*int@3", FormulaType.IntegerType, FormulaType.IntegerType);
            var d1771687225 = mgr.getArrayFormulaManager().store(d1692523793, d1299126654, d116356643);
            var d347791431 = mgr.getArrayFormulaManager().equivalence(d1544067887, d1771687225);
            var d2128195220 = mgr.getArrayFormulaManager().makeArray("*int@2", FormulaType.IntegerType, FormulaType.IntegerType);
            var d1720746883 = mgr.getArrayFormulaManager().makeArray("*int@3", FormulaType.IntegerType, FormulaType.IntegerType);
            var d1095203437 = mgr.getArrayFormulaManager().equivalence(d1720746883, d2128195220);
            var d45880026 = mgr.getBooleanFormulaManager().and(d713898436, d347791431);
            var d824357143 = mgr.getBooleanFormulaManager().not(d713898436);
            var d1397530667 = mgr.getBooleanFormulaManager().and(d824357143, d1095203437);
            var d698498109 = mgr.getBooleanFormulaManager().or(d45880026, d1397530667);
            var d1265287441 = mgr.getBooleanFormulaManager().and(d713898436, d698498109);
            var d1877240674 = mgr.getBooleanFormulaManager().and(d1265287441, d713898436);
            var d1495257933 = mgr.getBooleanFormulaManager().and(d1052127672, d1877240674);
            var d1962865655 = mgr.getIntegerFormulaManager().makeNumber(4);
            var d704869156 = mgr.getBooleanFormulaManager().and(d713898436, d713898436);
            var d1777043124 = mgr.getBooleanFormulaManager().and(d704869156, d713898436);
            var d1482344533 = mgr.getBooleanFormulaManager().and(d1495257933, d1777043124);
            var d1366212088 = mgr.getIntegerFormulaManager().makeNumber(8);
            var d1300576734 = mgr.getIntegerFormulaManager().makeVariable("__ADDRESS_OF_main::a__TERMINATION_PRIMED@");
            var d1052399527 = mgr.getIntegerFormulaManager().greaterThan(d1300576734, d399653041);
            var d657069980 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d51376124 = mgr.getIntegerFormulaManager().modularCongruence(d1300576734, d657069980, new BigInteger("4"));
            var d1730182538 = mgr.getIntegerFormulaManager().makeNumber(8);
            var d197855654 = mgr.getIntegerFormulaManager().add(d1300576734, d1730182538);
            var d2083154356 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d10885570 = mgr.getIntegerFormulaManager().greaterThan(d197855654, d2083154356);
            var d1687087217 = mgr.getIntegerFormulaManager().makeVariable("__ADDRESS_OF_main::a__TERMINATION_PRIMED@");
            var d403960809 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d684429600 = mgr.getIntegerFormulaManager().makeNumber(4);
            var d991242536 = mgr.getIntegerFormulaManager().multiply(d684429600, d403960809);
            var d1450712470 = mgr.getIntegerFormulaManager().add(d1687087217, d991242536);
            var d1366499339 = mgr.getArrayFormulaManager().makeArray("*int@3", FormulaType.IntegerType, FormulaType.IntegerType);
            var d633727380 = mgr.getArrayFormulaManager().makeArray("*int@3", FormulaType.IntegerType, FormulaType.IntegerType);
            var d931911789 = mgr.getArrayFormulaManager().equivalence(d633727380, d1366499339);
            var d562685863 = mgr.getBooleanFormulaManager().and(d713898436, d713898436);
            var d1773336805 = mgr.getBooleanFormulaManager().not(d713898436);
            var d1664165134 = mgr.getBooleanFormulaManager().and(d1773336805, d931911789);
            var d168870325 = mgr.getBooleanFormulaManager().or(d562685863, d1664165134);
            var d1682619279 = mgr.getBooleanFormulaManager().and(d713898436, d168870325);
            var d440472115 = mgr.getIntegerFormulaManager().makeNumber(1);
            var d1882348832 = mgr.getIntegerFormulaManager().makeNumber(4);
            var d2082678778 = mgr.getIntegerFormulaManager().multiply(d1882348832, d440472115);
            var d1300528434 = mgr.getIntegerFormulaManager().add(d1687087217, d2082678778);
            var d1598434875 = mgr.getArrayFormulaManager().makeArray("*int@3", FormulaType.IntegerType, FormulaType.IntegerType);
            var d1031775150 = mgr.getArrayFormulaManager().makeArray("*int@3", FormulaType.IntegerType, FormulaType.IntegerType);
            var d1476812556 = mgr.getArrayFormulaManager().equivalence(d1031775150, d1598434875);
            var d906347731 = mgr.getBooleanFormulaManager().and(d713898436, d713898436);
            var d1482429406 = mgr.getBooleanFormulaManager().not(d713898436);
            var d410958248 = mgr.getBooleanFormulaManager().and(d1482429406, d1476812556);
            var d1919576980 = mgr.getBooleanFormulaManager().or(d906347731, d410958248);
            var d1792088662 = mgr.getBooleanFormulaManager().and(d1682619279, d1919576980);
            var d1378559537 = mgr.getBooleanFormulaManager().and(d713898436, d1792088662);
            var d1073051173 = mgr.getBooleanFormulaManager().and(d1052399527, d713898436);
            var d518167684 = mgr.getBooleanFormulaManager().and(d51376124, d1073051173);
            var d2088969892 = mgr.getBooleanFormulaManager().and(d10885570, d518167684);
            var d1997704619 = mgr.getBooleanFormulaManager().and(d1378559537, d2088969892);
            var d1665308978 = mgr.getBooleanFormulaManager().and(d1482344533, d1997704619);
            var d211649273 = mgr.getBooleanFormulaManager().and(d713898436, d713898436);
            var d419280591 = mgr.getBooleanFormulaManager().and(d713898436, d713898436);
            var d1932244589 = mgr.getBooleanFormulaManager().and(d713898436, d1665308978);
            var d1340086275 = mgr.getIntegerFormulaManager().makeNumber(new BigInteger("0"));
            var d332498651 = mgr.getIntegerFormulaManager().makeNumber(new BigInteger("1"));
            var d1503614751 = mgr.getIntegerFormulaManager().equal(d1340086275, d332498651);
            var d129371198 = mgr.getIntegerFormulaManager().makeNumber(1);
            var d66845334 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d1701436909 = mgr.getBooleanFormulaManager().ifThenElse(d1503614751, d129371198, d66845334);
            var d1896708863 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d719182854 = mgr.getIntegerFormulaManager().equal(d1701436909, d1896708863);
            var d807239968 = mgr.getBooleanFormulaManager().not(d719182854);
            var d1832284192 = mgr.getBooleanFormulaManager().not(d807239968);
            var d1917161212 = mgr.getBooleanFormulaManager().and(d1832284192, d713898436);
            var d882706486 = mgr.getBooleanFormulaManager().and(d713898436, d713898436);
            var d1041451158 = mgr.getIntegerFormulaManager().makeNumber(new BigInteger("0"));
            var d1924802798 = mgr.getIntegerFormulaManager().makeNumber(new BigInteger("1"));
            var d775574071 = mgr.getIntegerFormulaManager().equal(d1041451158, d1924802798);
            var d1320869181 = mgr.getIntegerFormulaManager().makeNumber(1);
            var d1791589252 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d1226298219 = mgr.getBooleanFormulaManager().ifThenElse(d775574071, d1320869181, d1791589252);
            var d901815188 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d755759908 = mgr.getIntegerFormulaManager().equal(d1226298219, d901815188);
            var d205496410 = mgr.getBooleanFormulaManager().not(d755759908);
            var d2068100669 = mgr.getBooleanFormulaManager().and(d205496410, d713898436);
            var d1248435962 = mgr.getBooleanFormulaManager().and(d713898436, d2068100669);
            var d397309480 = mgr.getIntegerFormulaManager().makeNumber(4);
            var d288797801 = mgr.getBooleanFormulaManager().and(d713898436, d713898436);
            var d1702478809 = mgr.getBooleanFormulaManager().and(d288797801, d713898436);
            var d45643137 = mgr.getBooleanFormulaManager().and(d713898436, d1702478809);
            var d1715686600 = mgr.getIntegerFormulaManager().makeNumber(4);
            var d1123166613 = mgr.getBooleanFormulaManager().and(d713898436, d713898436);
            var d1765690649 = mgr.getBooleanFormulaManager().and(d1123166613, d713898436);
            var d678115778 = mgr.getBooleanFormulaManager().and(d1248435962, d1765690649);
            var d471004142 = mgr.getIntegerFormulaManager().makeVariable("__VERIFIER_nondet_int!5@");
            var d1833335943 = mgr.getIntegerFormulaManager().makeVariable("int main();::__CPAchecker_termination_temp@3");
            var d689448569 = mgr.getIntegerFormulaManager().equal(d1833335943, d471004142);
            var d1472036907 = mgr.getBooleanFormulaManager().and(d713898436, d689448569);
            var d1555793073 = mgr.getBooleanFormulaManager().and(d1472036907, d713898436);
            var d46627301 = mgr.getBooleanFormulaManager().and(d45643137, d1555793073);
            var d1787083818 = mgr.getIntegerFormulaManager().makeVariable("__VERIFIER_nondet_int!5@");
            var d1367594377 = mgr.getIntegerFormulaManager().makeVariable("int main();::__CPAchecker_termination_temp@3");
            var d1360878852 = mgr.getIntegerFormulaManager().equal(d1367594377, d1787083818);
            var d1747721875 = mgr.getBooleanFormulaManager().and(d713898436, d1360878852);
            var d654740048 = mgr.getBooleanFormulaManager().and(d1747721875, d713898436);
            var d1759915172 = mgr.getBooleanFormulaManager().and(d678115778, d654740048);
            var d777190206 = mgr.getIntegerFormulaManager().makeVariable("int main();::__CPAchecker_termination_temp@3");
            var d385784873 = mgr.getIntegerFormulaManager().makeNumber(new BigInteger("0"));
            var d1050149826 = mgr.getIntegerFormulaManager().equal(d777190206, d385784873);
            var d1160106451 = mgr.getIntegerFormulaManager().makeNumber(1);
            var d2090289474 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d518692141 = mgr.getBooleanFormulaManager().ifThenElse(d1050149826, d1160106451, d2090289474);
            var d1620187937 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d198374825 = mgr.getIntegerFormulaManager().equal(d518692141, d1620187937);
            var d1296654536 = mgr.getBooleanFormulaManager().not(d198374825);
            var d125865913 = mgr.getBooleanFormulaManager().not(d1296654536);
            var d2000410491 = mgr.getBooleanFormulaManager().and(d125865913, d713898436);
            var d1800932232 = mgr.getBooleanFormulaManager().and(d46627301, d2000410491);
            var d1838250251 = mgr.getIntegerFormulaManager().makeVariable("int main();::__CPAchecker_termination_temp@3");
            var d1852821063 = mgr.getIntegerFormulaManager().makeNumber(new BigInteger("0"));
            var d1204178174 = mgr.getIntegerFormulaManager().equal(d1838250251, d1852821063);
            var d1827212229 = mgr.getIntegerFormulaManager().makeNumber(1);
            var d173440626 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d442205321 = mgr.getBooleanFormulaManager().ifThenElse(d1204178174, d1827212229, d173440626);
            var d1871678080 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d1260127127 = mgr.getIntegerFormulaManager().equal(d442205321, d1871678080);
            var d1921012072 = mgr.getBooleanFormulaManager().not(d1260127127);
            var d884604029 = mgr.getBooleanFormulaManager().not(d1921012072);
            var d670153696 = mgr.getBooleanFormulaManager().and(d884604029, d713898436);
            var d215614514 = mgr.getBooleanFormulaManager().and(d1759915172, d670153696);
            var d92864491 = mgr.getIntegerFormulaManager().makeVariable("main::i@3");
            var d8136897 = mgr.getIntegerFormulaManager().makeVariable("main::i__TERMINATION_PRIMED@3");
            var d196025267 = mgr.getIntegerFormulaManager().equal(d8136897, d92864491);
            var d1743553655 = mgr.getBooleanFormulaManager().and(d713898436, d196025267);
            var d635001030 = mgr.getBooleanFormulaManager().and(d1743553655, d713898436);
            var d1149388444 = mgr.getBooleanFormulaManager().and(d1800932232, d635001030);
            var d922992444 = mgr.getIntegerFormulaManager().makeVariable("main::i@3");
            var d886004375 = mgr.getIntegerFormulaManager().makeVariable("main::i__TERMINATION_PRIMED@3");
            var d1530870688 = mgr.getIntegerFormulaManager().equal(d886004375, d922992444);
            var d232726781 = mgr.getBooleanFormulaManager().and(d713898436, d1530870688);
            var d663716901 = mgr.getBooleanFormulaManager().and(d232726781, d713898436);
            var d1767532961 = mgr.getBooleanFormulaManager().and(d215614514, d663716901);
            var d1060549703 = mgr.getIntegerFormulaManager().makeVariable("__ADDRESS_OF_main::a__TERMINATION_PRIMED@");
            var d1682157864 = mgr.getIntegerFormulaManager().makeVariable("__ADDRESS_OF_main::a@");
            var d1275011461 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d1545666472 = mgr.getIntegerFormulaManager().makeNumber(4);
            var d2146303527 = mgr.getIntegerFormulaManager().multiply(d1545666472, d1275011461);
            var d797416363 = mgr.getIntegerFormulaManager().add(d1060549703, d2146303527);
            var d491152599 = mgr.getIntegerFormulaManager().makeNumber(4);
            var d1186989416 = mgr.getIntegerFormulaManager().multiply(d491152599, d1275011461);
            var d1456265041 = mgr.getIntegerFormulaManager().add(d1682157864, d1186989416);
            var d1166361824 = mgr.getArrayFormulaManager().makeArray("*int@3", FormulaType.IntegerType, FormulaType.IntegerType);
            var d1808527451 = mgr.getArrayFormulaManager().select(d1166361824, d1456265041);
            var d761680655 = mgr.getArrayFormulaManager().makeArray("*int@3", FormulaType.IntegerType, FormulaType.IntegerType);
            var d488669101 = mgr.getArrayFormulaManager().makeArray("*int@4", FormulaType.IntegerType, FormulaType.IntegerType);
            var d1928174253 = mgr.getArrayFormulaManager().store(d761680655, d797416363, d1808527451);
            var d1183905155 = mgr.getArrayFormulaManager().equivalence(d488669101, d1928174253);
            var d1500588149 = mgr.getArrayFormulaManager().makeArray("*int@3", FormulaType.IntegerType, FormulaType.IntegerType);
            var d1202907617 = mgr.getArrayFormulaManager().makeArray("*int@4", FormulaType.IntegerType, FormulaType.IntegerType);
            var d1502882632 = mgr.getArrayFormulaManager().equivalence(d1202907617, d1500588149);
            var d409596180 = mgr.getBooleanFormulaManager().and(d713898436, d1183905155);
            var d1217089772 = mgr.getBooleanFormulaManager().not(d713898436);
            var d413550077 = mgr.getBooleanFormulaManager().and(d1217089772, d1502882632);
            var d1620112330 = mgr.getBooleanFormulaManager().or(d409596180, d413550077);
            var d933646237 = mgr.getBooleanFormulaManager().and(d713898436, d1620112330);
            var d632841653 = mgr.getIntegerFormulaManager().makeNumber(1);
            var d261838162 = mgr.getIntegerFormulaManager().makeNumber(4);
            var d1752365512 = mgr.getIntegerFormulaManager().multiply(d261838162, d632841653);
            var d1831705084 = mgr.getIntegerFormulaManager().add(d1060549703, d1752365512);
            var d199150625 = mgr.getIntegerFormulaManager().makeNumber(4);
            var d1580874189 = mgr.getIntegerFormulaManager().multiply(d199150625, d632841653);
            var d569976699 = mgr.getIntegerFormulaManager().add(d1682157864, d1580874189);
            var d538618049 = mgr.getArrayFormulaManager().makeArray("*int@4", FormulaType.IntegerType, FormulaType.IntegerType);
            var d1566099239 = mgr.getArrayFormulaManager().select(d538618049, d569976699);
            var d1386440976 = mgr.getArrayFormulaManager().makeArray("*int@4", FormulaType.IntegerType, FormulaType.IntegerType);
            var d973692608 = mgr.getArrayFormulaManager().makeArray("*int@5", FormulaType.IntegerType, FormulaType.IntegerType);
            var d1327539680 = mgr.getArrayFormulaManager().store(d1386440976, d1831705084, d1566099239);
            var d1423586012 = mgr.getArrayFormulaManager().equivalence(d973692608, d1327539680);
            var d494414526 = mgr.getArrayFormulaManager().makeArray("*int@4", FormulaType.IntegerType, FormulaType.IntegerType);
            var d1844942991 = mgr.getArrayFormulaManager().makeArray("*int@5", FormulaType.IntegerType, FormulaType.IntegerType);
            var d665988980 = mgr.getArrayFormulaManager().equivalence(d1844942991, d494414526);
            var d586917260 = mgr.getBooleanFormulaManager().and(d713898436, d1423586012);
            var d2122991287 = mgr.getBooleanFormulaManager().not(d713898436);
            var d803768841 = mgr.getBooleanFormulaManager().and(d2122991287, d665988980);
            var d420993295 = mgr.getBooleanFormulaManager().or(d586917260, d803768841);
            var d1723848804 = mgr.getBooleanFormulaManager().and(d933646237, d420993295);
            var d1252820474 = mgr.getBooleanFormulaManager().and(d713898436, d1723848804);
            var d570422884 = mgr.getBooleanFormulaManager().and(d1252820474, d713898436);
            var d101162229 = mgr.getBooleanFormulaManager().and(d1149388444, d570422884);
            var d509806761 = mgr.getIntegerFormulaManager().makeVariable("__ADDRESS_OF_main::a__TERMINATION_PRIMED@");
            var d818859466 = mgr.getIntegerFormulaManager().makeVariable("__ADDRESS_OF_main::a@");
            var d1418102907 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d1378280450 = mgr.getIntegerFormulaManager().makeNumber(4);
            var d339788561 = mgr.getIntegerFormulaManager().multiply(d1378280450, d1418102907);
            var d412835761 = mgr.getIntegerFormulaManager().add(d509806761, d339788561);
            var d2017380745 = mgr.getIntegerFormulaManager().makeNumber(4);
            var d501036152 = mgr.getIntegerFormulaManager().multiply(d2017380745, d1418102907);
            var d261567641 = mgr.getIntegerFormulaManager().add(d818859466, d501036152);
            var d1295225869 = mgr.getArrayFormulaManager().makeArray("*int@3", FormulaType.IntegerType, FormulaType.IntegerType);
            var d1137667747 = mgr.getArrayFormulaManager().select(d1295225869, d261567641);
            var d935722070 = mgr.getArrayFormulaManager().makeArray("*int@3", FormulaType.IntegerType, FormulaType.IntegerType);
            var d29369803 = mgr.getArrayFormulaManager().makeArray("*int@4", FormulaType.IntegerType, FormulaType.IntegerType);
            var d1350720002 = mgr.getArrayFormulaManager().store(d935722070, d412835761, d1137667747);
            var d1753259207 = mgr.getArrayFormulaManager().equivalence(d29369803, d1350720002);
            var d1883237069 = mgr.getArrayFormulaManager().makeArray("*int@3", FormulaType.IntegerType, FormulaType.IntegerType);
            var d1884387196 = mgr.getArrayFormulaManager().makeArray("*int@4", FormulaType.IntegerType, FormulaType.IntegerType);
            var d843149630 = mgr.getArrayFormulaManager().equivalence(d1884387196, d1883237069);
            var d1590404373 = mgr.getBooleanFormulaManager().and(d713898436, d1753259207);
            var d1361921411 = mgr.getBooleanFormulaManager().not(d713898436);
            var d716972621 = mgr.getBooleanFormulaManager().and(d1361921411, d843149630);
            var d332234405 = mgr.getBooleanFormulaManager().or(d1590404373, d716972621);
            var d271422148 = mgr.getBooleanFormulaManager().and(d713898436, d332234405);
            var d731368479 = mgr.getIntegerFormulaManager().makeNumber(1);
            var d1618099562 = mgr.getIntegerFormulaManager().makeNumber(4);
            var d405950359 = mgr.getIntegerFormulaManager().multiply(d1618099562, d731368479);
            var d1693799911 = mgr.getIntegerFormulaManager().add(d509806761, d405950359);
            var d1897368146 = mgr.getIntegerFormulaManager().makeNumber(4);
            var d16736375 = mgr.getIntegerFormulaManager().multiply(d1897368146, d731368479);
            var d180078856 = mgr.getIntegerFormulaManager().add(d818859466, d16736375);
            var d1152380885 = mgr.getArrayFormulaManager().makeArray("*int@4", FormulaType.IntegerType, FormulaType.IntegerType);
            var d161982472 = mgr.getArrayFormulaManager().select(d1152380885, d180078856);
            var d1914740115 = mgr.getArrayFormulaManager().makeArray("*int@4", FormulaType.IntegerType, FormulaType.IntegerType);
            var d646445398 = mgr.getArrayFormulaManager().makeArray("*int@5", FormulaType.IntegerType, FormulaType.IntegerType);
            var d502102804 = mgr.getArrayFormulaManager().store(d1914740115, d1693799911, d161982472);
            var d700348233 = mgr.getArrayFormulaManager().equivalence(d646445398, d502102804);
            var d1602530280 = mgr.getArrayFormulaManager().makeArray("*int@4", FormulaType.IntegerType, FormulaType.IntegerType);
            var d1179689991 = mgr.getArrayFormulaManager().makeArray("*int@5", FormulaType.IntegerType, FormulaType.IntegerType);
            var d806572546 = mgr.getArrayFormulaManager().equivalence(d1179689991, d1602530280);
            var d1783463798 = mgr.getBooleanFormulaManager().and(d713898436, d700348233);
            var d283923004 = mgr.getBooleanFormulaManager().not(d713898436);
            var d1407167674 = mgr.getBooleanFormulaManager().and(d283923004, d806572546);
            var d2037806977 = mgr.getBooleanFormulaManager().or(d1783463798, d1407167674);
            var d2017530134 = mgr.getBooleanFormulaManager().and(d271422148, d2037806977);
            var d181326224 = mgr.getBooleanFormulaManager().and(d713898436, d2017530134);
            var d609879567 = mgr.getBooleanFormulaManager().and(d181326224, d713898436);
            var d1859823482 = mgr.getBooleanFormulaManager().and(d1767532961, d609879567);
            var d1658704411 = mgr.getBooleanFormulaManager().and(d713898436, d713898436);
            var d381930033 = mgr.getBooleanFormulaManager().and(d713898436, d713898436);
            var d691096777 = mgr.getIntegerFormulaManager().makeVariable("int main();::__CPAchecker_termination_temp@3");
            var d1312348533 = mgr.getIntegerFormulaManager().makeNumber(new BigInteger("0"));
            var d905488851 = mgr.getIntegerFormulaManager().equal(d691096777, d1312348533);
            var d1223303171 = mgr.getIntegerFormulaManager().makeNumber(1);
            var d1797159635 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d1676010932 = mgr.getBooleanFormulaManager().ifThenElse(d905488851, d1223303171, d1797159635);
            var d329481770 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d173059685 = mgr.getIntegerFormulaManager().equal(d1676010932, d329481770);
            var d310412574 = mgr.getBooleanFormulaManager().not(d173059685);
            var d1585711807 = mgr.getBooleanFormulaManager().and(d310412574, d713898436);
            var d1457417579 = mgr.getBooleanFormulaManager().and(d46627301, d1585711807);
            var d1500697171 = mgr.getIntegerFormulaManager().makeVariable("int main();::__CPAchecker_termination_temp@3");
            var d1338770454 = mgr.getIntegerFormulaManager().makeNumber(new BigInteger("0"));
            var d836972194 = mgr.getIntegerFormulaManager().equal(d1500697171, d1338770454);
            var d343128256 = mgr.getIntegerFormulaManager().makeNumber(1);
            var d1532756055 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d1956598686 = mgr.getBooleanFormulaManager().ifThenElse(d836972194, d343128256, d1532756055);
            var d1554118033 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d1428022141 = mgr.getIntegerFormulaManager().equal(d1956598686, d1554118033);
            var d1861754673 = mgr.getBooleanFormulaManager().not(d1428022141);
            var d1618326227 = mgr.getBooleanFormulaManager().and(d1861754673, d713898436);
            var d866901553 = mgr.getBooleanFormulaManager().and(d1759915172, d1618326227);
            var d657998502 = mgr.getBooleanFormulaManager().and(d713898436, d713898436);
            var d1788256184 = mgr.getBooleanFormulaManager().and(d713898436, d713898436);
            var d128028301 = mgr.getBooleanFormulaManager().and(d713898436, d713898436);
            var d807986446 = mgr.getBooleanFormulaManager().and(d713898436, d713898436);
            var d766101 = mgr.getIntegerFormulaManager().makeNumber(new BigInteger("0"));
            var d2004628751 = mgr.getIntegerFormulaManager().makeVariable("main::i@3");
            var d665512315 = mgr.getIntegerFormulaManager().lessOrEquals(d766101, d2004628751);
            var d5021240 = mgr.getIntegerFormulaManager().makeNumber(1);
            var d1562249660 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d1272744797 = mgr.getBooleanFormulaManager().ifThenElse(d665512315, d5021240, d1562249660);
            var d1003307628 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d1595188851 = mgr.getIntegerFormulaManager().equal(d1272744797, d1003307628);
            var d1919555524 = mgr.getBooleanFormulaManager().not(d1595188851);
            var d1573125303 = mgr.getBooleanFormulaManager().and(d1919555524, d713898436);
            var d206310209 = mgr.getBooleanFormulaManager().and(d101162229, d1573125303);
            var d1416097444 = mgr.getIntegerFormulaManager().makeNumber(new BigInteger("0"));
            var d369333979 = mgr.getIntegerFormulaManager().makeVariable("main::i@3");
            var d2054787417 = mgr.getIntegerFormulaManager().lessOrEquals(d1416097444, d369333979);
            var d67811496 = mgr.getIntegerFormulaManager().makeNumber(1);
            var d1878225987 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d1707901480 = mgr.getBooleanFormulaManager().ifThenElse(d2054787417, d67811496, d1878225987);
            var d1393112209 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d35068320 = mgr.getIntegerFormulaManager().equal(d1707901480, d1393112209);
            var d1991386317 = mgr.getBooleanFormulaManager().not(d35068320);
            var d2012095985 = mgr.getBooleanFormulaManager().not(d1991386317);
            var d1842952737 = mgr.getBooleanFormulaManager().and(d2012095985, d713898436);
            var d1471800355 = mgr.getBooleanFormulaManager().and(d101162229, d1842952737);
            var d810169941 = mgr.getIntegerFormulaManager().makeNumber(new BigInteger("0"));
            var d915233792 = mgr.getIntegerFormulaManager().makeVariable("main::i@3");
            var d312565954 = mgr.getIntegerFormulaManager().lessOrEquals(d810169941, d915233792);
            var d178325065 = mgr.getIntegerFormulaManager().makeNumber(1);
            var d1798861270 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d923360749 = mgr.getBooleanFormulaManager().ifThenElse(d312565954, d178325065, d1798861270);
            var d783785150 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d749098095 = mgr.getIntegerFormulaManager().equal(d923360749, d783785150);
            var d70788844 = mgr.getBooleanFormulaManager().not(d749098095);
            var d2032399795 = mgr.getBooleanFormulaManager().and(d70788844, d713898436);
            var d1801704517 = mgr.getBooleanFormulaManager().and(d1859823482, d2032399795);
            var d1970856042 = mgr.getIntegerFormulaManager().makeNumber(new BigInteger("0"));
            var d817018735 = mgr.getIntegerFormulaManager().makeVariable("main::i@3");
            var d1457148583 = mgr.getIntegerFormulaManager().lessOrEquals(d1970856042, d817018735);
            var d602830277 = mgr.getIntegerFormulaManager().makeNumber(1);
            var d296204898 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d873168630 = mgr.getBooleanFormulaManager().ifThenElse(d1457148583, d602830277, d296204898);
            var d809520570 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d1615873578 = mgr.getIntegerFormulaManager().equal(d873168630, d809520570);
            var d1275626728 = mgr.getBooleanFormulaManager().not(d1615873578);
            var d589016913 = mgr.getBooleanFormulaManager().not(d1275626728);
            var d293870357 = mgr.getBooleanFormulaManager().and(d589016913, d713898436);
            var d1938259481 = mgr.getBooleanFormulaManager().and(d1859823482, d293870357);
            var d2065730373 = mgr.getIntegerFormulaManager().makeNumber(new BigInteger("0"));
            var d96453207 = mgr.getIntegerFormulaManager().makeVariable("main::i@3");
            var d877804870 = mgr.getIntegerFormulaManager().lessOrEquals(d2065730373, d96453207);
            var d2095970915 = mgr.getIntegerFormulaManager().makeNumber(1);
            var d65551384 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d2017393480 = mgr.getBooleanFormulaManager().ifThenElse(d877804870, d2095970915, d65551384);
            var d1562595588 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d1317963297 = mgr.getIntegerFormulaManager().equal(d2017393480, d1562595588);
            var d205810452 = mgr.getBooleanFormulaManager().not(d1317963297);
            var d61814127 = mgr.getBooleanFormulaManager().and(d205810452, d713898436);
            var d1145302895 = mgr.getBooleanFormulaManager().and(d1457417579, d61814127);
            var d2118571592 = mgr.getIntegerFormulaManager().makeNumber(new BigInteger("0"));
            var d1366629983 = mgr.getIntegerFormulaManager().makeVariable("main::i@3");
            var d722160979 = mgr.getIntegerFormulaManager().lessOrEquals(d2118571592, d1366629983);
            var d1885927370 = mgr.getIntegerFormulaManager().makeNumber(1);
            var d945064729 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d1101721002 = mgr.getBooleanFormulaManager().ifThenElse(d722160979, d1885927370, d945064729);
            var d809128217 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d123418227 = mgr.getIntegerFormulaManager().equal(d1101721002, d809128217);
            var d466319810 = mgr.getBooleanFormulaManager().not(d123418227);
            var d219812012 = mgr.getBooleanFormulaManager().not(d466319810);
            var d1875520143 = mgr.getBooleanFormulaManager().and(d219812012, d713898436);
            var d838627755 = mgr.getBooleanFormulaManager().and(d1457417579, d1875520143);
            var d1899567935 = mgr.getIntegerFormulaManager().makeNumber(new BigInteger("0"));
            var d754707140 = mgr.getIntegerFormulaManager().makeVariable("main::i@3");
            var d316355462 = mgr.getIntegerFormulaManager().lessOrEquals(d1899567935, d754707140);
            var d1081633119 = mgr.getIntegerFormulaManager().makeNumber(1);
            var d2040623756 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d176097974 = mgr.getBooleanFormulaManager().ifThenElse(d316355462, d1081633119, d2040623756);
            var d1106468732 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d1120072844 = mgr.getIntegerFormulaManager().equal(d176097974, d1106468732);
            var d805690186 = mgr.getBooleanFormulaManager().not(d1120072844);
            var d1113414982 = mgr.getBooleanFormulaManager().and(d805690186, d713898436);
            var d428798670 = mgr.getBooleanFormulaManager().and(d866901553, d1113414982);
            var d1287455719 = mgr.getIntegerFormulaManager().makeNumber(new BigInteger("0"));
            var d1392271025 = mgr.getIntegerFormulaManager().makeVariable("main::i@3");
            var d2053349061 = mgr.getIntegerFormulaManager().lessOrEquals(d1287455719, d1392271025);
            var d336927685 = mgr.getIntegerFormulaManager().makeNumber(1);
            var d806588571 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d2771454 = mgr.getBooleanFormulaManager().ifThenElse(d2053349061, d336927685, d806588571);
            var d1717136008 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d1521389237 = mgr.getIntegerFormulaManager().equal(d2771454, d1717136008);
            var d1989495347 = mgr.getBooleanFormulaManager().not(d1521389237);
            var d614635686 = mgr.getBooleanFormulaManager().not(d1989495347);
            var d159562640 = mgr.getBooleanFormulaManager().and(d614635686, d713898436);
            var d670517043 = mgr.getBooleanFormulaManager().and(d866901553, d159562640);
            var d253027775 = mgr.getBooleanFormulaManager().and(d713898436, d713898436);
            var d219638321 = mgr.getBooleanFormulaManager().and(d1801704517, d253027775);
            var d982634822 = mgr.getBooleanFormulaManager().and(d713898436, d713898436);
            var d1199833406 = mgr.getBooleanFormulaManager().and(d206310209, d982634822);
            var d1872047468 = mgr.getBooleanFormulaManager().or(d219638321, d1199833406);
            var d1499825229 = mgr.getBooleanFormulaManager().and(d713898436, d713898436);
            var d1833592262 = mgr.getBooleanFormulaManager().and(d1872047468, d1499825229);
            var d466577384 = mgr.getBooleanFormulaManager().and(d713898436, d713898436);
            var d1598047636 = mgr.getBooleanFormulaManager().and(d428798670, d466577384);
            var d1399398408 = mgr.getBooleanFormulaManager().and(d713898436, d713898436);
            var d2066366456 = mgr.getBooleanFormulaManager().and(d1145302895, d1399398408);
            var d465233746 = mgr.getBooleanFormulaManager().or(d1598047636, d2066366456);
            var d1175154004 = mgr.getBooleanFormulaManager().and(d713898436, d713898436);
            var d1559788797 = mgr.getBooleanFormulaManager().and(d465233746, d1175154004);
            var d978035840 = mgr.getBooleanFormulaManager().and(d713898436, d713898436);
            var d666312528 = mgr.getBooleanFormulaManager().and(d670517043, d978035840);
            var d943165647 = mgr.getBooleanFormulaManager().and(d713898436, d713898436);
            var d1956060889 = mgr.getBooleanFormulaManager().and(d838627755, d943165647);
            var d320850799 = mgr.getBooleanFormulaManager().or(d666312528, d1956060889);
            var d214768579 = mgr.getBooleanFormulaManager().and(d713898436, d713898436);
            var d142103421 = mgr.getBooleanFormulaManager().and(d320850799, d214768579);
            var d1292570580 = mgr.getIntegerFormulaManager().makeVariable("main::i@3");
            var d128077491 = mgr.getIntegerFormulaManager().makeNumber(new BigInteger("2"));
            var d1815592231 = mgr.getIntegerFormulaManager().lessThan(d1292570580, d128077491);
            var d634638280 = mgr.getIntegerFormulaManager().makeNumber(1);
            var d808653065 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d628164202 = mgr.getBooleanFormulaManager().ifThenElse(d1815592231, d634638280, d808653065);
            var d1962826086 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d1340634558 = mgr.getIntegerFormulaManager().equal(d628164202, d1962826086);
            var d1736150547 = mgr.getBooleanFormulaManager().not(d1340634558);
            var d1251247808 = mgr.getBooleanFormulaManager().and(d1736150547, d713898436);
            var d1277678493 = mgr.getBooleanFormulaManager().and(d1833592262, d1251247808);
            var d2078154554 = mgr.getIntegerFormulaManager().makeVariable("main::i@3");
            var d361903111 = mgr.getIntegerFormulaManager().makeNumber(new BigInteger("2"));
            var d1742448147 = mgr.getIntegerFormulaManager().lessThan(d2078154554, d361903111);
            var d1465126864 = mgr.getIntegerFormulaManager().makeNumber(1);
            var d1559817679 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d1489946715 = mgr.getBooleanFormulaManager().ifThenElse(d1742448147, d1465126864, d1559817679);
            var d1654589039 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d356691811 = mgr.getIntegerFormulaManager().equal(d1489946715, d1654589039);
            var d248495761 = mgr.getBooleanFormulaManager().not(d356691811);
            var d552416003 = mgr.getBooleanFormulaManager().not(d248495761);
            var d987489551 = mgr.getBooleanFormulaManager().and(d552416003, d713898436);
            var d979532928 = mgr.getBooleanFormulaManager().and(d1833592262, d987489551);
            var d1694519286 = mgr.getIntegerFormulaManager().makeVariable("main::i@3");
            var d1286580650 = mgr.getIntegerFormulaManager().makeNumber(new BigInteger("2"));
            var d1445758842 = mgr.getIntegerFormulaManager().lessThan(d1694519286, d1286580650);
            var d1728057672 = mgr.getIntegerFormulaManager().makeNumber(1);
            var d10001825 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d835426017 = mgr.getBooleanFormulaManager().ifThenElse(d1445758842, d1728057672, d10001825);
            var d65982709 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d1677921169 = mgr.getIntegerFormulaManager().equal(d835426017, d65982709);
            var d540206885 = mgr.getBooleanFormulaManager().not(d1677921169);
            var d1294139740 = mgr.getBooleanFormulaManager().and(d540206885, d713898436);
            var d943659381 = mgr.getBooleanFormulaManager().and(d1559788797, d1294139740);
            var d1142735456 = mgr.getIntegerFormulaManager().makeVariable("main::i@3");
            var d1939869193 = mgr.getIntegerFormulaManager().makeNumber(new BigInteger("2"));
            var d652007616 = mgr.getIntegerFormulaManager().lessThan(d1142735456, d1939869193);
            var d1726515679 = mgr.getIntegerFormulaManager().makeNumber(1);
            var d1145391264 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d929482343 = mgr.getBooleanFormulaManager().ifThenElse(d652007616, d1726515679, d1145391264);
            var d2000421523 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d1438178266 = mgr.getIntegerFormulaManager().equal(d929482343, d2000421523);
            var d995531141 = mgr.getBooleanFormulaManager().not(d1438178266);
            var d973219190 = mgr.getBooleanFormulaManager().not(d995531141);
            var d767393855 = mgr.getBooleanFormulaManager().and(d973219190, d713898436);
            var d1044965465 = mgr.getBooleanFormulaManager().and(d1559788797, d767393855);
            var d442465916 = mgr.getBooleanFormulaManager().and(d713898436, d713898436);
            var d1529002352 = mgr.getBooleanFormulaManager().and(d1044965465, d442465916);
            var d584157293 = mgr.getBooleanFormulaManager().and(d713898436, d713898436);
            var d2113273959 = mgr.getBooleanFormulaManager().and(d142103421, d584157293);
            var d482032955 = mgr.getBooleanFormulaManager().or(d1529002352, d2113273959);
            var d1386020581 = mgr.getBooleanFormulaManager().and(d713898436, d713898436);
            var d2090894907 = mgr.getBooleanFormulaManager().and(d482032955, d1386020581);
            var d1095849663 = mgr.getIntegerFormulaManager().makeVariable("__ADDRESS_OF_main::a@");
            var d960004592 = mgr.getIntegerFormulaManager().makeVariable("main::i@3");
            var d1257532915 = mgr.getIntegerFormulaManager().makeNumber(4);
            var d1096343229 = mgr.getIntegerFormulaManager().multiply(d1257532915, d960004592);
            var d183995527 = mgr.getIntegerFormulaManager().add(d1095849663, d1096343229);
            var d2000530216 = mgr.getArrayFormulaManager().makeArray("*int@5", FormulaType.IntegerType, FormulaType.IntegerType);
            var d516934601 = mgr.getArrayFormulaManager().select(d2000530216, d183995527);
            var d426070939 = mgr.getIntegerFormulaManager().makeNumber(new BigInteger("0"));
            var d801142660 = mgr.getIntegerFormulaManager().greaterOrEquals(d516934601, d426070939);
            var d893320639 = mgr.getIntegerFormulaManager().makeNumber(1);
            var d1439693138 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d1711641083 = mgr.getBooleanFormulaManager().ifThenElse(d801142660, d893320639, d1439693138);
            var d1247127272 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d147089688 = mgr.getIntegerFormulaManager().equal(d1711641083, d1247127272);
            var d577442875 = mgr.getBooleanFormulaManager().not(d147089688);
            var d1747702724 = mgr.getBooleanFormulaManager().and(d577442875, d713898436);
            var d254692047 = mgr.getBooleanFormulaManager().and(d1277678493, d1747702724);
            var d1589214445 = mgr.getIntegerFormulaManager().makeVariable("__ADDRESS_OF_main::a@");
            var d1757032717 = mgr.getIntegerFormulaManager().makeVariable("main::i@3");
            var d356476647 = mgr.getIntegerFormulaManager().makeNumber(4);
            var d2058174333 = mgr.getIntegerFormulaManager().multiply(d356476647, d1757032717);
            var d1868987089 = mgr.getIntegerFormulaManager().add(d1589214445, d2058174333);
            var d1449987177 = mgr.getArrayFormulaManager().makeArray("*int@5", FormulaType.IntegerType, FormulaType.IntegerType);
            var d948650013 = mgr.getArrayFormulaManager().select(d1449987177, d1868987089);
            var d734971558 = mgr.getIntegerFormulaManager().makeNumber(new BigInteger("0"));
            var d2007138812 = mgr.getIntegerFormulaManager().greaterOrEquals(d948650013, d734971558);
            var d1225970981 = mgr.getIntegerFormulaManager().makeNumber(1);
            var d737935282 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d1985869725 = mgr.getBooleanFormulaManager().ifThenElse(d2007138812, d1225970981, d737935282);
            var d353580491 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d1249337777 = mgr.getIntegerFormulaManager().equal(d1985869725, d353580491);
            var d1048903970 = mgr.getBooleanFormulaManager().not(d1249337777);
            var d670951536 = mgr.getBooleanFormulaManager().not(d1048903970);
            var d726416425 = mgr.getBooleanFormulaManager().and(d670951536, d713898436);
            var d1523034648 = mgr.getBooleanFormulaManager().and(d1277678493, d726416425);
            var d1313618488 = mgr.getIntegerFormulaManager().makeVariable("__ADDRESS_OF_main::a@");
            var d691854979 = mgr.getIntegerFormulaManager().makeVariable("main::i@3");
            var d203936099 = mgr.getIntegerFormulaManager().makeNumber(4);
            var d1472759652 = mgr.getIntegerFormulaManager().multiply(d203936099, d691854979);
            var d2029709919 = mgr.getIntegerFormulaManager().add(d1313618488, d1472759652);
            var d939391749 = mgr.getArrayFormulaManager().makeArray("*int@3", FormulaType.IntegerType, FormulaType.IntegerType);
            var d98801744 = mgr.getArrayFormulaManager().select(d939391749, d2029709919);
            var d369351727 = mgr.getIntegerFormulaManager().makeNumber(new BigInteger("0"));
            var d964981922 = mgr.getIntegerFormulaManager().greaterOrEquals(d98801744, d369351727);
            var d1635358020 = mgr.getIntegerFormulaManager().makeNumber(1);
            var d2025955363 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d1890318768 = mgr.getBooleanFormulaManager().ifThenElse(d964981922, d1635358020, d2025955363);
            var d1779479139 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d1198442960 = mgr.getIntegerFormulaManager().equal(d1890318768, d1779479139);
            var d844872102 = mgr.getBooleanFormulaManager().not(d1198442960);
            var d487764004 = mgr.getBooleanFormulaManager().and(d844872102, d713898436);
            var d1929284175 = mgr.getBooleanFormulaManager().and(d943659381, d487764004);
            var d1139801481 = mgr.getIntegerFormulaManager().makeVariable("__ADDRESS_OF_main::a@");
            var d739703515 = mgr.getIntegerFormulaManager().makeVariable("main::i@3");
            var d613281005 = mgr.getIntegerFormulaManager().makeNumber(4);
            var d573023937 = mgr.getIntegerFormulaManager().multiply(d613281005, d739703515);
            var d513279161 = mgr.getIntegerFormulaManager().add(d1139801481, d573023937);
            var d88335763 = mgr.getArrayFormulaManager().makeArray("*int@3", FormulaType.IntegerType, FormulaType.IntegerType);
            var d1315081042 = mgr.getArrayFormulaManager().select(d88335763, d513279161);
            var d1374432753 = mgr.getIntegerFormulaManager().makeNumber(new BigInteger("0"));
            var d261052089 = mgr.getIntegerFormulaManager().greaterOrEquals(d1315081042, d1374432753);
            var d368727462 = mgr.getIntegerFormulaManager().makeNumber(1);
            var d1326998608 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d2141932519 = mgr.getBooleanFormulaManager().ifThenElse(d261052089, d368727462, d1326998608);
            var d174383157 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d1299497914 = mgr.getIntegerFormulaManager().equal(d2141932519, d174383157);
            var d1103234208 = mgr.getBooleanFormulaManager().not(d1299497914);
            var d1679002380 = mgr.getBooleanFormulaManager().not(d1103234208);
            var d1239132915 = mgr.getBooleanFormulaManager().and(d1679002380, d713898436);
            var d584698209 = mgr.getBooleanFormulaManager().and(d943659381, d1239132915);
            var d199000084 = mgr.getBooleanFormulaManager().and(d713898436, d713898436);
            var d524566446 = mgr.getBooleanFormulaManager().and(d584698209, d199000084);
            var d1941598182 = mgr.getBooleanFormulaManager().and(d713898436, d713898436);
            var d2041263297 = mgr.getBooleanFormulaManager().and(d2090894907, d1941598182);
            var d379115456 = mgr.getBooleanFormulaManager().or(d524566446, d2041263297);
            var d673129458 = mgr.getBooleanFormulaManager().and(d713898436, d713898436);
            var d142261320 = mgr.getBooleanFormulaManager().and(d379115456, d673129458);
            var d1949672824 = mgr.getIntegerFormulaManager().makeNumber(new BigInteger("0"));
            var d1620301064 = mgr.getIntegerFormulaManager().makeVariable("main::__retval__@2");
            var d319061373 = mgr.getIntegerFormulaManager().equal(d1620301064, d1949672824);
            var d1014824123 = mgr.getBooleanFormulaManager().and(d713898436, d319061373);
            var d1706790953 = mgr.getIntegerFormulaManager().makeNumber(4);
            var d469643779 = mgr.getBooleanFormulaManager().and(d1014824123, d713898436);
            var d723602324 = mgr.getBooleanFormulaManager().and(d142261320, d469643779);
            var d45666436 = mgr.getIntegerFormulaManager().makeVariable("__ADDRESS_OF_main::a@");
            var d1840194359 = mgr.getIntegerFormulaManager().makeVariable("main::i@3");
            var d620412175 = mgr.getIntegerFormulaManager().makeNumber(4);
            var d621486957 = mgr.getIntegerFormulaManager().multiply(d620412175, d1840194359);
            var d1643379640 = mgr.getIntegerFormulaManager().add(d45666436, d621486957);
            var d1968298538 = mgr.getIntegerFormulaManager().makeNumber(new BigInteger("0"));
            var d70386506 = mgr.getArrayFormulaManager().makeArray("*int@5", FormulaType.IntegerType, FormulaType.IntegerType);
            var d2027837674 = mgr.getArrayFormulaManager().makeArray("*int@6", FormulaType.IntegerType, FormulaType.IntegerType);
            var d101601906 = mgr.getArrayFormulaManager().store(d70386506, d1643379640, d1968298538);
            var d2104842259 = mgr.getArrayFormulaManager().equivalence(d2027837674, d101601906);
            var d1774795940 = mgr.getArrayFormulaManager().makeArray("*int@5", FormulaType.IntegerType, FormulaType.IntegerType);
            var d1675239551 = mgr.getArrayFormulaManager().makeArray("*int@6", FormulaType.IntegerType, FormulaType.IntegerType);
            var d389247924 = mgr.getArrayFormulaManager().equivalence(d1675239551, d1774795940);
            var d1087440001 = mgr.getBooleanFormulaManager().and(d713898436, d2104842259);
            var d1625111587 = mgr.getBooleanFormulaManager().not(d713898436);
            var d1387671967 = mgr.getBooleanFormulaManager().and(d1625111587, d389247924);
            var d1586779822 = mgr.getBooleanFormulaManager().or(d1087440001, d1387671967);
            var d380216561 = mgr.getBooleanFormulaManager().and(d713898436, d1586779822);
            var d521973283 = mgr.getBooleanFormulaManager().and(d380216561, d713898436);
            var d2084920982 = mgr.getBooleanFormulaManager().and(d254692047, d521973283);
            var d1540219992 = mgr.getIntegerFormulaManager().makeVariable("__VERIFIER_nondet_int!6@");
            var d559559860 = mgr.getIntegerFormulaManager().makeVariable("main::i@4");
            var d2008907751 = mgr.getIntegerFormulaManager().equal(d559559860, d1540219992);
            var d903064416 = mgr.getBooleanFormulaManager().and(d713898436, d2008907751);
            var d17331878 = mgr.getBooleanFormulaManager().and(d903064416, d713898436);
            var d1904676263 = mgr.getBooleanFormulaManager().and(d2084920982, d17331878);
            var d117885704 = mgr.getIntegerFormulaManager().makeVariable("__ADDRESS_OF_main::a@");
            var d1311052922 = mgr.getIntegerFormulaManager().makeVariable("main::i@3");
            var d1802029863 = mgr.getIntegerFormulaManager().makeNumber(4);
            var d1734343965 = mgr.getIntegerFormulaManager().multiply(d1802029863, d1311052922);
            var d1445999733 = mgr.getIntegerFormulaManager().add(d117885704, d1734343965);
            var d810576909 = mgr.getIntegerFormulaManager().makeNumber(new BigInteger("0"));
            var d499951827 = mgr.getArrayFormulaManager().makeArray("*int@3", FormulaType.IntegerType, FormulaType.IntegerType);
            var d90380642 = mgr.getArrayFormulaManager().makeArray("*int@4", FormulaType.IntegerType, FormulaType.IntegerType);
            var d1386677799 = mgr.getArrayFormulaManager().store(d499951827, d1445999733, d810576909);
            var d1629759610 = mgr.getArrayFormulaManager().equivalence(d90380642, d1386677799);
            var d425107133 = mgr.getArrayFormulaManager().makeArray("*int@3", FormulaType.IntegerType, FormulaType.IntegerType);
            var d73608444 = mgr.getArrayFormulaManager().makeArray("*int@4", FormulaType.IntegerType, FormulaType.IntegerType);
            var d1847559273 = mgr.getArrayFormulaManager().equivalence(d73608444, d425107133);
            var d775423528 = mgr.getBooleanFormulaManager().and(d713898436, d1629759610);
            var d62309924 = mgr.getBooleanFormulaManager().not(d713898436);
            var d514793058 = mgr.getBooleanFormulaManager().and(d62309924, d1847559273);
            var d209845522 = mgr.getBooleanFormulaManager().or(d775423528, d514793058);
            var d1659282412 = mgr.getBooleanFormulaManager().and(d713898436, d209845522);
            var d1465179762 = mgr.getBooleanFormulaManager().and(d1659282412, d713898436);
            var d837719796 = mgr.getBooleanFormulaManager().and(d1929284175, d1465179762);
            var d839161014 = mgr.getIntegerFormulaManager().makeVariable("__VERIFIER_nondet_int!6@");
            var d1697298649 = mgr.getIntegerFormulaManager().makeVariable("main::i@4");
            var d352083264 = mgr.getIntegerFormulaManager().equal(d1697298649, d839161014);
            var d1373646877 = mgr.getBooleanFormulaManager().and(d713898436, d352083264);
            var d1205321651 = mgr.getBooleanFormulaManager().and(d1373646877, d713898436);
            var d1997224928 = mgr.getBooleanFormulaManager().and(d837719796, d1205321651);
            var d730583371 = mgr.getBooleanFormulaManager().and(d713898436, d713898436);
            var d99695585 = mgr.getBooleanFormulaManager().and(d713898436, d1904676263);
            var d696591495 = mgr.getIntegerFormulaManager().makeNumber(new BigInteger("0"));
            var d1998434604 = mgr.getIntegerFormulaManager().makeNumber(new BigInteger("1"));
            var d989520513 = mgr.getIntegerFormulaManager().equal(d696591495, d1998434604);
            var d648972298 = mgr.getIntegerFormulaManager().makeNumber(1);
            var d638525764 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d1006727288 = mgr.getBooleanFormulaManager().ifThenElse(d989520513, d648972298, d638525764);
            var d1367503763 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d62803825 = mgr.getIntegerFormulaManager().equal(d1006727288, d1367503763);
            var d1550080835 = mgr.getBooleanFormulaManager().not(d62803825);
            var d1808884231 = mgr.getBooleanFormulaManager().not(d1550080835);
            var d697145861 = mgr.getBooleanFormulaManager().and(d1808884231, d713898436);
            var d1188623367 = mgr.getBooleanFormulaManager().and(d713898436, d713898436);
            var d408909888 = mgr.getBooleanFormulaManager().and(d713898436, d713898436);
            var d2122256138 = mgr.getIntegerFormulaManager().makeNumber(new BigInteger("0"));
            var d2126876651 = mgr.getIntegerFormulaManager().makeNumber(new BigInteger("1"));
            var d498820363 = mgr.getIntegerFormulaManager().equal(d2122256138, d2126876651);
            var d1701646500 = mgr.getIntegerFormulaManager().makeNumber(1);
            var d1676428380 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d822359325 = mgr.getBooleanFormulaManager().ifThenElse(d498820363, d1701646500, d1676428380);
            var d2010221835 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d2050247525 = mgr.getIntegerFormulaManager().equal(d822359325, d2010221835);
            var d2071674587 = mgr.getBooleanFormulaManager().not(d2050247525);
            var d1799831668 = mgr.getBooleanFormulaManager().and(d2071674587, d713898436);
            var d277164482 = mgr.getBooleanFormulaManager().and(d713898436, d1799831668);
            var d990442552 = mgr.getIntegerFormulaManager().makeNumber(4);
            var d45795770 = mgr.getBooleanFormulaManager().and(d713898436, d713898436);
            var d1529842358 = mgr.getBooleanFormulaManager().and(d45795770, d713898436);
            var d1541232265 = mgr.getBooleanFormulaManager().and(d713898436, d1529842358);
            var d663277822 = mgr.getIntegerFormulaManager().makeNumber(4);
            var d1940601516 = mgr.getBooleanFormulaManager().and(d713898436, d713898436);
            var d1425433685 = mgr.getBooleanFormulaManager().and(d1940601516, d713898436);
            var d1705904476 = mgr.getBooleanFormulaManager().and(d277164482, d1425433685);
            var d1235686146 = mgr.getIntegerFormulaManager().makeVariable("__VERIFIER_nondet_int!7@");
            var d1557534595 = mgr.getIntegerFormulaManager().makeVariable("int main();::__CPAchecker_termination_temp@5");
            var d1497538476 = mgr.getIntegerFormulaManager().equal(d1557534595, d1235686146);
            var d1470772251 = mgr.getBooleanFormulaManager().and(d713898436, d1497538476);
            var d652481263 = mgr.getBooleanFormulaManager().and(d1470772251, d713898436);
            var d1256350655 = mgr.getBooleanFormulaManager().and(d1541232265, d652481263);
            var d118504112 = mgr.getIntegerFormulaManager().makeVariable("__VERIFIER_nondet_int!7@");
            var d27053221 = mgr.getIntegerFormulaManager().makeVariable("int main();::__CPAchecker_termination_temp@5");
            var d124376339 = mgr.getIntegerFormulaManager().equal(d27053221, d118504112);
            var d1582277082 = mgr.getBooleanFormulaManager().and(d713898436, d124376339);
            var d1485624601 = mgr.getBooleanFormulaManager().and(d1582277082, d713898436);
            var d1066582857 = mgr.getBooleanFormulaManager().and(d1705904476, d1485624601);
            var d1111710616 = mgr.getIntegerFormulaManager().makeVariable("int main();::__CPAchecker_termination_temp@5");
            var d1723498053 = mgr.getIntegerFormulaManager().makeNumber(new BigInteger("0"));
            var d1893736577 = mgr.getIntegerFormulaManager().equal(d1111710616, d1723498053);
            var d164757726 = mgr.getIntegerFormulaManager().makeNumber(1);
            var d1360332263 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d1684541910 = mgr.getBooleanFormulaManager().ifThenElse(d1893736577, d164757726, d1360332263);
            var d368955890 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d212924259 = mgr.getIntegerFormulaManager().equal(d1684541910, d368955890);
            var d1970528559 = mgr.getBooleanFormulaManager().not(d212924259);
            var d1370597622 = mgr.getBooleanFormulaManager().and(d1970528559, d713898436);
            var d708350323 = mgr.getBooleanFormulaManager().and(d1256350655, d1370597622);
            var d557342904 = mgr.getIntegerFormulaManager().makeVariable("int main();::__CPAchecker_termination_temp@5");
            var d1269339945 = mgr.getIntegerFormulaManager().makeNumber(new BigInteger("0"));
            var d394424498 = mgr.getIntegerFormulaManager().equal(d557342904, d1269339945);
            var d2036324408 = mgr.getIntegerFormulaManager().makeNumber(1);
            var d453007883 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d337545117 = mgr.getBooleanFormulaManager().ifThenElse(d394424498, d2036324408, d453007883);
            var d278753868 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d386201215 = mgr.getIntegerFormulaManager().equal(d337545117, d278753868);
            var d239937174 = mgr.getBooleanFormulaManager().not(d386201215);
            var d1846508205 = mgr.getBooleanFormulaManager().and(d239937174, d713898436);
            var d368802354 = mgr.getBooleanFormulaManager().and(d1066582857, d1846508205);
            var d1122118227 = mgr.getBooleanFormulaManager().and(d713898436, d713898436);
            var d1471019696 = mgr.getBooleanFormulaManager().and(d713898436, d713898436);
            var d424226973 = mgr.getIntegerFormulaManager().makeNumber(new BigInteger("0"));
            var d1526296937 = mgr.getIntegerFormulaManager().makeVariable("main::i@4");
            var d161118423 = mgr.getIntegerFormulaManager().lessOrEquals(d424226973, d1526296937);
            var d836397870 = mgr.getIntegerFormulaManager().makeNumber(1);
            var d1640458320 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d1881419576 = mgr.getBooleanFormulaManager().ifThenElse(d161118423, d836397870, d1640458320);
            var d706915627 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d1220747354 = mgr.getIntegerFormulaManager().equal(d1881419576, d706915627);
            var d303846650 = mgr.getBooleanFormulaManager().not(d1220747354);
            var d1133573230 = mgr.getBooleanFormulaManager().and(d303846650, d713898436);
            var d2086945474 = mgr.getBooleanFormulaManager().and(d708350323, d1133573230);
            var d762604772 = mgr.getIntegerFormulaManager().makeNumber(new BigInteger("0"));
            var d1572820532 = mgr.getIntegerFormulaManager().makeVariable("main::i@4");
            var d424209001 = mgr.getIntegerFormulaManager().lessOrEquals(d762604772, d1572820532);
            var d1206180304 = mgr.getIntegerFormulaManager().makeNumber(1);
            var d1232703108 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d1859153769 = mgr.getBooleanFormulaManager().ifThenElse(d424209001, d1206180304, d1232703108);
            var d806738808 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d1365163763 = mgr.getIntegerFormulaManager().equal(d1859153769, d806738808);
            var d1414924274 = mgr.getBooleanFormulaManager().not(d1365163763);
            var d957387062 = mgr.getBooleanFormulaManager().not(d1414924274);
            var d666911607 = mgr.getBooleanFormulaManager().and(d957387062, d713898436);
            var d55429210 = mgr.getBooleanFormulaManager().and(d708350323, d666911607);
            var d1732261462 = mgr.getIntegerFormulaManager().makeNumber(new BigInteger("0"));
            var d1516536489 = mgr.getIntegerFormulaManager().makeVariable("main::i@4");
            var d2140846441 = mgr.getIntegerFormulaManager().lessOrEquals(d1732261462, d1516536489);
            var d318288344 = mgr.getIntegerFormulaManager().makeNumber(1);
            var d1953290071 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d182678201 = mgr.getBooleanFormulaManager().ifThenElse(d2140846441, d318288344, d1953290071);
            var d546886525 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d2008666311 = mgr.getIntegerFormulaManager().equal(d182678201, d546886525);
            var d1711105800 = mgr.getBooleanFormulaManager().not(d2008666311);
            var d1956296628 = mgr.getBooleanFormulaManager().and(d1711105800, d713898436);
            var d310350177 = mgr.getBooleanFormulaManager().and(d368802354, d1956296628);
            var d737756161 = mgr.getIntegerFormulaManager().makeNumber(new BigInteger("0"));
            var d624079697 = mgr.getIntegerFormulaManager().makeVariable("main::i@4");
            var d70555476 = mgr.getIntegerFormulaManager().lessOrEquals(d737756161, d624079697);
            var d1781459498 = mgr.getIntegerFormulaManager().makeNumber(1);
            var d194408994 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d990830650 = mgr.getBooleanFormulaManager().ifThenElse(d70555476, d1781459498, d194408994);
            var d463494712 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d113416412 = mgr.getIntegerFormulaManager().equal(d990830650, d463494712);
            var d1048444228 = mgr.getBooleanFormulaManager().not(d113416412);
            var d1916720513 = mgr.getBooleanFormulaManager().not(d1048444228);
            var d1802896480 = mgr.getBooleanFormulaManager().and(d1916720513, d713898436);
            var d2036360618 = mgr.getBooleanFormulaManager().and(d368802354, d1802896480);
            var d997918120 = mgr.getBooleanFormulaManager().and(d713898436, d713898436);
            var d1027006452 = mgr.getBooleanFormulaManager().and(d310350177, d997918120);
            var d2059282367 = mgr.getBooleanFormulaManager().and(d713898436, d713898436);
            var d1536478396 = mgr.getBooleanFormulaManager().and(d2086945474, d2059282367);
            var d950125603 = mgr.getBooleanFormulaManager().or(d1027006452, d1536478396);
            var d862152124 = mgr.getBooleanFormulaManager().and(d713898436, d713898436);
            var d954937264 = mgr.getBooleanFormulaManager().and(d950125603, d862152124);
            var d1934729582 = mgr.getBooleanFormulaManager().and(d713898436, d713898436);
            try (ProverEnvironment prover = context.newProverEnvironment(SolverContext.ProverOptions.GENERATE_MODELS)) {
                prover.push();
                prover.addConstraint(d1665308978);
                prover.push();
                prover.addConstraint(d1904676263);
                prover.push();
                prover.addConstraint(d713898436);

                if (!prover.isUnsat()) {
                    System.out.println(prover.getModel());
                }
            }
            var d1441577726 = mgr.getBooleanFormulaManager().and(d713898436, d713898436);
            var d1519100796 = mgr.getIntegerFormulaManager().makeNumber(new BigInteger("0"));
            var d935520971 = mgr.getIntegerFormulaManager().makeVariable("main::i@3");
            var d36883680 = mgr.getIntegerFormulaManager().lessOrEquals(d1519100796, d935520971);
            var d851033362 = mgr.getIntegerFormulaManager().makeNumber(1);
            var d892237946 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d362432678 = mgr.getBooleanFormulaManager().ifThenElse(d36883680, d851033362, d892237946);
            var d22790969 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d2121645869 = mgr.getIntegerFormulaManager().equal(d362432678, d22790969);
            var d945747249 = mgr.getBooleanFormulaManager().not(d2121645869);
            var d2143700452 = mgr.getBooleanFormulaManager().and(d945747249, d713898436);
            var d542839598 = mgr.getBooleanFormulaManager().and(d1495257933, d2143700452);
            var d1929661663 = mgr.getIntegerFormulaManager().makeVariable("main::i@3");
            var d1019009267 = mgr.getIntegerFormulaManager().makeNumber(new BigInteger("2"));
            var d1905804261 = mgr.getIntegerFormulaManager().lessThan(d1929661663, d1019009267);
            var d161672347 = mgr.getIntegerFormulaManager().makeNumber(1);
            var d1477520324 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d36707189 = mgr.getBooleanFormulaManager().ifThenElse(d1905804261, d161672347, d1477520324);
            var d822409149 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d794563378 = mgr.getIntegerFormulaManager().equal(d36707189, d822409149);
            var d2126664214 = mgr.getBooleanFormulaManager().not(d794563378);
            var d2091586824 = mgr.getBooleanFormulaManager().and(d2126664214, d713898436);
            var d1787083839 = mgr.getBooleanFormulaManager().and(d542839598, d2091586824);
            var d630122462 = mgr.getIntegerFormulaManager().makeVariable("__ADDRESS_OF_main::a@");
            var d1227903899 = mgr.getIntegerFormulaManager().makeVariable("main::i@3");
            var d1830231264 = mgr.getIntegerFormulaManager().makeNumber(4);
            var d582819897 = mgr.getIntegerFormulaManager().multiply(d1830231264, d1227903899);
            var d1885307815 = mgr.getIntegerFormulaManager().add(d630122462, d582819897);
            var d1001958076 = mgr.getArrayFormulaManager().makeArray("*int@3", FormulaType.IntegerType, FormulaType.IntegerType);
            var d1847410999 = mgr.getArrayFormulaManager().select(d1001958076, d1885307815);
            var d627709989 = mgr.getIntegerFormulaManager().makeNumber(new BigInteger("0"));
            var d698676628 = mgr.getIntegerFormulaManager().greaterOrEquals(d1847410999, d627709989);
            var d1471633238 = mgr.getIntegerFormulaManager().makeNumber(1);
            var d1395105902 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d645476639 = mgr.getBooleanFormulaManager().ifThenElse(d698676628, d1471633238, d1395105902);
            var d679442449 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d1159694255 = mgr.getIntegerFormulaManager().equal(d645476639, d679442449);
            var d727018418 = mgr.getBooleanFormulaManager().not(d1159694255);
            var d1154172430 = mgr.getBooleanFormulaManager().and(d727018418, d713898436);
            var d388436342 = mgr.getBooleanFormulaManager().and(d1787083839, d1154172430);
            var d775741122 = mgr.getIntegerFormulaManager().makeVariable("__ADDRESS_OF_main::a@");
            var d775174220 = mgr.getIntegerFormulaManager().makeVariable("main::i@3");
            var d810672306 = mgr.getIntegerFormulaManager().makeNumber(4);
            var d525527919 = mgr.getIntegerFormulaManager().multiply(d810672306, d775174220);
            var d1473313929 = mgr.getIntegerFormulaManager().add(d775741122, d525527919);
            var d1479100519 = mgr.getIntegerFormulaManager().makeNumber(new BigInteger("0"));
            var d1740797856 = mgr.getArrayFormulaManager().makeArray("*int@3", FormulaType.IntegerType, FormulaType.IntegerType);
            var d1875108260 = mgr.getArrayFormulaManager().makeArray("*int@4", FormulaType.IntegerType, FormulaType.IntegerType);
            var d1067936865 = mgr.getArrayFormulaManager().store(d1740797856, d1473313929, d1479100519);
            var d761229698 = mgr.getArrayFormulaManager().equivalence(d1875108260, d1067936865);
            var d1498705150 = mgr.getArrayFormulaManager().makeArray("*int@3", FormulaType.IntegerType, FormulaType.IntegerType);
            var d703232177 = mgr.getArrayFormulaManager().makeArray("*int@4", FormulaType.IntegerType, FormulaType.IntegerType);
            var d757779849 = mgr.getArrayFormulaManager().equivalence(d703232177, d1498705150);
            var d2075093711 = mgr.getBooleanFormulaManager().and(d713898436, d761229698);
            var d31906520 = mgr.getBooleanFormulaManager().not(d713898436);
            var d2066945445 = mgr.getBooleanFormulaManager().and(d31906520, d757779849);
            var d9361871 = mgr.getBooleanFormulaManager().or(d2075093711, d2066945445);
            var d16196099 = mgr.getBooleanFormulaManager().and(d713898436, d9361871);
            var d930089183 = mgr.getBooleanFormulaManager().and(d16196099, d713898436);
            var d1410186665 = mgr.getBooleanFormulaManager().and(d388436342, d930089183);
            var d582702662 = mgr.getIntegerFormulaManager().makeVariable("__VERIFIER_nondet_int!5@");
            var d468033320 = mgr.getIntegerFormulaManager().makeVariable("main::i@4");
            var d753162875 = mgr.getIntegerFormulaManager().equal(d468033320, d582702662);
            var d356338363 = mgr.getBooleanFormulaManager().and(d713898436, d753162875);
            var d1833707324 = mgr.getBooleanFormulaManager().and(d356338363, d713898436);
            var d1516759394 = mgr.getBooleanFormulaManager().and(d1410186665, d1833707324);
            var d1415469015 = mgr.getBooleanFormulaManager().and(d713898436, d713898436);
            var d665846007 = mgr.getIntegerFormulaManager().makeNumber(new BigInteger("0"));
            var d1123664282 = mgr.getIntegerFormulaManager().makeNumber(new BigInteger("1"));
            var d1690294013 = mgr.getIntegerFormulaManager().equal(d665846007, d1123664282);
            var d44771088 = mgr.getIntegerFormulaManager().makeNumber(1);
            var d624637962 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d700631078 = mgr.getBooleanFormulaManager().ifThenElse(d1690294013, d44771088, d624637962);
            var d860941277 = mgr.getIntegerFormulaManager().makeNumber(0);
            var d1746458880 = mgr.getIntegerFormulaManager().equal(d700631078, d860941277);
            var d345986913 = mgr.getBooleanFormulaManager().not(d1746458880);
            var d732118572 = mgr.getBooleanFormulaManager().not(d345986913);
            var d521746054 = mgr.getBooleanFormulaManager().and(d732118572, d713898436);

            try (ProverEnvironment prover = context.newProverEnvironment(SolverContext.ProverOptions.GENERATE_MODELS)) {
                prover.push();
                prover.addConstraint(d1516759394);

                if (!prover.isUnsat()) {
                    System.out.println(prover.getModel());
                }
            }
        }
    }
}

The code was auto-generated by tracing all calls to the JavaSMT API with a new delegate. I'll try to reduce the example further and will then translate it to the MathSAT API

[baierd]

Good work!

Maybe you want to open a MR to add this debug delegate? ;D Seems helpful.