search

appleseedlab / superc

The SuperC Parsing Framework
24 stars 4 forks source link

z3 error when using more recent version of z3 #167

Open paulgazz opened 2 years ago

paulgazz commented 2 years ago

When running -sourcelinePC, e.g., java superc.SuperC -sourcelinePC sourcelines kernel/bpf/cgroup.c, on com.microsoft.z3-4.8.12.0.jar, we get the following error, which doesn't occur with com.microsoft.z3-4.8.7.0.jar:

java.lang.NoSuchMethodError: 'com.microsoft.z3.BoolExpr com.microsoft.z3.Context.mkAnd(com.microsoft.z3.BoolExpr[])'
    at superc.core.PresenceConditionManager$PresenceConditionBDD.bddToZ3(PresenceConditionManager.java:1178)
    at superc.core.PresenceConditionManager$PresenceConditionBDD.toSMT2(PresenceConditionManager.java:1186)
    at superc.SuperC$ConditionalBlock.toString(SuperC.java:163)
    at superc.SuperC.parse(SuperC.java:970)
    at xtc.util.Tool.run(Tool.java:502)
    at superc.SuperC.main(SuperC.java:2012)
paulgazz commented 2 years ago

Fixed by using working version on z3, but should look into why there is this loss of backwards compatibility.