NoSuchElementException for MathSAT5 Model Despite Its Iterator Claiming That There Should Be an Element

[baierd]

MathSAT5 throws a NoSuchElementException in the model in the following CPAchecker run --symbolicExecution --stats --spec test/programs/benchmarks/properties/unreach-call.prp --32 --no-output-files test/programs/benchmarks/hardness-nfm22/hardness_fillercode_fillercodesize_ps-cn-25_file-4.i in this branch/MR latest state. This looks like a bug, either from us or MathSAT5. We should investigate and either fix this, or tell the MathSAT5 devs about it.

Stacktrace (excerpt):

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

(= |var_1_35#45@1| #b00000000)
(= |var_1_35#45@1| #b00000010)
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.cpa.constraints.domain.ConstraintsSolver.handleSolverResult(ConstraintsSolver.java:391)
	at org.sosy_lab.cpachecker.cpa.constraints.domain.ConstraintsSolver.checkUnsat(ConstraintsSolver.java:359)
	at org.sosy_lab.cpachecker.cpa.constraints.domain.ConstraintsSolver.checkUnsatWithOptionDefinedSolverReuse(ConstraintsSolver.java:269)
	at org.sosy_lab.cpachecker.cpa.constraints.ConstraintsTransferRelation.getIfSatisfiable(ConstraintsTransferRelation.java:337)
	at org.sosy_lab.cpachecker.cpa.constraints.ConstraintsTransferRelation$ValueAnalysisStrengthenOperator.strengthen(ConstraintsTransferRelation.java:388)
	at org.sosy_lab.cpachecker.cpa.constraints.ConstraintsTransferRelation.strengthen(ConstraintsTransferRelation.java:304)
	at org.sosy_lab.cpachecker.cpa.composite.CompositeTransferRelation.callStrengthen(CompositeTransferRelation.java:326)
	at org.sosy_lab.cpachecker.cpa.composite.CompositeTransferRelation.getAbstractSuccessorForSimpleEdge(CompositeTransferRelation.java:269)
	at org.sosy_lab.cpachecker.cpa.composite.CompositeTransferRelation.getAbstractSuccessorForEdge(CompositeTransferRelation.java:190)
	at org.sosy_lab.cpachecker.cpa.composite.CompositeTransferRelation.getAbstractSuccessors(CompositeTransferRelation.java:88)
	at org.sosy_lab.cpachecker.cpa.arg.ARGTransferRelation.getAbstractSuccessors(ARGTransferRelation.java:45)
	at org.sosy_lab.cpachecker.core.algorithm.CPAAlgorithm.handleState(CPAAlgorithm.java:334)
	at org.sosy_lab.cpachecker.core.algorithm.CPAAlgorithm.run0(CPAAlgorithm.java:289)
	at org.sosy_lab.cpachecker.core.algorithm.CPAAlgorithm.run(CPAAlgorithm.java:260)
	at org.sosy_lab.cpachecker.core.algorithm.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)

Process finished with exit code 1

(Also, please take a look whether or not the print-outs of the formulas are from JavaSMT when debugging. If yes, we want to get rid of this.)

[baierd]

@daniel-raffler maybe you want to do this, as you are currently already working on a similar issue? (might even be related)

[baierd]

There are multiple more examples of this in the MR referenced above. If needed i can provide them as well, but the example above crashes the fastest with it.

[daniel-raffler]

@daniel-raffler maybe you want to do this, as you are currently already working on a similar issue? (might even be related)

I'll have a look at it. This is most likely the same issue as https://github.com/sosy-lab/java-smt/issues/481, but it doesn't hurt to have some more examples

Also, please take a look whether or not the print-outs of the formulas are from JavaSMT when debugging. If yes, we want to get rid of this.

These formulas are printed by MathSAT. I'm not sure why, but they seem to be some sort of unsat core. Maybe one of their assertions failed and this is debugging output?

[baierd]

Thank you!

These formulas are printed by MathSAT. I'm not sure why, but they seem to be some sort of unsat core. Maybe one of their assertions failed and this is debugging output?

That is also what i suspected. We should ask the devs whether or not they can remove this.

Alternatively, i know that @kfriedberger tried to mute the output of solvers at some point. Maybe we can use that here as well?

[baierd]

@daniel-raffler found a minimal query triggering this problem. Thank you!

(set-option :produce-models true)
(declare-fun a () (_ BitVec 32))
(declare-fun d () (Array (_ BitVec 32) Float64))
(declare-fun *d () (Array (_ BitVec 32) Float64))
(assert (and (= *d d) (not (fp.eq (select d a) (select d (_ bv0 32)))) (fp.eq (select d (_ bv0 32)) (select d (_ bv0 32)))))
(check-sat)
(get-model)

I reported it to the developers.

[kfriedberger]

This should be fixed with upcoming v5.6.12 of MathSAT.

[kfriedberger]

The PR #544 was merged. We still require feedback from CPAchecker whether the issues with model generation are solved.

[daniel-raffler]

The PR #544 was merged. We still require feedback from CPAchecker whether the issues with model generation are solved.

I ran more tests and version 5.6.12 seems to only have partially fixed the issue. However, there are still crashes left where MathSAT returns an invalid model iterator. I'll try to extract another trace from those failed tasks and will then report it to the MathSAT developers

[daniel-raffler]

I've extracted a trace from one of the failing runs here and reported it to the MathSAT developers:

(set-option :config "model_generation=true")
(set-option :config "dpll.ghost_filtering=true")

(declare-fun a () (_ BitVec 8))
(assert (not (= (_ bv0 32) (ite (= (_ bv0 32) (bvand (_ bv1 32) (bvnot (bvor (_ bv1 32) (ite (= (_ bv0 32) (ite (= (_ bv0 32) (ite (= (_ bv0 32) (ite (= (_ bv0 32) (ite (= (_ bv0 32) ((_ zero_extend 24) a)) (_ bv1 32) (_ bv0 32))) (_ bv1 32) (_ bv0 32))) (_ bv1 32) (_ bv0 32))) (_ bv1 32) (_ bv0 32))) (_ bv1 32) (_ bv0 32)))))) (_ bv1 32) (_ bv0 32)))))
(declare-fun m () (_ BitVec 8))
(assert (= (_ bv0 32) (ite (= (_ bv3 32) (bvor (_ bv1 32) (bvshl (_ bv1 32) (ite (not (= (_ bv0 32) (bvand (_ bv1 32) (bvor (_ bv1 32) (bvnot (ite (= (_ bv0 32) (ite (= (_ bv0 32) ((_ zero_extend 24) m)) (_ bv1 32) (_ bv0 32))) (_ bv1 32) (_ bv0 32))))))) (_ bv1 32) (_ bv0 32))))) (_ bv1 32) (_ bv0 32))))

(push 1)
(check-sat)
(pop 1)
(check-sat)

(get-model)

Here is the output with MathSAT 5.6.14:

daniel@notebook:~/Downloads/mathsat-5.6.14-linux-x86_64/bin$ ./mathsat ~/reduced.smt2 
unsat
sat
(= #b00000000000000000000000000000001 (bvand #b00000000000000000000000000000001 (bvor #b00000000000000000000000000000001 (bvnot (ite (= (ite (= m #b00000000) #b00000000000000000000000000000001 #b00000000000000000000000000000000) #b00000000000000000000000000000000) #b00000000000000000000000000000001 #b00000000000000000000000000000000)))))
(= (ite (not (= m #b00000000)) #b00000000000000000000000000000001 #b00000000000000000000000000000000) #b00000000000000000000000000000000)
(= (bvand #b00000000000000000000000000000001 (bvor #b00000000000000000000000000000001 (bvnot (ite (not (= m #b00000000)) #b00000000000000000000000000000001 #b00000000000000000000000000000000)))) #b00000000000000000000000000000000)
(= #b00000000000000000000000000000000 (ite (= (ite (= m #b00000000) #b00000000000000000000000000000001 #b00000000000000000000000000000000) #b00000000000000000000000000000000) #b00000000000000000000000000000001 #b00000000000000000000000000000000))
(error "Invalid model")

[baierd]

Thank you very much! A new MathSAT version has been published that addresses this. Related: #556

[kfriedberger]

MathSAT v5.6.15 is available via Ivy and integrated via #557 . Could someone test the new version?

[baierd]

I'll start some tests. Note: i'll need to adapt CPAchecker to our new changes first ;D slight delay.

[daniel-raffler]

I repeated ReachSafety-Hardware from svcomp26, which still had some issues with MathSAT 5.6.14, and the crashes now seem to be gone with the latest update: results.2025-12-08_17-20-30.diff.html

The columns are for MathSat 5.6.12, MathSat 5.6.14 and MathSat 5.6.15 from left to right. Note that the two remaining exceptions are unrelated and not caused by MathSAT

[baierd]

Thanks! That looks promising!

I started additional CPAchecker runs for the current master for SV-COMP, SymEx, Predicate Abstraction and IMC.