Error appears in SMG join depending on wall time limit present
scripts/cpa.sh -heap 4000M -noout -setprop cpa.smg.runtimeCheck=FULL -setprop limits.time.wall=30 -smg-ldv -spec config/properties/valid-memsafety.prp test/programs/benchmarks/forester-heap/dll-01-2.i
results in FALSE (valid-deref: invalid pointer dereference in line 1056), while same command line without wall time limit results in exception in SMG join:
Full trace
Exception in thread "main" java.lang.IllegalArgumentException: expected one element but was: <Sym_723->dll+0b, Sym_726->dll+0b>
at com.google.common.collect.Iterators.getOnlyElement(Iterators.java:323)
at com.google.common.collect.Iterables.getOnlyElement(Iterables.java:263)
at org.sosy_lab.cpachecker.cpa.smg.join.SMGJoinMapTargetAddress.<init>(SMGJoinMapTargetAddress.java:74)
at org.sosy_lab.cpachecker.cpa.smg.join.SMGJoinTargetObjects.checkAlreadyJoined(SMGJoinTargetObjects.java:62)
at org.sosy_lab.cpachecker.cpa.smg.join.SMGJoinTargetObjects.<init>(SMGJoinTargetObjects.java:133)
at org.sosy_lab.cpachecker.cpa.smg.join.SMGJoinValues.joinValuesPointers(SMGJoinValues.java:198)
at org.sosy_lab.cpachecker.cpa.smg.join.SMGJoinValues.<init>(SMGJoinValues.java:297)
at org.sosy_lab.cpachecker.cpa.smg.join.SMGJoinValues.insertLeftListAndJoin(SMGJoinValues.java:1076)
at org.sosy_lab.cpachecker.cpa.smg.join.SMGJoinValues.<init>(SMGJoinValues.java:318)
at org.sosy_lab.cpachecker.cpa.smg.join.SMGJoinSubSMGs.<init>(SMGJoinSubSMGs.java:143)
at org.sosy_lab.cpachecker.cpa.smg.join.SMGJoin.<init>(SMGJoin.java:115)
at org.sosy_lab.cpachecker.cpa.smg.SMGState.isLessOrEqual(SMGState.java:1529)
at org.sosy_lab.cpachecker.cpa.smg.SMGState.isLessOrEqual(SMGState.java:90)
at org.sosy_lab.cpachecker.core.defaults.DelegateAbstractDomain.isLessOrEqual(DelegateAbstractDomain.java:40)
at org.sosy_lab.cpachecker.core.defaults.StopSepOperator.stop(StopSepOperator.java:33)
at org.sosy_lab.cpachecker.cpa.smg.SMGStopOperator.stop(SMGStopOperator.java:30)
at org.sosy_lab.cpachecker.cpa.composite.CompositeStopOperator.stop(CompositeStopOperator.java:67)
at org.sosy_lab.cpachecker.cpa.composite.CompositeStopOperator.stop(CompositeStopOperator.java:40)
at org.sosy_lab.cpachecker.cpa.arg.ARGStopSep.stop(ARGStopSep.java:148)
at org.sosy_lab.cpachecker.cpa.arg.ARGStopSep.stop(ARGStopSep.java:111)
at org.sosy_lab.cpachecker.core.algorithm.CPAAlgorithm.handleState(CPAAlgorithm.java:451)
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.CounterexampleStoreAlgorithm.run(CounterexampleStoreAlgorithm.java:58)
at org.sosy_lab.cpachecker.core.CPAchecker.runAlgorithm(CPAchecker.java:512)
at org.sosy_lab.cpachecker.core.CPAchecker.run(CPAchecker.java:377)
at org.sosy_lab.cpachecker.cmdline.CPAMain.main(CPAMain.java:170)