Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Cannot merge Overapprox #189

Closed
Heizmann opened this issue Jun 3, 2017 · 0 comments
Closed

Cannot merge Overapprox #189

Heizmann opened this issue Jun 3, 2017 · 0 comments
Assignees

Comments

@Heizmann
Copy link
Member

Heizmann commented Jun 3, 2017

Input: examples/svcomp/ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c
Toolchain: examples/toolchains/AutomizerCInlineWithBlockEncoding.xml
Settings: examples/settings/svcomp2017/automizer/svcomp-Reach-32bit-Automizer_Default.epf

I get the following error message.
(Issue has low priority for me.)

de.uni_freiburg.informatik.ultimate.core.model.models.annotation.IAnnotations$UnmergeableAnnotationsException: Cannot merge class de.uni_freiburg.informatik.ultimate.core.lib.models.annotation.Overapprox with class de.uni_freiburg.informatik.ultimate.core.lib.models.annotation.Overapprox
at de.uni_freiburg.informatik.ultimate.core.model.models.annotation.IAnnotations.merge(IAnnotations.java:75)
at de.uni_freiburg.informatik.ultimate.core.model.models.ModelUtils.mergeAnnotations(ModelUtils.java:100)
at de.uni_freiburg.informatik.ultimate.plugins.blockencoding.encoding.IcfgEdgeBuilder.constructSequentialComposition(IcfgEdgeBuilder.java:119)
at de.uni_freiburg.informatik.ultimate.plugins.blockencoding.encoding.IcfgEdgeBuilder.constructSequentialComposition(IcfgEdgeBuilder.java:101)
at de.uni_freiburg.informatik.ultimate.plugins.blockencoding.encoding.MinimizeStatesMultiEdgeMultiNode$EdgeConstructor.constructSequentialComposition(MinimizeStatesMultiEdgeMultiNode.java:185)
at de.uni_freiburg.informatik.ultimate.plugins.blockencoding.encoding.MinimizeStatesMultiEdgeMultiNode$EdgeConstructor.access$1(MinimizeStatesMultiEdgeMultiNode.java:184)
at java.util.HashMap$KeySpliterator.forEachRemaining(HashMap.java:1548)
at java.util.stream.ReferencePipeline$Head.forEach(ReferencePipeline.java:580)
at de.uni_freiburg.informatik.ultimate.plugins.blockencoding.encoding.MinimizeStatesMultiEdgeMultiNode.processCandidate(MinimizeStatesMultiEdgeMultiNode.java:129)
at de.uni_freiburg.informatik.ultimate.plugins.blockencoding.encoding.BaseMinimizeStates.createResult(BaseMinimizeStates.java:97)
at de.uni_freiburg.informatik.ultimate.plugins.blockencoding.encoding.BaseBlockEncoder.getResult(BaseBlockEncoder.java:78)
at de.uni_freiburg.informatik.ultimate.plugins.blockencoding.BlockEncoder.applyEncoder(BlockEncoder.java:272)
at de.uni_freiburg.informatik.ultimate.plugins.blockencoding.BlockEncoder.processIcfg(BlockEncoder.java:188)
at de.uni_freiburg.informatik.ultimate.plugins.blockencoding.BlockEncoder.(BlockEncoder.java:109)
at de.uni_freiburg.informatik.ultimate.plugins.blockencoding.BlockEncodingObserver.process(BlockEncodingObserver.java:96)
at de.uni_freiburg.informatik.ultimate.core.coreplugin.modelwalker.CFGWalker.runObserver(CFGWalker.java:57)
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:324)
at de.uni_freiburg.informatik.ultimate.core.coreplugin.toolchain.DefaultToolchainJob.rerunToolchain(DefaultToolchainJob.java:173)
at de.uni_freiburg.informatik.ultimate.core.coreplugin.toolchain.BasicToolchainJob.run(BasicToolchainJob.java:131)
at org.eclipse.core.internal.jobs.Worker.run(Worker.java:55)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants