Hi,

I’m trying to check my understanding of `invariant`

and `requireInvariant`

but hitting a roadblock. Here’s the scenario:

I have two simple contracts, `First.sol`

and `Second.sol`

. Here is the code:

First.sol

```
// SPDX-License-Identifier: MIT
pragma solidity 0.8.0;
import "./Second.sol";
contract First is Second {
uint256 valueFirst;
function changeValue(uint256 valueX) external {
valueFirst = valueX + valueSecond;
}
}
```

And,

Second.sol

```
// SPDX-License-Identifier: MIT
pragma solidity 0.8.0;
contract Second {
uint256 valueSecond;
constructor() {
valueSecond = 52;
}
function getValueSecond() external view returns(uint256) {
return valueSecond;
}
}
```

I want to verify that the `valueSecond`

variable always has a value of 52. So, here’s my `Multi.spec`

:

```
using Second as sec
methods {
sec.getValueSecond() returns(uint256) envfree;
}
invariant valueSecond_is_constant()
sec.getValueSecond() == 52
rule arbitRule(env e, uint256 x) {
requireInvariant valueSecond_is_constant();
changeValue(e, x);
assert sec.getValueSecond() == 52, "valueSecond changed!";
}
```

And I run this via -

```
certoraRun contracts/Multi/First.sol contracts/Multi/Second.sol \
--verify First:specs/Multi/Multi.spec \
--solc solc \
--msg "Multi_Invariant_Spec_Style1"
```

The Prover fails saying **valueSecond_is_constant_instate → invariant violated in post-state**

Can someone help me understand what am I missing? Any help or pointers would be much appreciated!

Thanks