[isabelle-dev] smt2

[Lawrence Paulson]

But working very well, in my experience.

Now, will smt2 calls be suitable for the Library and AFP?

Larry

On 6 Mar 2014, at 15:43, Jasmin Christian Blanchette <jasmin.blanchette at gmail.com> wrote:

> As you may know, Sascha and I have been working on a new version of the "smt" proof method, called "smt2". It is effectively a clone of "smt", but with the Z3 interaction (problem generation, proof parsing, and reconstruction) rewritten from scratch, with the following short-term goals:
> 
> 1. Use SMT-LIB 2 instead of 1.
> 2. Support newer versions of Z3 (> 4.0).
> 3. Produce Isar proofs from Z3 proofs.
> 
> It is still highly experimental