| Mon, 06 Dec 2010 11:25:21 +0100 | blanchet | have SMT solvers report the number of facts that they should have by default in Sledgehammer -- the information might not seem to belong there but it also belongs nowhere else, for how is Sledgehammer to know how different solvers deal with hundreds of facts? | changeset | files |
| Mon, 06 Dec 2010 10:32:39 +0100 | blanchet | return all facts for CVC3 and Yices, since there is no proof parsing / unsat core extraction | changeset | files |
| Mon, 06 Dec 2010 10:31:29 +0100 | blanchet | trust SMT filter's timeout -- nested timeouts seem to be at the origin of spontaneous Interrupt exceptions in some cases | changeset | files |
| Mon, 06 Dec 2010 10:23:31 +0100 | blanchet | reraise interrupt exceptions | changeset | files |
| Mon, 06 Dec 2010 09:54:58 +0100 | blanchet | [mq]: sledge_binary_minimizer | changeset | files |
| Mon, 06 Dec 2010 10:52:48 +0100 | bulwahn | correcting usage documentation in mirabelle tool | changeset | files |