Implement support for crucible_fresh_var in final states

[atomb]

Building on #179 (and probably #180), implement support for executing overrides that use crucible_fresh_var after crucible_execute_func (i.e., in the final state). This can be used in conjunction with crucible_points_to to indicate that the function writes some unknown value as a a side effect. It should also be possible to do something like:

r <- crucible_execute_func [...];
x <- crucible_fresh_var ...;
crucible_equal r (crucible_term x);

This would assert that the function returns some unknown value. This could, of course, be packaged up into a reusable function, as it's a bit verbose to include verbatim every time.