Remove an obsolete fixme
Do not allow sbv 2.10 yet

This might be relying on an unreleased z3 version?  Couldn't get
it to work.  2.9 is more than sufficient.
More refined handling of output parameters

Reading the value of a pointer makes it an input parameter.  Example:

> if(p)
>   *p = 0;

The main idea is that conditions on pointer values allow the user to
choose what code is being executed, and we don't want to automatically
choose for them.  This is especially important in the presence of
guarded side effects (imagine if there was a call on the RHS on the
assignment).

This change also introduces a flag to enable a "hack" behavior where
we allow the code above to report @p@ as an output parameter because
there are no other side effects in the guarded branch.
Handle aliased actual arguments

Includes a description and test case
Include support for in/out parameters in actual argument handling
Tests and tweaks for the output parameter analysis

These tests are for commit 1280682002f7214c70ef6065fcc641e69ae647f1.
This splits the test suite into normal tests and tests for the
trivial block hack.