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 #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.