more robust determination of java executable;

init_component: require absolute path (when invoked by user scripts);

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;