[isabelle-dev] NEWS: Z3 open source

Jasmin Blanchette jasmin.blanchette at inria.fr
Thu Apr 9 21:50:14 CEST 2015

> Can you explain the status of Old_SMT?  Is there anything that isatest still needs to run here?

“old_smt” is there just in case. I was thinking of killing it right after the Isabelle2015 release. It’s not even tested by any regression test. People like Filip Maric, who use Z3 heavily (cf. his emails on the mailing list), might benefit from it, and perhaps others might benefit from it.

We could also ask on the user mailing list and see if anybody cares — although they might not know if they care until it’s too late…


More information about the isabelle-dev mailing list