| Fri, 01 Aug 2014 14:43:57 +0200 | blanchet | added appropriate method for skolemization of Z3 steps to the mix | changeset | files |
| Fri, 01 Aug 2014 14:43:57 +0200 | blanchet | pushing skolems under 'iff' sometimes breaks things further down the proof (as was to be feared) | changeset | files |
| Fri, 01 Aug 2014 14:43:57 +0200 | blanchet | honor 'try0' also for one-liners | changeset | files |
| Fri, 01 Aug 2014 14:43:57 +0200 | blanchet | tentatively took out 'fastforce' from the set of tried methods -- it seems to be largely subsumed and is hard to silence | changeset | files |
| Fri, 01 Aug 2014 14:43:57 +0200 | blanchet | further minimize one-liner | changeset | files |
| Fri, 01 Aug 2014 14:43:57 +0200 | blanchet | tuning | changeset | files |
| Fri, 01 Aug 2014 14:43:57 +0200 | blanchet | eliminated needlessly complex message tail | changeset | files |