re-generalized type of option_rel and sum_rel (accident from 2989f9f3aa10)

re-generalized type of prod_rel (accident from 2989f9f3aa10)

formal dependency on b2i files

merged

check the return code of the SMT solver and raise an exception if the prover failed

updated README;

tuned;

cover 'write' as primitive proof command;

clarified interact/print state: proof commands are treated as in TTY mode to get full response;

somewhat adhoc replacement for 'thus' and 'hence'; complete words as short as 2 characters, e.g. "Un";

always print state of proof commands (notably "qed" etc.);

simplified message: malformed symbols are fully internalized, i.e. can be printed without crashing;

tuned message;

proper escape in regex;

report malformed symbols;

qualified Symbol_Pos.symbol;

total Symbol.source;

eliminated slightly odd pervasive Symbol_Pos.symbol;

treat Unicode "replacement character" (i.e. decoding error) is malformed;

simplified/robustified treatment of malformed symbols, which are now fully internalized (total Symbol.explode etc.); allow malformed symbols inside quoted material, comments etc. -- for improved user experience with incremental re-parsing; refined treatment of malformed surrogates (Scala);

tuned;

back to quick_and_dirty, which is still practically important since the scheduler does not jump over subproofs;

await_cancellation in the main thread, independently of the execution futures, which might get interrupted or be absent after node deletetion;

updated README;

defensive defaults for more robust experience for new users;

merged

preliminary support for newer versions of Z3

turned SMT counterexamples into verbose messages (they had been swallowed before, following the state of smt_trace -- which is off by default), because they might be useful for the user

let the theory formally depend on the Boogie output

look for certificates relative to the theory