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

Arithmetic Exception #47

Closed lgwagner closed 6 years ago

lgwagner commented 6 years ago

Attached model exercises an arithmetic exception.

Solver = Z3 (4.7.1) JKind (latest commit from master, em in an Eclipse tool)

error.txt error_image

lgwagner commented 6 years ago

Hmmm...nevermind. I believe we discussed this quite some time ago. I think back then you told me there was nothing to consider.

agacek commented 6 years ago

Yes, nonlinear is a bit of a pain. In particular, if you divide by zero, the SMT solver treats the result as arbitrary. That means we are not able to simulate any counterexamples with division by zero. I think the best workaround is to ensure that the variables you divide by are never zero (either through assertion or other means that are sound for your problem).

That said, JKind should produce a better message in this case.

On Fri, Sep 14, 2018 at 4:08 PM Lucas Wagner notifications@github.com wrote:

Closed #47 https://github.com/agacek/jkind/issues/47.

— 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/47#event-1847047197, or mute the thread https://github.com/notifications/unsubscribe-auth/AAKgiHs7bOTFFr23U4iBn5oePAikg10mks5ubBrhgaJpZM4Wp7rj .