[isabelle-dev] SMT in Isabelle2013 (was: Re: AFP: Session AVL-Trees broken)
makarius at sketis.net
Mon Jan 7 10:26:22 CET 2013
On Thu, 3 Jan 2013, Jasmin Blanchette wrote:
> Hence, Sascha and I will look at the issue, and at any Z3 4.x-specific
> issues, after the release.
> On the other hand, he has a change to the monomorphizer in the pipeline
> since October and might be able to introduce some enhancements in the
> coming days (to make it more complete -- i.e. generate monomorphic
> instances that previously were strangely forgotten). We'll proceed by
> steps there, first upgrading the "smt" method, then Sledgehammer. The
> change should be fairly straightforward; should there be any issues, we
> can postpone it to after the release.
OK, just keep me informed once you know if it will be before or after the
I hope to make a initial "test" snapshot within 1-2 days/weeks, and start
the actual "RC" phase before the end of January. The latter means the
usual fork to a restricted isabelle-release repository with public testing
and only important fixes accepted.
More information about the isabelle-dev