Mon, 06 Dec 2010 13:18:25 +0100 blanchet started generalizing monotonicity code to accommodate new calculus
Mon, 06 Dec 2010 13:17:26 +0100 blanchet merged
Mon, 06 Dec 2010 11:41:24 +0100 blanchet handle "max_relevant" uniformly
Mon, 06 Dec 2010 11:26:17 +0100 blanchet honor the default max relevant facts setting from the SMT solvers in Sledgehammer
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?
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
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
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -7 +7 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip