| Sat, 13 Nov 2010 12:32:21 +0100 |
wenzelm |
back to quick_and_dirty, which is still practically important since the scheduler does not jump over subproofs;
|
changeset |
files
|
| Sat, 13 Nov 2010 11:41:02 +0100 |
wenzelm |
await_cancellation in the main thread, independently of the execution futures, which might get interrupted or be absent after node deletetion;
|
changeset |
files
|
| Sat, 13 Nov 2010 00:24:41 +0100 |
wenzelm |
updated README;
|
changeset |
files
|
| Fri, 12 Nov 2010 21:37:01 +0100 |
wenzelm |
defensive defaults for more robust experience for new users;
|
changeset |
files
|
| Fri, 12 Nov 2010 17:44:03 +0100 |
wenzelm |
merged
|
changeset |
files
|
| Fri, 12 Nov 2010 15:56:11 +0100 |
boehmes |
preliminary support for newer versions of Z3
|
changeset |
files
|
| Fri, 12 Nov 2010 15:56:10 +0100 |
boehmes |
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
|
changeset |
files
|
| Fri, 12 Nov 2010 15:56:08 +0100 |
boehmes |
let the theory formally depend on the Boogie output
|
changeset |
files
|
| Fri, 12 Nov 2010 15:56:07 +0100 |
boehmes |
look for certificates relative to the theory
|
changeset |
files
|
| Fri, 12 Nov 2010 15:56:06 +0100 |
boehmes |
dropped numerals from monomorphization blacklist (only particular numerals are builtin, all other numerals should be treated uninterpreted), this blacklist should contain only truely polymorphic builtin constants supported by SMT
|
changeset |
files
|
| Fri, 12 Nov 2010 06:11:29 -0800 |
huffman |
merged
|
changeset |
files
|
| Fri, 12 Nov 2010 06:05:26 -0800 |
huffman |
update Theory.requires with new theory name
|
changeset |
files
|
| Fri, 12 Nov 2010 14:51:28 +0100 |
wenzelm |
tuned signatures;
|
changeset |
files
|
| Fri, 12 Nov 2010 14:06:37 +0100 |
wenzelm |
never open Unsynchronized;
|
changeset |
files
|