The implementation of stepBack does not take into account the pre and post assignments.
Created attachment 135 [details]
When generating a concrete trace (option -t0 of verifyta) to location l, the necessary delay of 20 is not generated.
Fixed on the trunk from rev. 2877.
Fixed on the 4.0 branch from rev. 2878.