Tue, 01 Jan 2013 11:36:30 +0100 | blanchet | regenerate certificates -- and use oracle in a few cases where the Z3 proof parser can't deal with Z3 3.2 proofs | file | diff | annotate |
Thu, 23 Aug 2012 15:06:15 +0200 | wenzelm | turned 'boogie_open' into thy_load command, without any declarations of 'uses'; | file | diff | annotate |
Tue, 27 Mar 2012 16:59:13 +0300 | blanchet | renamed "smt_fixed" to "smt_read_only_certificates" | file | diff | annotate |
Mon, 17 Jan 2011 17:45:52 +0100 | boehmes | made Z3 the default SMT solver again | file | diff | annotate |
Thu, 06 Jan 2011 17:51:56 +0100 | boehmes | differentiate between local and remote SMT solvers (e.g., "z3" vs. "remote_z3"); | file | diff | annotate |
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) | file | diff | annotate |
Mon, 15 Nov 2010 00:20:36 +0100 | boehmes | formal dependency on b2i files | file | diff | annotate |