Predicate Guards::Internal::asserts

Holds if assertion a directly asserts that expression e evaluates to value v.

predicate asserts(Assertion a, Expr e, AbstractValue v)