ethereum/act

Invariants ignored by `prove`

leonardoalt opened this issue · 2 comments

constructor of LValue
interface constructor()

creates
	uint x := 0
	uint y := 2

invariants
	x == 0
	y == 2

behaviour f of LValue
interface f()

storage
	x => 0
	y => 2

Also not sure what the expected behavior here is, but I get:

$ ./result/bin/act prove --file lvalue.act

============

Invariant "(LValue.x == 0)" of "LValue": Q.E.D

Shouldn't y == 2 also be proved? Or am I missing something?

d-xo commented

hmmmm I just ran this with current master and it seems to be proving both of them on my machine. Can you still reproduce this @leonardoalt?

============

Invariant "(LValue.x == 0)" of "LValue": Q.E.D ✨

============

Invariant "(LValue.y == 2)" of "LValue": Q.E.D ✨
d-xo commented

Fixed by #80