| Wed, 15 Dec 2010 18:18:56 +0100 | boehmes | fixed trigger inference: testing if a theorem already has a trigger was too strict; | changeset | files |
| Wed, 15 Dec 2010 16:32:45 +0100 | boehmes | fixed checking and translation of weights (previously, weights occurring in terms were rejected, and weight numbers were unintended translated into Vars) | changeset | files |
| Wed, 15 Dec 2010 16:29:56 +0100 | boehmes | the functions term_of and prop_of are also needed in earlier stages, not only for Z3 proof reconstruction, so they really belong in SMT_Utils | changeset | files |
| Wed, 15 Dec 2010 18:10:32 +0100 | blanchet | facilitate debugging | changeset | files |