true story...
added Corestar_std.pp_pair

I needed it during some debugging and figured it can stay
circumvent bug in Z3 binding where arguments get reversed

Specifically, Z3.Expr.get_args returns arguments in the reverse order,
so that
  Z3.FuncDecl.apply (Z3.Expr.get_func_decl e) (Z3.Expr.get_args e))
is different from e (and indeed most of the time ill-typed!).

See https://z3.codeplex.com/workitem/106 .
don't throw an error on formula variables
only guess well-typed instantiations

Expressions with different types are not good guesses, and moreover Z3
is not happy with building e = f with e and f of different types.
fixed a bug in Prover.inline_pvars_rule

There were still cases where inline_pvars_rule would incorrectly fire
without making progress (good thing we have that check in
Prover.solve!).

If we have v = p1 * v = p2 in the formula, then v appears twice but not
progress is achieved by substituting. The previous criterion for
usefulness was that v appears at least twice in the formula. Instead, we
have to make sure that v appears more times in the formula than the
numer of times it appears as v = p.
really take assoc of * into account when matching

The current implementation was broken because we used the binary
on_star. This prevents matching from working correctly.

The function on_big_star has made a reappearance. It's been rewritten
differently because the previous one was buggy (it would only descend
into right arguments of *). Perhaps it should use unfold instead but I
couldn't figure out how.

The find_matches complexity has been restored to its former exponential
glory (in the size of the concrete formula to match). This function
should probably be rewritten not to be exponential, since formulas can
grow very large, which makes this a serious issue.

The only way I can see around this would be to stop allowing ?f patterns
at the top level (which require all *-splittings to be explored, of
which there is an exponential number), or perhaps allow only one, which
would then have to be treated very specially (it gets the frame once the
rest of the pattern has been matched). Maybe there was another intent
that I'm missing and find_matches is not supposed to be of exponential
complexity in the first place. Thoughts?
handle emp as the neutral element of * when matching

This is to match a * b against a non-* formula c: rewrite c as c * emp
and continue.

It is possible that this breaks some invariant of find_matches as we
change the formula in the middle of execution. I don't think so because
this triggers only when we are still matching * on the pattern, so
around the beginning.

This would not be needed if we did not require patterns of the form
a * ?f and made sure that the pattern does not contain some * emp.
does less expensive matching first to detect non-matches early
no point verifying "where" clauses if the pattern did not match