| Fri, 10 Sep 2010 17:53:25 +0200 | bulwahn | directly computing the values of interest instead of composing functions in an unintelligent way that causes exponential much garbage; using the latest theory | changeset | files |
| Mon, 13 Sep 2010 06:02:47 +0200 | boehmes | added preliminary support for SMT datatypes (for now restricted to tuples and lists); only the Z3 interface (in oracle mode) makes use of it, there is especially no Z3 proof reconstruction support for datatypes yet | changeset | files |
| Fri, 10 Sep 2010 23:56:35 +0200 | krauss | use eta-contracted version for occurrence check (avoids possible non-termination) | changeset | files |