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

PDR soundness bug with assertions #43

Closed agacek closed 6 years ago

agacek commented 6 years ago

PDR handles assertions in an unsound way. The following property should be false but PDR proves it.

node main(x : bool) returns ();
let
  assert true -> pre x;
  --%PROPERTY x;
tel;