| Mon, 26 Sep 2016 07:56:54 +0200 |
haftmann |
syntactic type class for operation mod named after mod;
|
file |
diff |
annotate
|
| Fri, 04 Dec 2015 14:15:17 +0100 |
blanchet |
updated SMT certificates
|
file |
diff |
annotate
|
| Mon, 01 Jun 2015 18:59:21 +0200 |
haftmann |
separate class for division operator, with particular syntax added in more specific classes
|
file |
diff |
annotate
|
| 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
|
| Wed, 24 Sep 2014 15:46:41 +0200 |
blanchet |
updated SMT certificates
|
file |
diff |
annotate
|
| Thu, 18 Sep 2014 00:03:46 +0200 |
blanchet |
renamed SMT certificate files, following 'SMT2' -> 'SMT' renaming
|
file |
diff |
annotate
| base
|
| 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 13:18:13 +0100 |
blanchet |
use 'smt2' in SMT examples as much as currently possible
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:37:28 +0100 |
blanchet |
updated certificates
|
file |
diff |
annotate
|
| Tue, 24 Sep 2013 16:21:04 +0200 |
blanchet |
updated certificates
|
file |
diff |
annotate
|
| Thu, 28 Mar 2013 23:44:43 +0100 |
boehmes |
re-generated SMT certificates
|
file |
diff |
annotate
|
| 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, 01 Nov 2012 11:34:00 +0100 |
blanchet |
regenerated "SMT_Examples" certificates after soft-timeout change + removed a few needless oracles
|
file |
diff |
annotate
|
| Mon, 26 Mar 2012 11:01:04 +0200 |
blanchet |
reintroduced broken proofs and regenerated certificates
|
file |
diff |
annotate
|
| Tue, 03 Jan 2012 18:33:17 +0100 |
blanchet |
regenerate SMT example certificates, to reflect "set" type constructor
|
file |
diff |
annotate
|
| Mon, 07 Nov 2011 17:54:38 +0100 |
boehmes |
try different alternatives in discharging extra assumptions when schematic theorems obtained from lambda-lifting can be instantiated in different ways
|
file |
diff |
annotate
|
| Mon, 18 Jul 2011 18:52:52 +0200 |
boehmes |
allow rules with premises to be declared as z3_rule (to circumvent incompleteness of Z3 proof reconstruction)
|
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
|
| Fri, 08 Apr 2011 19:04:08 +0200 |
boehmes |
added SMT certificates
|
file |
diff |
annotate
|
| Fri, 08 Apr 2011 19:04:08 +0200 |
boehmes |
corrected order of steps in Z3 proof reconstruction for elimination of unused quantified variables: first try to eliminate unused variables, then skip over used variables
|
file |
diff |
annotate
|
| Mon, 21 Feb 2011 09:19:44 +0100 |
boehmes |
added test cases with quantifier occurring in first-order term positions
|
file |
diff |
annotate
|
| Mon, 14 Feb 2011 12:25:26 +0100 |
boehmes |
limit the number of generated SMT monomorphization instances (in addition to the existing monomorphization limit which does not prevent seemingly infinite loops);
|
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
|
| Fri, 17 Dec 2010 08:37:35 +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
|
| Tue, 26 Oct 2010 11:46:19 +0200 |
boehmes |
changed SMT configuration options; updated SMT certificates
|
file |
diff |
annotate
|
| Thu, 27 May 2010 17:09:37 +0200 |
boehmes |
updated SMT certificates
|
file |
diff |
annotate
|
| Thu, 27 May 2010 16:29:33 +0200 |
boehmes |
renamed constant "apply" to "fun_app" (which is closer to the related "fun_upd")
|
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
|