Resolve "Correctly model state without next"
Issue #36 :
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.
States that do not have a 'next' should now be updated at the end of the loop.