smtlib2 parse error

[TheBeaNerd]

jkind --version

JKind 4.0.0 Detected solvers: smtinterpol, z3, yices, yices2, cvc4, mathsat

command:

jkind -xml -solver z3 -timeout 16 --no_slicing fuzz.lus

exception:

jkind.JKindException: Solver output parse error line 8368:5 missing {'/', '>=', '<', '=', '>', '<=', 'and', 'ite', 'not', '-'} at 'or' at jkind.solvers.SolverParserErrorListener.syntaxError(SolverParserErrorListener.java:13) at org.antlr.v4.runtime.ProxyErrorListener.syntaxError(ProxyErrorListener.java:67) at org.antlr.v4.runtime.Parser.notifyErrorListeners(Parser.java:561) at org.antlr.v4.runtime.DefaultErrorStrategy.reportMissingToken(DefaultErrorStrategy.java:409) at org.antlr.v4.runtime.DefaultErrorStrategy.singleTokenInsertion(DefaultErrorStrategy.java:512) at org.antlr.v4.runtime.DefaultErrorStrategy.recoverInline(DefaultErrorStrategy.java:476) at jkind.solvers.smtlib2.SmtLib2Parser.fn(SmtLib2Parser.java:339) at jkind.solvers.smtlib2.SmtLib2Parser.body(SmtLib2Parser.java:290) at jkind.solvers.smtlib2.SmtLib2Parser.define(SmtLib2Parser.java:153) at jkind.solvers.smtlib2.SmtLib2Parser.model(SmtLib2Parser.java:83) at jkind.solvers.smtlib2.SmtLib2Solver.parseSmtLib2Model(SmtLib2Solver.java:208) at jkind.solvers.smtlib2.SmtLib2Solver.parseModel(SmtLib2Solver.java:198) at jkind.solvers.z3.Z3Solver.query(Z3Solver.java:63) at jkind.engines.KInductionEngine.checkProperties(KInductionEngine.java:88) at jkind.engines.KInductionEngine.main(KInductionEngine.java:53) at jkind.engines.Engine.run(Engine.java:35) at jkind.engines.SolverBasedEngine.run(SolverBasedEngine.java:37) at java.lang.Thread.run(Thread.java:745)

fuzz.lus:

fuzz.txt

[TheBeaNerd]

This may be relevant:

z3 --version Z3 version 4.8.0 - 64 bit

Let me know how I might capture the offending file, if that would help.

[agacek]

Run with -scratch to get the debug files.

On Fri, Aug 31, 2018 at 2:40 PM David Greve notifications@github.com wrote:

This may be relevant:

z3 --version Z3 version 4.8.0 - 64 bit

Let me know how I might capture the offending file, if that would help.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/agacek/jkind/issues/46#issuecomment-417769846, or mute the thread https://github.com/notifications/unsubscribe-auth/AAKgiEgbDSwRr6XGJoEV9WW4M4CYI7qgks5uWZFIgaJpZM4WVvkx .

[TheBeaNerd]

There is a ternary 'or' expression in the k-induction file (?)

Would you prefer a different file?

fuzz.lus.k-induction.txt

[agacek]

Yes, the 'or' expression was the problem. None of the SMT-LIB solvers have used it before. I pushed out a fix. Thanks for finding this.