| Mon, 15 Nov 2010 18:56:31 +0100 |
blanchet |
interpret SMT_Failure.Solver_Crashed correctly
|
changeset |
files
|
| Mon, 15 Nov 2010 18:56:30 +0100 |
blanchet |
turn on Sledgehammer verbosity so we can track down crashes
|
changeset |
files
|
| Mon, 15 Nov 2010 18:56:29 +0100 |
blanchet |
pick up SMT solver crashes and report them to the user/Mirabelle if desired
|
changeset |
files
|
| Mon, 15 Nov 2010 18:04:04 +0100 |
boehmes |
merged
|
changeset |
files
|
| Mon, 15 Nov 2010 17:52:48 +0100 |
boehmes |
only replace unknowns of type nat with known integer numbers, don't alias unknown values in Z3's counterexamples with known integers
|
changeset |
files
|
| Mon, 15 Nov 2010 17:35:57 +0100 |
boehmes |
trace more solver output before raising an exception due to a non-zero return code (avoids truncating potential counterexamples produced by Z3)
|
changeset |
files
|
| Mon, 15 Nov 2010 17:04:53 +0100 |
bulwahn |
merged
|
changeset |
files
|
| Mon, 15 Nov 2010 13:40:12 +0100 |
bulwahn |
ignoring the constant STR in the predicate compiler
|
changeset |
files
|
| Mon, 15 Nov 2010 17:40:38 +0100 |
wenzelm |
non-executable source files;
|
changeset |
files
|
| Mon, 15 Nov 2010 17:39:23 +0100 |
wenzelm |
eliminated old-style sed in favour of builtin regex matching;
|
changeset |
files
|
| Mon, 15 Nov 2010 17:14:43 +0100 |
wenzelm |
more robust treatment of spaces in file names;
|
changeset |
files
|
| Mon, 15 Nov 2010 15:41:58 +0100 |
wenzelm |
tuned error messages;
|
changeset |
files
|
| Mon, 15 Nov 2010 14:59:53 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Mon, 15 Nov 2010 14:59:21 +0100 |
haftmann |
re-generalized type of option_rel and sum_rel (accident from 2989f9f3aa10)
|
changeset |
files
|
| Mon, 15 Nov 2010 14:14:38 +0100 |
haftmann |
re-generalized type of prod_rel (accident from 2989f9f3aa10)
|
changeset |
files
|
| Mon, 15 Nov 2010 00:20:36 +0100 |
boehmes |
formal dependency on b2i files
|
changeset |
files
|
| Sun, 14 Nov 2010 23:55:25 +0100 |
boehmes |
merged
|
changeset |
files
|
| Fri, 12 Nov 2010 17:28:43 +0100 |
boehmes |
check the return code of the SMT solver and raise an exception if the prover failed
|
changeset |
files
|
| Sun, 14 Nov 2010 17:33:28 +0100 |
wenzelm |
updated README;
|
changeset |
files
|
| Sun, 14 Nov 2010 15:25:01 +0100 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 14 Nov 2010 15:21:49 +0100 |
wenzelm |
cover 'write' as primitive proof command;
|
changeset |
files
|
| Sun, 14 Nov 2010 14:05:08 +0100 |
wenzelm |
clarified interact/print state: proof commands are treated as in TTY mode to get full response;
|
changeset |
files
|
| Sat, 13 Nov 2010 22:33:07 +0100 |
wenzelm |
somewhat adhoc replacement for 'thus' and 'hence';
|
changeset |
files
|
| Sat, 13 Nov 2010 21:46:24 +0100 |
wenzelm |
always print state of proof commands (notably "qed" etc.);
|
changeset |
files
|
| Sat, 13 Nov 2010 21:01:03 +0100 |
wenzelm |
simplified message: malformed symbols are fully internalized, i.e. can be printed without crashing;
|
changeset |
files
|
| Sat, 13 Nov 2010 20:49:02 +0100 |
wenzelm |
tuned message;
|
changeset |
files
|
| Sat, 13 Nov 2010 20:20:05 +0100 |
wenzelm |
proper escape in regex;
|
changeset |
files
|
| Sat, 13 Nov 2010 20:13:35 +0100 |
wenzelm |
report malformed symbols;
|
changeset |
files
|
| Sat, 13 Nov 2010 20:06:52 +0100 |
wenzelm |
qualified Symbol_Pos.symbol;
|
changeset |
files
|
| Sat, 13 Nov 2010 19:55:45 +0100 |
wenzelm |
total Symbol.source;
|
changeset |
files
|