Mon, 06 Dec 2010 11:25:21 +0100 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?
blanchet [Mon, 06 Dec 2010 11:25:21 +0100] rev 40981
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?
Mon, 06 Dec 2010 10:32:39 +0100 return all facts for CVC3 and Yices, since there is no proof parsing / unsat core extraction
blanchet [Mon, 06 Dec 2010 10:32:39 +0100] rev 40980
return all facts for CVC3 and Yices, since there is no proof parsing / unsat core extraction
Mon, 06 Dec 2010 10:31:29 +0100 trust SMT filter's timeout -- nested timeouts seem to be at the origin of spontaneous Interrupt exceptions in some cases
blanchet [Mon, 06 Dec 2010 10:31:29 +0100] rev 40979
trust SMT filter's timeout -- nested timeouts seem to be at the origin of spontaneous Interrupt exceptions in some cases
Mon, 06 Dec 2010 10:23:31 +0100 reraise interrupt exceptions
blanchet [Mon, 06 Dec 2010 10:23:31 +0100] rev 40978
reraise interrupt exceptions
Mon, 06 Dec 2010 09:54:58 +0100 [mq]: sledge_binary_minimizer
blanchet [Mon, 06 Dec 2010 09:54:58 +0100] rev 40977
[mq]: sledge_binary_minimizer
Mon, 06 Dec 2010 10:52:48 +0100 correcting usage documentation in mirabelle tool
bulwahn [Mon, 06 Dec 2010 10:52:48 +0100] rev 40976
correcting usage documentation in mirabelle tool
Mon, 06 Dec 2010 10:52:46 +0100 adding mutabelle as a component and an isabelle tool to be used in regression testing
bulwahn [Mon, 06 Dec 2010 10:52:46 +0100] rev 40975
adding mutabelle as a component and an isabelle tool to be used in regression testing
Mon, 06 Dec 2010 10:52:45 +0100 commenting out sledgehammer_mtd in Mutabelle
bulwahn [Mon, 06 Dec 2010 10:52:45 +0100] rev 40974
commenting out sledgehammer_mtd in Mutabelle
Mon, 06 Dec 2010 10:52:45 +0100 removing declaration in quickcheck to really enable exhaustive testing
bulwahn [Mon, 06 Dec 2010 10:52:45 +0100] rev 40973
removing declaration in quickcheck to really enable exhaustive testing
Mon, 06 Dec 2010 10:52:44 +0100 adding timeout to try invocation in mutabelle
bulwahn [Mon, 06 Dec 2010 10:52:44 +0100] rev 40972
adding timeout to try invocation in mutabelle
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip