| Thu, 10 Feb 2011 16:15:43 +0100 | blanchet | run all provers in blocking mode, even if a proof was already found -- this behavior is less confusing to the user | changeset | files |
| Thu, 10 Feb 2011 16:05:33 +0100 | blanchet | remove pointless clutter | changeset | files |
| Thu, 10 Feb 2011 10:09:38 +0100 | blanchet | make minimizer verbose | changeset | files |
| Wed, 09 Feb 2011 17:18:58 +0100 | blanchet | tuning | changeset | files |
| Wed, 09 Feb 2011 17:18:58 +0100 | blanchet | automatically minimize Z3-as-an-ATP proofs (cf. CVC3 and Yices) | changeset | files |
| Wed, 09 Feb 2011 17:18:58 +0100 | blanchet | renamed field | changeset | files |
| Wed, 09 Feb 2011 17:18:58 +0100 | blanchet | added "Z3 as an ATP" support to Sledgehammer locally | changeset | files |
| Wed, 09 Feb 2011 17:18:57 +0100 | blanchet | remove Z3 wrapper script, which is no longer necessary now that the SMT module generates SMT-LIB compliant files | changeset | files |