| 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 |