Add rd frames to Satisfiability Op (via x~ = x).
Updated test results with frame rd conditions.
Satisfiability predicate now takes invariant into account.