search

loonwerks / jkind

JKind - An infinite-state model checker for safety properties in Lustre
http://loonwerks.com/tools/jkind.html
Other
52 stars 32 forks source link

SmtLib2 Parser does not work for z3 models #60

Closed mgudemann closed 3 years ago

mgudemann commented 3 years ago

Current z3 (version 4.8.11) creates models which do not start with '(model ` which is defined in the grammar for smtlib.

bmc process failed                                                                                                                                                                           
jkind.JKindException: Solver output parse error line 2:2 missing 'model' at '('                                                                                                              
        at jkind.solvers.SolverParserErrorListener.syntaxError(SolverParserErrorListener.java:13)       
...

I think this is also what the SMTlib documentation specifies.

c.f. https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.5-r2015-06-28.pdf

(get-model) returns a list (d1 · · · dk) of definitions specifying all and only the current user declared function symbols {g1, . . . , gm} in the current model A.
lgwagner commented 3 years ago

Thank you for submitting this. I apologize for this fix taking so long. I have one more issue to fix and I will generate a new release.