Wed, 17 Nov 2010 09:22:23 +0100 | boehmes | require the b2i file ending in the boogie_open command (for consistency with the theory header) | changeset | files |
Wed, 17 Nov 2010 08:14:56 +0100 | boehmes | use the const antiquotation for constants (this checks that the constant is declared, whereas the more general term antiquotation treats undeclared names as free variable) | changeset | files |
Wed, 17 Nov 2010 08:14:55 +0100 | boehmes | keep input and output files used to communicate with the SMT solver (for debugging purposes mainly) | changeset | files |