Module Pulselib.PulseEternal

implies lhs rhs is true if there is a renaming σ of abstract values in rhs.current_state such that lhs.current_state ⊢ σ(rhs.current_state) ∧ σ(lhs.path_condition). Assuming lhs is the analysis state after going through a loop body and rhs is the state before, this tests whether it is possible to satisfy the loop conditions again. If so, following the UNTER theory, an infinite loop is detected.