[isabelle-dev] AFP: Session AVL-Trees broken

[Jasmin Christian Blanchette]

Hi Sascha,

> Before Tobias' change, one sub-conversion (a rewr_conv) in that process returns a beta-reduced equation (reducing one of the above lambda abstractions), and hence the left-hand side does not match anymore the term given to the conversion.

Right now I am experiencing lots of failures -- typically Z3 3.2 returning with error code 112. I don't know if it's an instance of the same bug, but as long as this is broken it's hard to know.

Would it be possible to change the offending "rewr_conv" call(s) with a local copy of the old "rewr_conv" code as a temporary, immediate solution? I would sleep better if we had something that is not-more-broken-than-it-used-to-be in the repository, especially in the face of a release in January or February. I would be ready to do the change myself but they you would need to tell me exactly which "rewr_conv" call(s) are concerned, and ideally explain how to reproduce the issue on smaller examples.

Thanks,

Jasmin