Hi,
I spent a couple of hours on this issue. Some odd things are going on during
normalization of goals in the smt method. I have the feeling that normalization
somehow (accidentally?) worked before Tobias' change on rewr_conv, but that it
should really be implemented in a different, more stable way. I'll need a bit
more time. Everything should be fixed by the end of the year.
Cheers,
Sascha
----- Ursprüngliche Nachricht -----
Von: Jasmin Christian Blanchette
Gesendet: 04.12.2012 15:07
An: Makarius
Cc: isabelle-dev Mailinglist; Sascha Boehme
Betreff: Re: [isabelle-dev] Status of HOL/SMT
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
