| Tue, 26 Oct 2010 11:39:26 +0200 | boehmes | keep track of theorems initially given to SMT (even if they are rewritten); provide interface to filter theorems necessary for SMT proofs | file | diff | annotate |
| Sun, 19 Sep 2010 11:33:39 +0200 | boehmes | properly parse Z3 error models, including datatypes, and represent function valuations as lambda terms; also normalize Z3 error models | file | diff | annotate |
| 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 | file | diff | annotate |
| Wed, 12 May 2010 23:54:04 +0200 | boehmes | layered SMT setup, adapted SMT clients, added further tests, made Z3 proof abstraction configurable | file | diff | annotate |