Fix (I hope) PULSE model nondeterminism

I should have checked this list of side-effect functions
much earlier, but ... EBRAINTOOSMALL.  I hope that these
changes will help avoid the evil nondeterminism that I've
seen with shrinking PULSE model counterexamples.