Z3 parse error during division

TimArnettThales commented 3 years ago

Division operations fail when using non-constant values with Z3 versions 4.8.9+

bmc process failed
jkind.JKindException: Solver output parse error line 80:14 no viable alternative at input '/'
        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.reportNoViableAlternative(DefaultErrorStrategy.java:310)
        at org.antlr.v4.runtime.DefaultErrorStrategy.reportError(DefaultErrorStrategy.java:147)
        at jkind.solvers.smtlib2.SmtLib2Parser.id(SmtLib2Parser.java:633)
        at jkind.solvers.smtlib2.SmtLib2Parser.define(SmtLib2Parser.java:139)
        at jkind.solvers.smtlib2.SmtLib2Parser.model(SmtLib2Parser.java:86)
        at jkind.solvers.smtlib2.SmtLib2Solver.parseSmtLib2Model(SmtLib2Solver.java:219)
        at jkind.solvers.smtlib2.SmtLib2Solver.parseModel(SmtLib2Solver.java:208)
        at jkind.solvers.z3.Z3Solver.query(Z3Solver.java:72)
        at jkind.engines.BmcEngine.checkProperties(BmcEngine.java:48)
        at jkind.engines.BmcEngine.main(BmcEngine.java:39)
        at jkind.engines.Engine.run(Engine.java:36)
        at jkind.engines.SolverBasedEngine.run(SolverBasedEngine.java:37)
        at java.lang.Thread.run(Unknown Source)
k-induction process failed
jkind.JKindException: Solver output parse error line 80:14 no viable alternative at input '/'
        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.reportNoViableAlternative(DefaultErrorStrategy.java:310)
        at org.antlr.v4.runtime.DefaultErrorStrategy.reportError(DefaultErrorStrategy.java:147)
        at jkind.solvers.smtlib2.SmtLib2Parser.id(SmtLib2Parser.java:633)
        at jkind.solvers.smtlib2.SmtLib2Parser.define(SmtLib2Parser.java:139)
        at jkind.solvers.smtlib2.SmtLib2Parser.model(SmtLib2Parser.java:86)
        at jkind.solvers.smtlib2.SmtLib2Solver.parseSmtLib2Model(SmtLib2Solver.java:219)
        at jkind.solvers.smtlib2.SmtLib2Solver.parseModel(SmtLib2Solver.java:208)
        at jkind.solvers.z3.Z3Solver.query(Z3Solver.java:72)
        at jkind.engines.KInductionEngine.checkProperties(KInductionEngine.java:88)
        at jkind.engines.KInductionEngine.main(KInductionEngine.java:53)
        at jkind.engines.Engine.run(Engine.java:36)
        at jkind.engines.SolverBasedEngine.run(SolverBasedEngine.java:37)
        at java.lang.Thread.run(Unknown Source)
invariant-generation process failed
jkind.JKindException: Solver output parse error line 80:14 no viable alternative at input '/'
        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.reportNoViableAlternative(DefaultErrorStrategy.java:310)
        at org.antlr.v4.runtime.DefaultErrorStrategy.reportError(DefaultErrorStrategy.java:147)
        at jkind.solvers.smtlib2.SmtLib2Parser.id(SmtLib2Parser.java:633)
        at jkind.solvers.smtlib2.SmtLib2Parser.define(SmtLib2Parser.java:139)
        at jkind.solvers.smtlib2.SmtLib2Parser.model(SmtLib2Parser.java:86)
        at jkind.solvers.smtlib2.SmtLib2Solver.parseSmtLib2Model(SmtLib2Solver.java:219)
        at jkind.solvers.smtlib2.SmtLib2Solver.parseModel(SmtLib2Solver.java:208)
        at jkind.solvers.z3.Z3Solver.query(Z3Solver.java:72)
        at jkind.engines.invariant.AbstractInvariantGenerationEngine.refineBaseStep(AbstractInvariantGenerationEngine.java:74)
        at jkind.engines.invariant.AbstractInvariantGenerationEngine.main(AbstractInvariantGenerationEngine.java:49)
        at jkind.engines.Engine.run(Engine.java:36)
        at jkind.engines.SolverBasedEngine.run(SolverBasedEngine.java:37)
        at java.lang.Thread.run(Unknown Source)

lgwagner commented 3 years ago

Hi Tim.

I will take a look this ASAP. Can you send / attach a model that produces this or is it simply any operation that involve non-constant division?

TimArnettThales commented 3 years ago

It appears to be any non-constant division. I just replicated it with Z3 v4.8.8 also. Here's an example that causes it.

node main() returns ();

var
    a : real;
    b : real;
    div_test : real;
    phi1 : bool;

let

    b = 2.0 -> pre(b) + 0.01;
    a = 0.0 -> pre(a) + 0.01;
    div_test = a/b;

    phi1 = (div_test <= a);
    --%PROPERTY phi1;
tel;

lgwagner commented 3 years ago

This issue is finally fixed. Thank you for your patience. I will generate a new release once I fix your other issue.

loonwerks / jkind

Z3 parse error during division #63