search

kframework / k-legacy

The K tools (deprecated, see README)
http://kframework.org
Other
146 stars 61 forks source link

SHA3 Hook #2313

Closed ayberkt closed 7 years ago

ayberkt commented 7 years ago

I am trying to use the SHA3 hook @msaxena2 added just today, which results in the following error.

java.lang.NoClassDefFoundError: Could not initialize class com.microsoft.z3.Native
    at com.microsoft.z3.Context.<init>(Context.java:24)
    at org.kframework.backend.java.util.Z3Wrapper.checkQueryWithLibrary(Z3Wrapper.java:61)
    at org.kframework.backend.java.util.Z3Wrapper.isUnsat(Z3Wrapper.java:54)
    at org.kframework.backend.java.symbolic.SMTOperations.checkUnsat(SMTOperations.java:39)
    at org.kframework.backend.java.symbolic.ConjunctiveFormula.checkUnsat(ConjunctiveFormula.java:637)
    at org.kframework.backend.java.kil.ConstrainedTerm.evaluateConstraints(ConstrainedTerm.java:230)
    at org.kframework.backend.java.symbolic.FastRuleMatcher.matchRulePattern(FastRuleMatcher.java:127)
    at org.kframework.backend.java.symbolic.SymbolicRewriter.fastComputeRewriteStep(SymbolicRewriter.java:163)
    at org.kframework.backend.java.symbolic.SymbolicRewriter.computeRewriteStep(SymbolicRewriter.java:104)
    at org.kframework.backend.java.symbolic.SymbolicRewriter.rewrite(SymbolicRewriter.java:85)
    at org.kframework.backend.java.symbolic.InitializeRewriter$SymbolicRewriterGlue.execute(InitializeRewriter.java:147)
    at org.kframework.krun.modes.KRunExecutionMode.execute(KRunExecutionMode.java:65)
    at org.kframework.krun.KRun.run(KRun.java:104)
    at org.kframework.krun.KRunFrontEnd.run(KRunFrontEnd.java:67)
    at org.kframework.main.FrontEnd.main(FrontEnd.java:34)
    at org.kframework.main.Main.runApplication(Main.java:415)
    at org.kframework.main.Main.runApplication(Main.java:264)
    at org.kframework.kserver.KServerFrontEnd.run(KServerFrontEnd.java:90)
    at org.kframework.main.Main.nailMain(Main.java:435)
    at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
    at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
    at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
    at java.lang.reflect.Method.invoke(Method.java:497)
    at com.martiansoftware.nailgun.NGSession.run(NGSession.java:325)

I would appreciate if you could look into this some time @msaxena2.

/cc: @lucaspena

msaxena2 commented 7 years ago

fixed via #2315