DEFABBREV : IF, An ACL2 Solution DEFABBREV Solution Define MY-IF as DEFABBREV macro Disable during symbolic simulation Controls case splitting Expands to a generic IF statement in simulator Efficient in-line IF execution Might be usable over STOBJ objects (?) See Demonstration