| Tue, 26 Oct 2010 17:35:51 +0200 | boehmes | capture out-of-memory warnings of Z3 and turn them into proper exceptions; be more precise about SMT solver run-time: return NONE instead of ~1 | changeset | files |
| Tue, 26 Oct 2010 17:35:49 +0200 | boehmes | honor choice of either local or remote SMT solver only for smt_filter and keep default behaviour for the SMT tactic; omit messages when running smt_filter | changeset | files |
| Tue, 26 Oct 2010 16:39:21 +0200 | haftmann | include ATP in theory List -- avoid theory edge by-passing the prominent list theory | changeset | files |