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

Report invariants used #8

Closed agacek closed 11 years ago

agacek commented 11 years ago

It would be nice if JKind had an option to report the invariant lemmas which were necessary to prove a given property. This would require extra checking (removing unused lemmas) but could be very useful for users.

agacek commented 11 years ago

Added -reduce_inv flag in 12319336cd68023e061ca73ff2f96cc4e7855385