hackish more powerful smt rule
unreasonable assert
hack to get nobacktrack rules to be "free" in the proof tree exploration
raise timeout for symexe
move Symexec.specialize_spec to Core.specialize_spec

This way it can be used by clients. It may be useful for them to know how specs
are specialized. It's used in llStar. Otherwise clients need to reimplement
this function.
move ops from {core,calculus} to {coreOps, calculusOps}
added CalculusOps.vars_of_{sequent,sequent_schema,...}

to be used soon
well-formedness checks for rule schemas
add Corestar_std.pair_map
freshen free logical variables when applying rule schemas
Only show applied prover rules in debug
No penalty for large LHS when doing frame inference
Allow more than one formula pattern variable in patterns
Revert "Allow more than one formula pattern variable in patterns"

This reverts commit 9f2dbfb7d2bfb076c1522c12a4b9bdc0d446aedb.
handle matching * expressions at any level in formulas
fix previous commit
* is now an n-ary operator

Actually, it's several operators, one for each arity, since Z3 does not
directly support n-ary functions.  This is all abstracted by Syntax already
anyway, so it doesn't change much for the rest of the code! The only places
where one has to be careful is when testing whether two function declarations
represent the same operation, as comparing them with Z3.FuncDecl.equal is not
enough anymore: for a star of arity 2 vs a star of arity 3, Z3.FuncDecl.equal
would return false. One can use Syntax.is_star_op to deal with these cases.
on_op recognises * with different arities too
only pattern vars can be matched in [find_pattern_matches]
Debug.prof_fun5 and Debug.prof_fun6

this might be getting out of hands... oh, well, let's worry when we get
to prof_fun1000.