Thu, 16 Dec 2010 16:18:11 +0100 | blanchet | impose a limit on the breadth of monomorphization (in addition to on the depth) to prevent an explosion of the number of monomorphic instances | changeset | files |
Thu, 16 Dec 2010 15:46:54 +0100 | blanchet | no need to do a super-duper atomization if Metis fails afterwards anyway | changeset | files |
Thu, 16 Dec 2010 15:44:32 +0100 | blanchet | removed unused variable | changeset | files |
Thu, 16 Dec 2010 15:12:17 +0100 | blanchet | robustly handle SMT exceptions in Sledgehammer | changeset | files |
Thu, 16 Dec 2010 15:12:17 +0100 | blanchet | make "debug" imply "blocking", since in blocking mode the exceptions flow through and are more instructive | changeset | files |
Thu, 16 Dec 2010 15:12:17 +0100 | blanchet | reintroduce the higher penalty for skolems | changeset | files |