Tue, 21 Dec 2010 06:06:28 +0100 | blanchet | mechanism to keep SMT input and output files around in Mirabelle | changeset | files |
Tue, 21 Dec 2010 04:33:17 +0100 | blanchet | proper handling of the arguments of SMT builtins -- for numerals, ignore the arguments (Pls, Bit0, Bit1, ..), for functions, consider them; | changeset | files |
Tue, 21 Dec 2010 03:56:51 +0100 | blanchet | added "smt_triggers" option to experiment with triggers in Sledgehammer; | changeset | files |