Marco Eilers
Marco Eilers
Turns out there is an old issue that seems to describe the exact same problem (that I just didn't know about): #327 I'm working on a fix.
Sorry, I started working on this and then somehow forgot about it. It's finally fixed now in https://github.com/viperproject/silicon/pull/935.
Hey, thanks for trying that out! I really wasn't aware that that assumption leads to any performance issues, this is interesting. I'm not entirely sure I understand the push-pop approach....
Great, I just looked into the SMT stuff emitted by Silicon for the smaller example and tried to figure out what's happening, and it turns out I should have just...