| Fri, 08 Apr 2011 19:04:08 +0200 | boehmes | check if negating the goal is possible (avoids CTERM exception for Pure propositions) | changeset | files |
| Fri, 08 Apr 2011 19:04:08 +0200 | boehmes | unfold and eta-contract let expressions before lambda-lifting to avoid bad terms | changeset | files |
| Fri, 08 Apr 2011 19:04:08 +0200 | boehmes | corrected order of steps in Z3 proof reconstruction for elimination of unused quantified variables: first try to eliminate unused variables, then skip over used variables | changeset | files |