Rewrite-if-avoid-swap
Control rewriter's swapping of branches of IF calls
This topic concerns an advanced control for the ACL2 prover.
By default, the ACL2 rewriter may swap true and false branches of a call of
IF, in particular when the test is a call of NOT. Attach the
function constant-t-function-arity-0 to defeat this behavior. Attach the
function constant-nil-function-arity-0 to restore the default
behavior.
