Same as svl-run-phase but without guards
(svl-run-phase-wog modname inputs delayed-env modules) → (mv * *)
Please see svl-run-phase for the explanation of the arguments. svl-run-phase-wog has the same functionality as svl-run-phase but it does not have any guards. This can help makes the rewrite-based proof go faster because guards might be executed too many times during such proofs.