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

K-induction fails with SMTInterpol Exception #58

Closed mgudemann closed 3 years ago

mgudemann commented 4 years ago

For the attached Lustre program, current jkind (1f836bb08bc66256233fef4ee1a92e8c6a04592d) fails with

++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++                            
UNKNOWN PROPERTIES: [prop] || True for 17 steps || Time = 6.941s                          
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

    -------------------------------------                                
    --^^--        SUMMARY          --^^--       
    -------------------------------------           

UNKNOWN PROPERTIES: [prop]

k-induction process failed
de.uni_freiburg.informatik.ultimate.logic.SMTLIBException: Undeclared function symbol (ite Bool Real Int)
        at de.uni_freiburg.informatik.ultimate.logic.NoopScript.term(NoopScript.java:321)
        at de.uni_freiburg.informatik.ultimate.logic.NoopScript.term(NoopScript.java:296)
        at jkind.solvers.smtinterpol.SmtInterpolUtil.convert(SmtInterpolUtil.java:83)
        at jkind.solvers.smtinterpol.SmtInterpolUtil.convert(SmtInterpolUtil.java:64)
        at jkind.solvers.smtinterpol.SmtInterpolUtil.convert(SmtInterpolUtil.java:81)
        at jkind.solvers.smtinterpol.SmtInterpolUtil.convert(SmtInterpolUtil.java:64)
        at jkind.solvers.smtinterpol.SmtInterpolUtil.convert(SmtInterpolUtil.java:81)
        at jkind.solvers.smtinterpol.SmtInterpolUtil.convert(SmtInterpolUtil.java:64)
        at jkind.solvers.smtinterpol.SmtInterpolUtil.convert(SmtInterpolUtil.java:81)
        at jkind.solvers.smtinterpol.SmtInterpolUtil.convert(SmtInterpolUtil.java:64)
        at jkind.solvers.smtinterpol.SmtInterpolUtil.convert(SmtInterpolUtil.java:81)
        at jkind.solvers.smtinterpol.SmtInterpolUtil.convert(SmtInterpolUtil.java:64)
        at jkind.solvers.smtinterpol.SmtInterpolUtil.convert(SmtInterpolUtil.java:81)
        at jkind.solvers.smtinterpol.SmtInterpolUtil.convert(SmtInterpolUtil.java:64)
        at jkind.solvers.smtinterpol.SmtInterpolUtil.convert(SmtInterpolUtil.java:81)
        at jkind.solvers.smtinterpol.SmtInterpolUtil.convert(SmtInterpolUtil.java:64)
        at jkind.solvers.smtinterpol.SmtInterpolUtil.convert(SmtInterpolUtil.java:81)
        at jkind.solvers.smtinterpol.SmtInterpolUtil.convert(SmtInterpolUtil.java:64)
        at jkind.solvers.smtinterpol.SmtInterpolUtil.convert(SmtInterpolUtil.java:81)
        at jkind.solvers.smtinterpol.SmtInterpolUtil.convert(SmtInterpolUtil.java:64)
        at jkind.solvers.smtinterpol.SmtInterpolUtil.convert(SmtInterpolUtil.java:81)
        at jkind.solvers.smtinterpol.SmtInterpolUtil.convert(SmtInterpolUtil.java:64)
        at jkind.solvers.smtinterpol.SmtInterpolUtil.convert(SmtInterpolUtil.java:58)
        at jkind.solvers.smtinterpol.SmtInterpolSolver.convert(SmtInterpolSolver.java:168)
        at jkind.solvers.smtinterpol.SmtInterpolSolver.assertSexp(SmtInterpolSolver.java:46)
        at jkind.engines.KInductionEngine.assertInvariants(KInductionEngine.java:126)
        at jkind.engines.KInductionEngine.assertNewInvariants(KInductionEngine.java:121)
        at jkind.engines.KInductionEngine.handleMessage(KInductionEngine.java:180)
        at jkind.engines.messages.InvariantMessage.accept(InvariantMessage.java:22)
        at jkind.engines.messages.MessageHandler.handleMessage(MessageHandler.java:30)
        at jkind.engines.messages.MessageHandler.processMessagesAndWaitUntil(MessageHandler.java:38)
        at jkind.engines.KInductionEngine.processMessagesAndWait(KInductionEngine.java:62)
        at jkind.engines.KInductionEngine.main(KInductionEngine.java:49)
        at jkind.engines.Engine.run(Engine.java:36)
        at jkind.engines.SolverBasedEngine.run(SolverBasedEngine.java:37)
        at java.lang.Thread.run(Thread.java:748)

catching the error and printing the Sexp gives

(not (<= (+ (ite false (/ (/ 0 1) (/ 1 1)) (ite $f_t0$0 (+ $p12$0 (/ (/ (- 0 94) 1) (/ 1 1))) (ite $f_t5$0 (+ $p12$0 (/ (/ (- 0 94) 1) (/ 1 1))) (ite $f_t6$0 (+ $p12$0 (/ (/ (- 0 1) 1) (/
1 1))) (ite $f_t7$0 (+ $p12$0 (/ (/ (- 0 1) 1) (/ 1 1))) (ite $f_t2$0 (+ $p12$0 (/ (/ 1 1) (/ 1 1))) (ite $f_t6$0 (+ $p12$0 (/ (/ 1 1) (/ 1 1))) $p12$0))))))) (/ (/ 1 1) (/ 1 1))) (/ (/ 0
1) (/ 1 1))))

problem.zip

lgwagner commented 3 years ago

I apologize for the long delay in addressing this. I have updated the JAR of SMTInterpol to the latest and this error is resolved. I'm currently running regression. Look for a new release in a day or two to address.

I will formally close this issue when the release is issued.

mgudemann commented 3 years ago

@lgwagner great, thanks!