pub fn instantiate_transition(expr: &VerifyExpr, step: u32) -> VerifyExprExpand description
Instantiate a transition relation: replace @t with @{step} and @t’ with @{step+1}.
pub fn instantiate_transition(expr: &VerifyExpr, step: u32) -> VerifyExprInstantiate a transition relation: replace @t with @{step} and @t’ with @{step+1}.