| Tue, 26 Oct 2010 17:35:52 +0200 | boehmes | trace assumptions before giving them to the SMT solver | changeset | files |
| 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 |
| Tue, 26 Oct 2010 15:06:36 +0200 | krauss | fixed typo | changeset | files |
| Tue, 26 Oct 2010 15:01:39 +0200 | blanchet | merged | changeset | files |
| Tue, 26 Oct 2010 15:01:02 +0200 | blanchet | merged | changeset | files |