take return values into account when computing modifies

This fixes a bug where coreStar would require a function with return
arguments to have them in the modifies clause of their specs to verify
correct.

Also, when inferring specs, we now remove the return variables from the
inferred modifies clause.

Added regression tests for both of these bugs.
pretty-print returns and params in specs and assgn
minor code factorisation