more explicit explanation of init_component shell function;

paranoia export of CLASSPATH, just in case the initial status via allexport is lost due to other scripts;

tuned message;

post raw messages last, to ensure that result has been handled by session actor already (e.g. to avoid race between Session.session_actor and Session_Dockable.main_actor);

more reasonably defaults for typical laptops (2 GB RAM, 2 cores); enforce -server JVM if possible (NB: default JRE on Windows lacks that);

added forall2 predicate lifter

merged

merged

renamed SMT failure: Abnormal_Termination is indeed more appropriate than Solver_Crashed

honour timeouts which are not rounded to full seconds

better error message

better error message

merged

cosmetics

interpret SMT_Failure.Solver_Crashed correctly

turn on Sledgehammer verbosity so we can track down crashes

pick up SMT solver crashes and report them to the user/Mirabelle if desired

merged

only replace unknowns of type nat with known integer numbers, don't alias unknown values in Z3's counterexamples with known integers

trace more solver output before raising an exception due to a non-zero return code (avoids truncating potential counterexamples produced by Z3)

merged

ignoring the constant STR in the predicate compiler

non-executable source files;

eliminated old-style sed in favour of builtin regex matching;

more robust treatment of spaces in file names;

tuned error messages;

merged

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