Question: How to use bvbuiltin functions in LTLAutomizer?

[GreenieQwQ]

Basic Info

The following boogie example may require the boogie-steps Branch. The branch enables handling of LTL attributes in Boogie (as used by the example).

An archive with the Boogie file, the tool chain and the setting file is attached: archive.zip.

Description

I'm running Ultimate Debugging Gui to test if LTLAutomizer supports the bitvector version of boogie. Unfortunately, it reported:

java.lang.UnsupportedOperationException: function symbols not yet supported: (add.bv8 (_ BitVec 8) (_ BitVec 8) (_ BitVec 8)) Type: class de.uni_freiburg.informatik.ultimate.lib.smtlibutils.NonTheorySymbol$Function
	at de.uni_freiburg.informatik.ultimate.lassoranker.variables.LassoPartitioneer.addInOuAuxVar(LassoPartitioneer.java:238)
	at de.uni_freiburg.informatik.ultimate.lassoranker.variables.LassoPartitioneer.constructTransFormulaLR(LassoPartitioneer.java:210)
	at de.uni_freiburg.informatik.ultimate.lassoranker.variables.LassoPartitioneer.doPartition(LassoPartitioneer.java:165)
	at de.uni_freiburg.informatik.ultimate.lassoranker.variables.LassoPartitioneer.<init>(LassoPartitioneer.java:95)
	at de.uni_freiburg.informatik.ultimate.lassoranker.preprocessors.LassoPartitioneerPreprocessor.process(LassoPartitioneerPreprocessor.java:65)
	at de.uni_freiburg.informatik.ultimate.lassoranker.variables.LassoBuilder.applyPreprocessor(LassoBuilder.java:154)
	at de.uni_freiburg.informatik.ultimate.lassoranker.variables.LassoBuilder.preprocess(LassoBuilder.java:262)
	at de.uni_freiburg.informatik.ultimate.lassoranker.LassoAnalysis.preprocess(LassoAnalysis.java:280)
	at de.uni_freiburg.informatik.ultimate.lassoranker.LassoAnalysis.<init>(LassoAnalysis.java:229)
	at de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer.LassoCheck.synthesize(LassoCheck.java:601)
	at de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer.LassoCheck$LassoCheckResult.checkLassoTermination(LassoCheck.java:916)
	at de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer.LassoCheck$LassoCheckResult.<init>(LassoCheck.java:823)
	at de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer.LassoCheck.<init>(LassoCheck.java:247)
	at de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer.cegar.AbstractBuchiCegarLoop.runCegarLoop(AbstractBuchiCegarLoop.java:310)
	at de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer.BuchiAutomizerObserver.doTerminationAnalysis(BuchiAutomizerObserver.java:146)
	at de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer.BuchiAutomizerObserver.finish(BuchiAutomizerObserver.java:363)
	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)

I manually added the detailed information in the first line. I wonder if there is something wrong in my settings, or the current version of LTLAutomizer is not capable of handling bvbuiltin functions (as in the example, add.bv8 is of attribute {:bvbuiltin "bvadd"})?

Any answer would be of great help.

[schuessf]

If I remember correctly, we currently cannot handle bitvectors in the computation of ranking functions, which is however necessary in LTLAutomizer and BuchiAutomizer. The implementation of this feature would require some effort. @Heizmann knows more about this than I do, so correct me if I am wrong.