| Fri, 21 Dec 2012 11:05:44 +0100 |
boehmes |
updated SMT certificates
|
file |
diff |
annotate
|
| Thu, 01 Nov 2012 11:34:00 +0100 |
blanchet |
regenerated "SMT_Examples" certificates after soft-timeout change + removed a few needless oracles
|
file |
diff |
annotate
|
| Tue, 27 Mar 2012 17:11:02 +0200 |
boehmes |
dropped support for List.distinct in binding to SMT solvers: only few applications benefited from this support, and in some cases the smt method fails due to its support for List.distinct
|
file |
diff |
annotate
|
| Mon, 26 Mar 2012 11:01:04 +0200 |
blanchet |
reintroduced broken proofs and regenerated certificates
|
file |
diff |
annotate
|
| Sun, 25 Dec 2011 08:42:33 +0100 |
haftmann |
updated certificate
|
file |
diff |
annotate
|
| Wed, 14 Sep 2011 09:46:59 +0200 |
boehmes |
observe distinction between sets and predicates
|
file |
diff |
annotate
|
| Tue, 06 Sep 2011 18:07:44 +0200 |
boehmes |
added some examples for pattern and weight annotations
|
file |
diff |
annotate
|
| Sun, 26 Jun 2011 19:10:03 +0200 |
boehmes |
updated SMT certificates
|
file |
diff |
annotate
|
| Wed, 08 Jun 2011 13:43:15 +0200 |
boehmes |
updated SMT certificates
|
file |
diff |
annotate
|
| Sun, 05 Jun 2011 15:00:52 +0200 |
boehmes |
updated SMT certificates
|
file |
diff |
annotate
|
| Tue, 31 May 2011 19:28:03 +0200 |
boehmes |
updated SMT certificates
|
file |
diff |
annotate
|
| Wed, 09 Mar 2011 21:40:38 +0100 |
boehmes |
finished and tested Z3 proof reconstruction for injective functions;
|
file |
diff |
annotate
|
| Mon, 03 Jan 2011 16:49:28 +0100 |
boehmes |
updated SMT certificates
|
file |
diff |
annotate
|
| Mon, 20 Dec 2010 09:31:47 +0100 |
boehmes |
updated SMT certificates
|
file |
diff |
annotate
|
| Sun, 19 Dec 2010 18:55:21 +0100 |
boehmes |
updated SMT certificates
|
file |
diff |
annotate
|
| Fri, 17 Dec 2010 14:59:06 +0100 |
boehmes |
updated SMT certificates
|
file |
diff |
annotate
|
| Wed, 15 Dec 2010 10:52:43 +0100 |
boehmes |
updated SMT certificates
|
file |
diff |
annotate
|
| Tue, 07 Dec 2010 15:44:38 +0100 |
boehmes |
updated SMT certificates
|
file |
diff |
annotate
|
| Wed, 24 Nov 2010 10:39:58 +0100 |
boehmes |
be more precise: only treat constant 'distinct' applied to an explicit list as built-in
|
file |
diff |
annotate
|
| Wed, 03 Nov 2010 17:02:53 +0100 |
boehmes |
updated SMT certificates
|
file |
diff |
annotate
|
| Fri, 29 Oct 2010 18:17:11 +0200 |
boehmes |
updated SMT certificates
|
file |
diff |
annotate
|
| Tue, 26 Oct 2010 11:46:19 +0200 |
boehmes |
changed SMT configuration options; updated SMT certificates
|
file |
diff |
annotate
|
| Tue, 13 Jul 2010 02:29:05 +0200 |
boehmes |
fixed handling of Ball/Bex: turn equalities into meta-equalities for the rewriting conversions;
|
file |
diff |
annotate
|
| Thu, 27 May 2010 18:16:54 +0200 |
boehmes |
added function update examples and set examples
|
file |
diff |
annotate
|
| Thu, 27 May 2010 17:09:37 +0200 |
boehmes |
updated SMT certificates
|
file |
diff |
annotate
|
| Thu, 27 May 2010 14:55:53 +0200 |
boehmes |
use Z3's builtin support for div and mod
|
file |
diff |
annotate
|
| Wed, 26 May 2010 15:35:17 +0200 |
boehmes |
updated SMT certificates
|
file |
diff |
annotate
|
| Wed, 12 May 2010 23:54:06 +0200 |
boehmes |
updated SMT certificates
|
file |
diff |
annotate
|