search

ultimate-pa / ultimate

The Ultimate program analysis framework.
https://ultimate-pa.org/
198 stars 41 forks source link

Bug: SMTLIBException: Timeout exceeded #573

Open danieldietsch opened 3 years ago

danieldietsch commented 3 years ago

SMTInterpol timeout is not converted to TimeoutResult. Instead, it is handled as an ExceptionOrErrorResult, thus canceling the whole verification.

Stacktrace

de.uni_freiburg.informatik.ultimate.logic.SMTLIBException: Timeout exceeded
        at de.uni_freiburg.informatik.ultimate.smtinterpol.interpolate.Interpolator.interpolate(Interpolator.java:244)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.interpolate.Interpolator.getInterpolants(Interpolator.java:226)
        at de.uni_freiburg.informatik.ultimate.smtinterpol.smtlib2.SMTInterpol.getInterpolants(SMTInterpol.java:876)
        at de.uni_freiburg.informatik.ultimate.logic.NoopScript.getInterpolants(NoopScript.java:392)
        at de.uni_freiburg.informatik.ultimate.logic.NoopScript.getInterpolants(NoopScript.java:386)
        at de.uni_freiburg.informatik.ultimate.logic.WrapperScript.getInterpolants(WrapperScript.java:337)
        at de.uni_freiburg.informatik.ultimate.logic.WrapperScript.getInterpolants(WrapperScript.java:337)
        at de.uni_freiburg.informatik.ultimate.lib.smtlibutils.ManagedScript.getInterpolants(ManagedScript.java:191)
        at de.uni_freiburg.informatik.ultimate.lib.tracecheckerutils.singletracecheck.NestedInterpolantsBuilder.computeCraigInterpolants(NestedInterpolantsBuilder.java:285)
        at de.uni_freiburg.informatik.ultimate.lib.tracecheckerutils.singletracecheck.NestedInterpolantsBuilder.<init>(NestedInterpolantsBuilder.java:166)
        at de.uni_freiburg.informatik.ultimate.lib.tracecheckerutils.singletracecheck.InterpolatingTraceCheckCraig.computeInterpolantsRecursive(InterpolatingTraceCheckCraig.java:327)
        at de.uni_freiburg.informatik.ultimate.lib.tracecheckerutils.singletracecheck.InterpolatingTraceCheckCraig.computeInterpolants(InterpolatingTraceCheckCraig.java:229)
        at de.uni_freiburg.informatik.ultimate.lib.tracecheckerutils.singletracecheck.InterpolatingTraceCheckCraig.<init>(InterpolatingTraceCheckCraig.java:97)
        at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.tracehandling.IpTcStrategyModuleCraig.construct(IpTcStrategyModuleCraig.java:79)
        at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.tracehandling.IpTcStrategyModuleCraig.construct(IpTcStrategyModuleCraig.java:1)
        at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.tracehandling.IpTcStrategyModuleBase.getOrConstruct(IpTcStrategyModuleBase.java:100)
        at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.tracehandling.IpTcStrategyModuleBase.isCorrect(IpTcStrategyModuleBase.java:56)
        at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.tracehandling.AutomatonFreeRefinementEngine.checkFeasibility(AutomatonFreeRefinementEngine.java:211)
        at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.tracehandling.AutomatonFreeRefinementEngine.executeStrategy(AutomatonFreeRefinementEngine.java:124)
        at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.tracehandling.AutomatonFreeRefinementEngine.<init>(AutomatonFreeRefinementEngine.java:88)
        at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.tracehandling.TraceAbstractionRefinementEngine.<init>(TraceAbstractionRefinementEngine.java:76)
        at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.BasicCegarLoop.isCounterexampleFeasible(BasicCegarLoop.java:621)
        at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.AbstractCegarLoop.iterate(AbstractCegarLoop.java:413)
        at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.AbstractCegarLoop.startCegar(AbstractCegarLoop.java:348)
        at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.AbstractCegarLoop.runCegar(AbstractCegarLoop.java:330)
        at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.CegarLoopUtils.getCegarLoopResult(CegarLoopUtils.java:53)
        at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionStarter.executeCegarLoop(TraceAbstractionStarter.java:368)
        at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionStarter.analyseProgram(TraceAbstractionStarter.java:298)
        at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionStarter.analyseSequentialProgram(TraceAbstractionStarter.java:258)
        at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionStarter.runCegarLoops(TraceAbstractionStarter.java:171)
        at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionStarter.<init>(TraceAbstractionStarter.java:150)
        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)
Heizmann commented 3 years ago

This is not a timeout of Ultimate either. We might want to continue with another solver. We probably need a mechanism that propagates this result down to the RefinementEngine that then has to decide how to continue.