diff --git a/trunk/examples/programs/regression/bpl/multipleCallSuccessors-01.bpl b/trunk/examples/programs/regression/bpl/multipleCallSuccessors-01.bpl
new file mode 100644
index 00000000000..e6071beb0c3
--- /dev/null
+++ b/trunk/examples/programs/regression/bpl/multipleCallSuccessors-01.bpl
@@ -0,0 +1,66 @@
+//#Safe
+/*
+    20021-06-21 Daniel Dietsch
+    
+    Necessary setting:
+    --traceabstraction.compute.hoare.annotation.of.negated.interpolant.automaton,.abstraction.and.cfg=true 
+    
+    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)
+ */
+
+var x : int;
+
+procedure main()
+modifies x;
+{
+  x:=0;
+  if(*){
+    call foo1();
+  } else if  (*){
+    call foo2();
+  } else {
+    assume false;
+  }
+  assert x == 1; 
+}
+
+procedure foo1()
+modifies x;
+{
+  x:=x+1;
+}
+
+procedure foo2()
+modifies x;
+{
+  x:=x+1;
+}
+
+
+
+