Hi Marc and everyone else reading this,
When I discovered the problem, it seemed to me that liveness checking
simply didn't work in simulation mode and I didn't bother recording
the examples on which I tried it. Now, we've been unable to reproduce
the problem. We'd appreciate it if people could try using simulation
mode to check a model specifying a liveness property and let us know
what happens.
Leslie