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

Z3-related crash regarding parsing Solver output #45

Closed lgwagner closed 6 years ago

lgwagner commented 6 years ago

JKind is crashing on the provided example model (you will have to unzip error.zip and run error.lus to reproduce the error.

jkind -solver z3 -smooth -no_slicing error.lus

This produces the following error:

image

This is using JKind version 4.0.1 and Z3 4.7.1. The error was reproduced on JKind 4.0.1 and Z3 4.6.0 and 4.6.2.

error.zip

agacek commented 6 years ago

Thanks!