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 |