Correctly model state without next
According to the Btor2 paper:
A state variable without associated next function is treated as a primary input, i.e., it has the same behaviour as inputs defined via keyword input.
Currently, Btor2C does not model this correctly.
For such a state without next
:
- If
init
of the state is given, Btor2C initialize the state with the given value. - Btor2C does not havoc the value of the state at the end of the loop. Therefore the value stays the same after initialization.