| Fri, 17 Dec 2010 15:30:43 +0100 | blanchet | run the SMT relevance filter only once, then run the normalization/monomorphization code once _per class_ of SMT solvers | changeset | files |
| Fri, 17 Dec 2010 12:10:08 +0100 | blanchet | make timeout part of the SMT filter's tail | changeset | files |
| Fri, 17 Dec 2010 12:02:57 +0100 | blanchet | merge | changeset | files |
| Fri, 17 Dec 2010 12:02:46 +0100 | blanchet | split "smt_filter" into head and tail | changeset | files |
| Fri, 17 Dec 2010 12:01:49 +0100 | blanchet | fewer facts to SInE-E | changeset | files |
| Fri, 17 Dec 2010 11:12:37 +0100 | blanchet | Z3 sometimes reports two errors, with the first one referring to line 1 for some strange reason -- but it makes no sense to kill line 1, so we traverse the errors in reverse and consider only the last error | changeset | files |