Am 04.12.2012 um 14:52 schrieb Jasmin Christian Blanchette:
> The real issue, at the end of the day, seems to be not so much Z3 4.0 in
> itself but rather the fact that our code often can't parse them. I've looked
> into this and saw no quick fix [*].
Oh, Tobias just reminded me that a second issue is the "rewr_conv" change. See
Ondra's and Sascha's emails on November 9. If there's no quick resolution on
that front, I would suggest simply introducing "rewr_conv_old" in the SMT
source code and using that.
Sascha, any progress on that front? Last time you wrote
I do have an idea what might go wrong. I'll need to investigate it further
before committing a patch.
Jasmin
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
