Switched to using explicit postcondition instead of Φ, changed files accordingly. Works nicer and is probably faster.