UnsupportedOperationException: State has more than one call successor in NestedWordAutomatonReachableStates

[danieldietsch]

Basic Info

• Version: 0.2.1-dev-bb7cadb (bb7cadb)
• Settings: set --traceabstraction.compute.hoare.annotation.of.negated.interpolant.automaton,.abstraction.and.cfg=true

Description

Programs with non-deterministic calls like the following may trigger the exception below. We probably notice the bug now because we remove all assume true edges during Icfg construction, but it should be fixed in the automata library.

A workaround is disabling the setting above, or add a condition to the Icfg construction.

  if(*){
    call foo1();
  } else if  (*){
    call foo2();
  }

Stacktrace:

java.lang.UnsupportedOperationException: State has more than one call successor
        at de.uni_freiburg.informatik.ultimate.automata.nestedword.reachablestates.NestedWordAutomatonReachableStates$AncestorComputation$1.next(NestedWordAutomatonReachableStates.java:1771)
        at de.uni_freiburg.informatik.ultimate.automata.nestedword.reachablestates.NestedWordAutomatonReachableStates$AncestorComputation$1.next(NestedWordAutomatonReachableStates.java:1)
        at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.HoareAnnotationFragments.addDeadEndDoubleDeckers(HoareAnnotationFragments.java:288)
        at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.BasicCegarLoop.computeAutomataDifference(BasicCegarLoop.java:908)
        at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.BasicCegarLoop.refineAbstraction(BasicCegarLoop.java:771)
        at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.AbstractCegarLoop.iterateInternal(AbstractCegarLoop.java:468)
        at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.AbstractCegarLoop.iterate(AbstractCegarLoop.java:372)
        at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.CegarLoopUtils.getCegarLoopResult(CegarLoopUtils.java:69)
        at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.CegarLoopUtils.getCegarLoopResult(CegarLoopUtils.java:63)
        at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionStarter.executeCegarLoop(TraceAbstractionStarter.java:383)
        at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionStarter.analyseProgram(TraceAbstractionStarter.java:317)
        at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionStarter.analyseSequentialProgram(TraceAbstractionStarter.java:277)
        at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionStarter.runCegarLoops(TraceAbstractionStarter.java:175)
        at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionStarter.<init>(TraceAbstractionStarter.java:154)
        at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver.finish(TraceAbstractionObserver.java:124)
        at de.uni_freiburg.informatik.ultimate.core.coreplugin.PluginConnector.runObserver(PluginConnector.java:168)
        at de.uni_freiburg.informatik.ultimate.core.coreplugin.PluginConnector.runTool(PluginConnector.java:151)
        at de.uni_freiburg.informatik.ultimate.core.coreplugin.PluginConnector.run(PluginConnector.java:128)
        at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainWalker.executePluginConnector(ToolchainWalker.java:232)
        at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainWalker.processPlugin(ToolchainWalker.java:226)
        at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainWalker.walkUnprotected(ToolchainWalker.java:142)
        at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainWalker.walk(ToolchainWalker.java:104)
        at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainManager$Toolchain.processToolchain(ToolchainManager.java:320)
        at de.uni_freiburg.informatik.ultimate.core.coreplugin.toolchain.RerunFreshToolchainJob.run(RerunFreshToolchainJob.java:91)
        at org.eclipse.core.internal.jobs.Worker.run(Worker.java:63)