Mon, 08 Nov 2010 02:32:27 +0100 better detection of completely irrelevant facts
blanchet [Mon, 08 Nov 2010 02:32:27 +0100] rev 40418
better detection of completely irrelevant facts
Sun, 07 Nov 2010 18:19:04 +0100 always use a hard timeout in Mirabelle
blanchet [Sun, 07 Nov 2010 18:19:04 +0100] rev 40417
always use a hard timeout in Mirabelle
Sun, 07 Nov 2010 18:15:13 +0100 use "smt" (rather than "metis") to reconstruct SMT proofs
blanchet [Sun, 07 Nov 2010 18:15:13 +0100] rev 40416
use "smt" (rather than "metis") to reconstruct SMT proofs
Sun, 07 Nov 2010 18:03:24 +0100 don't pass too many facts on the first iteration of the SMT solver
blanchet [Sun, 07 Nov 2010 18:03:24 +0100] rev 40415
don't pass too many facts on the first iteration of the SMT solver
Sun, 07 Nov 2010 18:02:02 +0100 catch TimeOut exception
blanchet [Sun, 07 Nov 2010 18:02:02 +0100] rev 40414
catch TimeOut exception
Sun, 07 Nov 2010 17:56:07 +0100 ensure the SMT solver respects the timeout -- Mirabelle revealed cases where "smt_filter" apparently never returns
blanchet [Sun, 07 Nov 2010 17:56:07 +0100] rev 40413
ensure the SMT solver respects the timeout -- Mirabelle revealed cases where "smt_filter" apparently never returns
Sun, 07 Nov 2010 17:51:25 +0100 if SMT used as a filter in a loop fails at each iteration, returns the first error, not the last, since it is more informative -- the first error typically says "out of memory", whereas the last might well be "the SMT problem is unprovable", which should be no surprise if too many facts were removed
blanchet [Sun, 07 Nov 2010 17:51:25 +0100] rev 40412
if SMT used as a filter in a loop fails at each iteration, returns the first error, not the last, since it is more informative -- the first error typically says "out of memory", whereas the last might well be "the SMT problem is unprovable", which should be no surprise if too many facts were removed
Sun, 07 Nov 2010 13:29:59 +0100 removed explicit "Interrupt" handling for conformity with async model -- unfortunately the user loses the information about how many scopes were checked, but this needs to be retought with the new interface anyway
blanchet [Sun, 07 Nov 2010 13:29:59 +0100] rev 40411
removed explicit "Interrupt" handling for conformity with async model -- unfortunately the user loses the information about how many scopes were checked, but this needs to be retought with the new interface anyway
Sat, 06 Nov 2010 10:25:08 +0100 make Nitpick datatype tests faster to make timeout less likely
blanchet [Sat, 06 Nov 2010 10:25:08 +0100] rev 40410
make Nitpick datatype tests faster to make timeout less likely
Sat, 06 Nov 2010 10:25:08 +0100 invoke SMT solver in a loop, with fewer and fewer facts, in case of error
blanchet [Sat, 06 Nov 2010 10:25:08 +0100] rev 40409
invoke SMT solver in a loop, with fewer and fewer facts, in case of error
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip