Skip to content

Resolve "Correctly model state without next"

Salih Ates requested to merge 36-model-state-without-next into main

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.

Merge request reports