DEFABBREV : IF, The JEM1 Solution JEM1 model uses special MY-IF functions Guarded to select between two integers Disabled during symbolic simulation Dual mode JEM1 model used to addresses efficiency issue ACL2 : expands to a guarded IF statement GCL : replaced with inline C selector "under-the-hood" Still must rewrite portions of model MY-IF is not STOBJ compliant Manually demote IF selecting actions over state May be a configuartion issue