blanchet [Thu, 09 Dec 2010 08:46:04 +0100] rev 41342
compile
blanchet [Wed, 08 Dec 2010 22:18:37 +0100] rev 41341
lower fudge factor
blanchet [Wed, 08 Dec 2010 22:17:53 +0100] rev 41340
reword error message
blanchet [Wed, 08 Dec 2010 22:17:53 +0100] rev 41339
implicitly call the minimizer for SMT solvers that don't return an unsat core
blanchet [Wed, 08 Dec 2010 22:17:52 +0100] rev 41338
renamings
blanchet [Wed, 08 Dec 2010 22:17:52 +0100] rev 41337
moved function to later module
blanchet [Wed, 08 Dec 2010 22:17:52 +0100] rev 41336
clarified terminology
blanchet [Wed, 08 Dec 2010 22:17:52 +0100] rev 41335
split "Sledgehammer" module into two parts, to resolve forthcoming dependency problems
bulwahn [Wed, 08 Dec 2010 18:07:04 +0100] rev 41334
if only finite types and no real datatypes occur in the quantifiers only enumerate cardinality not size in quickcheck
bulwahn [Wed, 08 Dec 2010 18:07:03 +0100] rev 41333
adding a smarter enumeration scheme for finite functions