Bug: ArrayIndexOutOfBoundsException in traceabstraction

[blizzard4591]

Basic Info

• Version: 38b53e6 (the one from svcomp23)

• (Optional) Java Version: 11 OpenJDK

• Input file: Req1_Prop1_Batch121dependencies.zip

• Settings: ./Ultimate.py --spec ../../custom-benchmarks/CodeModifications_Release/dependencies/reach.prp --file ../../custom-benchmarks/CodeModifications_Release/dependencies/Req1_Prop1_Batch121dependencies.i --full-output --architecture 32bit

• Toolchain: The toolchain file (.xml, provided with the -tc argument)

• The complete Ultimate log file (if available): CodeModifications_Release.Req1_Prop1_Batch121dependencies.yml.log

Description

One some of these instances, e.g. 121 as shown here, Ultimate crashes with

[2023-01-29 19:52:37,645 FATAL L?                        ?]: The Plugin de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction has thrown an exception:
java.lang.ArrayIndexOutOfBoundsException: Index -1 out of bounds for length 5
	at de.uni_freiburg.informatik.ultimate.util.datastructures.ScopedHashMap.undoMap(ScopedHashMap.java:97)
	at de.uni_freiburg.informatik.ultimate.util.datastructures.ScopedHashMap.endScope(ScopedHashMap.java:127)
	at de.uni_freiburg.informatik.ultimate.lib.smtlibutils.arrays.DiffWrapperScript.pop(DiffWrapperScript.java:101)
	at de.uni_freiburg.informatik.ultimate.logic.WrapperScript.pop(WrapperScript.java:153)
	at de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.smt.scripttransfer.HistoryRecordingScript.pop(HistoryRecordingScript.java:117)
	at de.uni_freiburg.informatik.ultimate.lib.smtlibutils.ManagedScript.pop(ManagedScript.java:129)
	at de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.hoaretriple.IncrementalHoareTripleChecker.unAssertCodeBlock(IncrementalHoareTripleChecker.java:436)
	at de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.hoaretriple.IncrementalHoareTripleChecker.clearAssertionStack(IncrementalHoareTripleChecker.java:278)
	at de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.hoaretriple.IncrementalHoareTripleChecker.releaseLock(IncrementalHoareTripleChecker.java:284)
	at de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.hoaretriple.ChainingHoareTripleChecker$ProtectedHtc.releaseLock(ChainingHoareTripleChecker.java:449)
	at java.base/java.util.ArrayList$ArrayListSpliterator.forEachRemaining(ArrayList.java:1655)
	at java.base/java.util.stream.ReferencePipeline$Head.forEach(ReferencePipeline.java:658)
	at de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.hoaretriple.ChainingHoareTripleChecker.releaseLock(ChainingHoareTripleChecker.java:98)
	at de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.hoaretriple.CachingHoareTripleChecker.releaseLock(CachingHoareTripleChecker.java:149)
	at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.interpolantautomata.transitionappender.AbstractInterpolantAutomaton.switchToReadonlyMode(AbstractInterpolantAutomaton.java:140)
	at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.NwaCegarLoop.computeAutomataDifference(NwaCegarLoop.java:365)
	at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.NwaCegarLoop.refineAbstraction(NwaCegarLoop.java:325)
	at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.AbstractCegarLoop.refineAbstractionInternal(AbstractCegarLoop.java:487)
	at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.AbstractCegarLoop.iterate(AbstractCegarLoop.java:438)
	at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.AbstractCegarLoop.startCegar(AbstractCegarLoop.java:366)
	at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.AbstractCegarLoop.runCegar(AbstractCegarLoop.java:348)
	at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionStarter.executeCegarLoop(TraceAbstractionStarter.java:415)
	at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionStarter.analyseProgram(TraceAbstractionStarter.java:302)
	at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionStarter.analyseSequentialProgram(TraceAbstractionStarter.java:262)
	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.DefaultToolchainJob.run(DefaultToolchainJob.java:145)
	at org.eclipse.core.internal.jobs.Worker.run(Worker.java:63)

[blizzard4591]

I should add that all of this is performed inside the SV-COMP23 container environment using Benchexec, so outside factors should not play a role.