Predicate signature LangSig::additionalBoundFlowStep
Holds if e2 >= e1 + delta
(if upper = false
) or e2 <= e1 + delta
(if upper = true
).
signature predicate additionalBoundFlowStep(Expr e2, Expr e1, Delta delta, boolean upper)
Holds if e2 >= e1 + delta
(if upper = false
) or e2 <= e1 + delta
(if upper = true
).
signature predicate additionalBoundFlowStep(Expr e2, Expr e1, Delta delta, boolean upper)