[isabelle-dev] SMT in Isabelle2013 (was: Re: AFP: Session AVL-Trees broken)

[Makarius]

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 
release.

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.


 	Makarius