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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
