Atc-valuep-rules
Rules for discharging valuep hypotheses.
Some symbolic execution rules have hypotheses saying that
certain terms are values, i.e. satisfy valuep.
These are discharged by backchaining to
the fact that those terms satisfy specific value predicates,
such as sintp.