| Mon, 08 Nov 2010 09:25:43 +0100 | bulwahn | adding code and theory for smallvalue generators, but do not setup the interpretation yet | changeset | files |
| Mon, 08 Nov 2010 02:33:48 +0100 | blanchet | make sure the SMT solver runs several iterations by lowering the timeout at each iteration -- yields better results in practice | changeset | files |
| Mon, 08 Nov 2010 02:32:27 +0100 | blanchet | better detection of completely irrelevant facts | changeset | files |
| Sun, 07 Nov 2010 18:19:04 +0100 | blanchet | always use a hard timeout in Mirabelle | changeset | files |
| Sun, 07 Nov 2010 18:15:13 +0100 | blanchet | use "smt" (rather than "metis") to reconstruct SMT proofs | changeset | files |
| Sun, 07 Nov 2010 18:03:24 +0100 | blanchet | don't pass too many facts on the first iteration of the SMT solver | changeset | files |