| Wed, 08 Apr 2015 19:05:57 +0200 |
blanchet |
updated certificates to latest Z3 (and took out one problem that no longer works)
|
file |
diff |
annotate
|
| Mon, 24 Nov 2014 12:35:13 +0100 |
blanchet |
updated SMT certificates
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Thu, 18 Sep 2014 00:03:46 +0200 |
blanchet |
renamed SMT certificate files, following 'SMT2' -> 'SMT' renaming
|
file |
diff |
annotate
|
| Thu, 28 Aug 2014 00:40:38 +0200 |
blanchet |
renamed new SMT module from 'SMT2' to 'SMT'
|
file |
diff |
annotate
|
| Tue, 19 Aug 2014 09:36:37 +0200 |
blanchet |
avoid old 'smt' method in examples
|
file |
diff |
annotate
|
| Sun, 27 Jul 2014 21:11:35 +0200 |
blanchet |
do not embed 'nat' into 'int's in 'smt2' method -- this is highly inefficient and decreases the Sledgehammer success rate significantly
|
file |
diff |
annotate
|
| Thu, 12 Jun 2014 01:00:49 +0200 |
blanchet |
adapted examples to changes in SMT triggers
|
file |
diff |
annotate
|
| Fri, 25 Apr 2014 22:13:17 +0200 |
blanchet |
use Z3 4.3.2 to fix most FIXMEs
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 16:17:14 +0100 |
blanchet |
updated SMT2 certificates
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 14:55:38 +0100 |
blanchet |
updated SMT example certificates
|
file |
diff |
annotate
|
| Thu, 13 Mar 2014 13:18:13 +0100 |
blanchet |
use 'smt2' in SMT examples as much as currently possible
|
file |
diff |
annotate
|
| Fri, 14 Feb 2014 07:53:45 +0100 |
blanchet |
merged 'List.map' and 'List.list.map'
|
file |
diff |
annotate
|
| Wed, 02 Jan 2013 09:31:25 +0100 |
blanchet |
actually run Z3 for "SMT_Tests" when "ISABELLE_FULL_TEST" is enabled
|
file |
diff |
annotate
|
| Mon, 04 Jun 2012 09:07:23 +0200 |
boehmes |
restricted Z3 by default to a fragment where proof reconstruction should not fail (for better integration with Sledgehammer) -- the full set of supported Z3 features can still be used by enabling the configuration option "z3_with_extensions"
|
file |
diff |
annotate
|