It would be nice to warn developers when they could use a constant instead of a variable. It is possible to go quite far in this but checking whether a variable only has one initial value and is only assigned to itself or not assigned at all would already be a nice addition. The change from a variable to a constant might seem small but it can have a huge impact on the synthesis performance, given the right circumstances. For example, the following cif code was part of a larger model: ``` disc bool recovery = false; location: initial; marked; edge call do state := Busy; edge callback do state := done; edge trigger_done do state := not_done; edge reset do state := if recovery = false: not_done else state end; ``` Changing recovery to be a constant instead of a variable changed the synthesis from running out of memory to being done within seconds.