haftmann [Mon, 08 Nov 2010 10:56:48 +0100] rev 40422
corrected slip: must keep constant map, not type map; tuned code
haftmann [Mon, 08 Nov 2010 10:43:24 +0100] rev 40421
constructors to datatypes in code_reflect can be globbed; dropped unused code
bulwahn [Mon, 08 Nov 2010 09:25:43 +0100] rev 40420
adding code and theory for smallvalue generators, but do not setup the interpretation yet
blanchet [Mon, 08 Nov 2010 02:33:48 +0100] rev 40419
make sure the SMT solver runs several iterations by lowering the timeout at each iteration -- yields better results in practice
blanchet [Mon, 08 Nov 2010 02:32:27 +0100] rev 40418
better detection of completely irrelevant facts
blanchet [Sun, 07 Nov 2010 18:19:04 +0100] rev 40417
always use a hard timeout in Mirabelle
blanchet [Sun, 07 Nov 2010 18:15:13 +0100] rev 40416
use "smt" (rather than "metis") to reconstruct SMT proofs
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
blanchet [Sun, 07 Nov 2010 18:02:02 +0100] rev 40414
catch TimeOut exception
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