The spec in livenessBenchmarks cannot be verified.
Closed this issue · 0 comments
Cglasses commented
The spec in the benchmarks even cannot be verified by SmartPulse, which throws an exception
[2022-07-05 23:07:40,355 FATAL L265 ToolchainWalker]: An unrecoverable error occured during an interaction with an SMT solver:
de.uni_freiburg.informatik.ultimate.logic.SMTLIBException: Undeclared function symbol (select (Array Int Int) (Array Int Int))
at de.uni_freiburg.informatik.ultimate.logic.NoopScript.term(NoopScript.java:321)
at de.uni_freiburg.informatik.ultimate.logic.NoopScript.term(NoopScript.java:296)
at de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.SmtUtils.select(SmtUtils.java:1322)
at de.uni_freiburg.informatik.ultimate.modelcheckerutils.boogie.Expression2Term.translate(Expression2Term.java:179)
at de.uni_freiburg.informatik.ultimate.modelcheckerutils.boogie.Expression2Term.translate(Expression2Term.java:223)
at de.uni_freiburg.informatik.ultimate.modelcheckerutils.boogie.Expression2Term.translate(Expression2Term.java:223)
at de.uni_freiburg.informatik.ultimate.modelcheckerutils.boogie.Expression2Term.translate(Expression2Term.java:222)
at de.uni_freiburg.informatik.ultimate.modelcheckerutils.boogie.Expression2Term.translateToTerm(Expression2Term.java:121)
at de.uni_freiburg.informatik.ultimate.modelcheckerutils.boogie.Statements2TransFormula.addAssume(Statements2TransFormula.java:320)
at de.uni_freiburg.informatik.ultimate.modelcheckerutils.boogie.Statements2TransFormula.statementSequence(Statements2TransFormula.java:704)
at de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder.util.TransFormulaAdder.addTransitionFormulas(TransFormulaAdder.java:119)
at de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder.cfg.CfgBuilder$ProcedureCfgBuilder.buildProcedureCfgFromImplementation(CfgBuilder.java:658)
at de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder.cfg.CfgBuilder$ProcedureCfgBuilder.access$1(CfgBuilder.java:572)
at de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder.cfg.CfgBuilder.createIcfg(CfgBuilder.java:260)
at de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder.RCFGBuilderObserver.process(RCFGBuilderObserver.java:91)
at de.uni_freiburg.informatik.ultimate.core.coreplugin.modelwalker.DFSTreeWalker.runObserver(DFSTreeWalker.java:65)
at de.uni_freiburg.informatik.ultimate.core.coreplugin.modelwalker.BaseWalker.runObserver(BaseWalker.java:93)
at de.uni_freiburg.informatik.ultimate.core.coreplugin.modelwalker.BaseWalker.run(BaseWalker.java:86)
at de.uni_freiburg.informatik.ultimate.core.coreplugin.PluginConnector.runObserver(PluginConnector.java:167)
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:317)
at de.uni_freiburg.informatik.ultimate.core.coreplugin.toolchain.DefaultToolchainJob.run(DefaultToolchainJob.java:145)
at org.eclipse.core.internal.jobs.Worker.run(Worker.java:55)
Besides, what's the meaning of sum_pendingReturns0 and pendingReturns_Auction? They are not variables in Auction.sol. I'm really curious about that.