<html><head><meta content="text/html; charset=us-ascii" http-equiv="Content-Type"></head><body><div><div style="font-family: Calibri,sans-serif; font-size: 11pt;">Hi,<br><br>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.<br><br>Cheers,<br>Sascha<br></div></div><hr><span style="font-family: Tahoma,sans-serif; font-size: 10pt; font-weight: bold;">Von: </span><span style="font-family: Tahoma,sans-serif; font-size: 10pt;">Jasmin Christian Blanchette</span><br><span style="font-family: Tahoma,sans-serif; font-size: 10pt; font-weight: bold;">Gesendet: </span><span style="font-family: Tahoma,sans-serif; font-size: 10pt;">04.12.2012 15:07</span><br><span style="font-family: Tahoma,sans-serif; font-size: 10pt; font-weight: bold;">An: </span><span style="font-family: Tahoma,sans-serif; font-size: 10pt;">Makarius</span><br><span style="font-family: Tahoma,sans-serif; font-size: 10pt; font-weight: bold;">Cc: </span><span style="font-family: Tahoma,sans-serif; font-size: 10pt;">isabelle-dev Mailinglist; Sascha Boehme</span><br><span style="font-family: Tahoma,sans-serif; font-size: 10pt; font-weight: bold;">Betreff: </span><span style="font-family: Tahoma,sans-serif; font-size: 10pt;">Re: [isabelle-dev] Status of HOL/SMT</span><br><br>Am 04.12.2012 um 14:52 schrieb Jasmin Christian Blanchette:<br><br>> 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 [*].<br><br>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.<br><br>Sascha, any progress on that front? Last time you wrote<br><br> I do have an idea what might go wrong. I'll need to investigate it further before committing a patch.<br><br>Jasmin<br></body></html>