EBMC/ic3 fails to analyze SMV converted from AIG

[mgudemann]

on master seems to be stuck at this

Parsing ./dpdtvisns3p02.aig/pdtvisns3p02.aig.smv
Converting
Type-checking smv::main
Generating Netlist

again, example from AIG_SMV_08

[eigold]

Thanks, Matthias, Could you mail this example to me? I already got 6 failed smv examples from the ebmc regression test. (Some of the failures can be trivially fixed.) As I said earlier, for now, I have set the type of properties checked by ic3 to "ID_sva_always" (as opposed to ID_AG, the type of safety properties generated off SMV designs). Apparently, there is a subtle difference between netlists generated from Verilog and SMV descriptions. I am not sure if Daniel wants ic3 to check safety properties generated by SMV designs in the coming release. (Fixing the problem above will definitely take some time.) Best wishes, Eugene

…

On Sun, Jul 2, 2017 at 12:59 PM, Matthias Güdemann ***@***.*** > wrote: Assigned #19 <#19> to @eigold <https://github.com/eigold>. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#19 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AS5pCnGLj-zuo_XJfxRxZY_KweD5ghGQks5sJ8yBgaJpZM4OLjjv> .