Why Primed Variables

Let's see if we can clear things up: A primed variable is, basically, a variable with an ' at the end of its name. That is, the primed version of the variable x is the variable x'. Usually, they are used to distinct current values of variables from the ones in the next state of the system.

Consider the transition x:=x+1, if executed in a state where x=2. We want to use Z3 to compute the next value of x. However, we can not simply use a conjunction: x = 2 & x = x+1 is false. To work around this issue, we use the primed version of x to denote the value in the next state: x = 2 & x' = x+1 is satisfiable and x' receives the values 3 as intended. The ' is later removed when a new state is constructed (see stateFromModel).