Open
Description
Here's an example:
#lang ivy1.7
type obj = struct {
s : bool
}
individual my_obj: obj
after init {
my_obj.s := false;
}
export action act = {
var o:obj;
o.s := *;
}
invariant my_obj.s = false
The invariant breaks when it should not.
Metadata
Metadata
Assignees
Labels
No labels