kindse: implement a simple invariant generation
Just check that a safe relation is inductive and if so, put it as an invariant into the program.
Loading
Please sign in to comment
Just check that a safe relation is inductive and if so, put it as an invariant into the program.