Re: [isabelle] AFP submission and smt2

On Tue, 4 Nov 2014, marco caminati wrote:

In AFP submission guidelines (, I read "No use of the command smt."

But what about smt2? Does the same exclusion hold?

(I should say I have no idea about the difference between them)

This is explained in NEWS:

* SMT module: A new version of the SMT module, temporarily called "SMT2",
  uses SMT-LIB 2 and supports recent versions of Z3 (e.g., 4.3). The new
  proof method is called "smt2". CVC3 and CVC4 are also supported as
  oracles. Yices is no longer supported, because no version of the solver
  can handle both SMT-LIB 2 and quantifiers.

In the next release, there will be only the new version of the SMT module and Z3, and the proof method will be just called "smt" again.

Back to the AFP question. The official text from says:

  No use of the command smt. The result of this command depends on
  external tools that are not under our control and may stop working in
  the future.

I am not an AFP editor, but my interpretation of it: since Z3 is non-free, having AFP entries depend on it would render them unusable for people who don't have a valid Z3 license. Z3 is only free as in beer for non-commercial users. It is a friendly move of MSR that we can easily bundle it according to its non-free license, but it is not a proper open-source component.


          797,770 people so far

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.