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