| 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 |
| Sun, 07 Nov 2010 18:02:02 +0100 | blanchet | catch TimeOut exception | changeset | files |
| Sun, 07 Nov 2010 17:56:07 +0100 | blanchet | ensure the SMT solver respects the timeout -- Mirabelle revealed cases where "smt_filter" apparently never returns | changeset | files |
| Sun, 07 Nov 2010 17:51:25 +0100 | blanchet | 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 | changeset | files |