bugfixes in prover, caused by previous merge

also, better profiling output
small performance fix

The change is necessary because Z3 substitutions reverse the
order of arguments of 'distinct'.
some speed improvements

(done with Jules&Rasmus)
preparing for rules that disprove the goal

(with NikosT)
added, but not activated smt_disprove rule

comment: the rule is inactive because it makes things slower :(
some very weird profiling results need to be sorted


also

1. Removed Smt.rewrite_star_to_and. Instead, we just tell Z3 that
star is the same as conjunction. As a bonus, we now do so only when
we shipped only pure stuff. (The purity checks should be cached in
the future, because they are now very frequent.)

2. Syntax.is_pure now handles quantifiers.

3. Some catching of Z3native.Exception, to get around what appear to
be rough edges of the Z3 interface. See
  https://z3.codeplex.com/workitem/101
and
  https://z3.codeplex.com/workitem/102

4. Better profiling. Handles functions that raise exceptions.
renamed some pp_* to print_* where appropriate

pp_* looks like it could be used as formatter. print_* looks like it
prints.

Conflicts:
	src/prover/prover.ml
	src/utils/debug.ml
typos
fixed a few non-optimised things

This makes coreStar slightly faster

Conflicts:
	src/prover/prover.ml
well-formedness checks

(it checks well-formedness)
of questions
Merge branch 'alt-abd' of github.com:seplogic/corestar into alt-abd
handle argument lists of mismatched lengths

and some small fixes
(with Jules, NikosT, Rasmus)
hacky fix to parse string constants as integer sorts

This is required to let Z3 know that all strings are different when
calling SMT. The parser only knows about ints and bools, because we do
not want type annotations in the .star files just yet. In particular,
this prevents the parser from using a third sort "string".

Before this fix, the examples involving strings did not pass correctly
because the parser interpreted them as integers (to get well-typed
expressions), but the prover only acts on strings of sort String.

Now strings are of sort Integer, in accordance with the parser.
change in notations: @ for globals, % for locals, ^ for vpats

Syntax.var is now an abstract type, use Syntax.var_name to get the name
of a variable (without the identifying first character!).

This hides the internals of coreStar to clients, which do not have to
worry about following coreStar's conventions for variable names. Also,
looking at the first character is probably more efficient than matching
regular expressions, but maybe not given OCaml's awkward string
manipulation library.

It looks like global/local program variable distinction is not used
anywhere in coreStar yet, but it's now made more explicit (pvar split
into plvar and pgvar).

Tests painfully adapted to the new syntax.

Feel free to comment/revert.
bumped Z3's version number

This version is incompatible with the previous version of Z3.

You'll need to reinstall Z3, eg using scripts/install_z3.sh.
added Z3's SMT statistics to the profiling output
added Syntax.mk_fresh_lvar

This is convenient for clients such as llStar
updated test generator

the global variable is now called @s
(see 0fc76b0eea24)
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