Trying basic ‘TotalSupplylsSumOfBalances’ invariant on WETH9 and got this error ‘invariant violated in post state’, but with no more info ?

constructor is empty, so no balance can be set > 0 , so no reason to violate the invariant

Trying basic ‘TotalSupplylsSumOfBalances’ invariant on WETH9 and got this error ‘invariant violated in post state’, but with no more info ?

constructor is empty, so no balance can be set > 0 , so no reason to violate the invariant

Hey @zapaz,

It seems that `totalSupply()`

, which is the ETH balance of the contract, is initialized with an arbitrary value (which is not a storage value), therefore your invariant, implying equality is trivially violated since the contract can start with an ETH balance before the constructor.

so how to say in CVL that totalSupply() is initially equal to 0 ?

something like for ghost function ?

```
ghost sum() returns uint256 {
init_state axiom sum() == 0;
}
```

is this available for real function ?

AFAIK, no. so the simplest way is to rewrite it as a rule, thus there is no instate check for invariant.

ok thanks, rule only