Kojak analysis often produces assertion during writing of output files
The Kojak analysis seems to produce an invalid reached set (with destroyed ARG states) on timeouts, which triggers an assertions during writing of output files:
Exception in thread "main" java.lang.AssertionError: Don't use destroyed ARGState Destroyed ARG State (Id: 829) (LocationState: N1028 (after line 1145)
CallstackState: Function eval called from node N1125, stack depth 3 [649f2009], stack [main, start_simulation, eval]
FunctionPointerState: []
NonAbstractionState: Abstraction location: false
AutomatonState: SVCOMP: Init
)
at org.sosy_lab.cpachecker.cpa.arg.ARGState.getChildren(ARGState.java:121)
at org.sosy_lab.cpachecker.util.coverage.ReachedSetCoverageCollector.collectCoveredEdges(CoverageCollector.java:141)
at org.sosy_lab.cpachecker.util.coverage.ReachedSetCoverageCollector.collectFromReachedSet(CoverageCollector.java:126)
at org.sosy_lab.cpachecker.util.coverage.CoverageCollector.fromReachedSet(CoverageCollector.java:51)
at org.sosy_lab.cpachecker.core.MainCPAStatistics.exportCoverage(MainCPAStatistics.java:346)
at org.sosy_lab.cpachecker.core.MainCPAStatistics.printStatistics(MainCPAStatistics.java:292)
at org.sosy_lab.cpachecker.core.CPAcheckerResult.printStatistics(CPAcheckerResult.java:104)
at org.sosy_lab.cpachecker.cmdline.CPAMain.printResultAndStatistics(CPAMain.java:588)
at org.sosy_lab.cpachecker.cmdline.CPAMain.main(CPAMain.java:187)
The refinement should make sure that the reached set is in a consistent (sound) state whenever refinement is terminated (even on timeout). This is also important for correctly detecting the result of the analysis, and for example for conditional model checking.
This happens non-deterministically, examples can be seen here.