problematic formula

[agriggio]

I just found this while fuzzing my solver. It seems yices goes crazy on this formula. It gets stuck after printing (final check: 4 interface lemmas), eventually running out of memory (I don't remember what was the memory limit though)

(Sorry that I'm putting this inline, but for some reason github doesn't allow me to attach the file -- I tried many different things before giving up).

[Dejan edited] Problem at https://gist.github.com/dddejan/470dc14c770cafe8d7b892b67e9ecc8e

[dddejan]

Thanks for reporting. Which version are you using?

[agriggio]

Sorry, git master

[dddejan]

I tried running it for 20 minutes and didn't get anything (Ubuntu). Are there any particular options or setup you are using?

[agriggio]

Well, that's kind of the point :-) It takes almost no time on other solvers. And if you take a look you will see the memory growing...

[dddejan]

Oh I see, I misunderstood and was waiting for printouts. Will investigate.

[BrunoDutertre]

It's a known issue with linear integer arithmetic. Yices sometimes goes into an infinite branch because its branch algorithm is too crude.

[agriggio]

oh, I see. sorry for the noise then

[BrunoDutertre]

No need to apologize. Thanks for reporting the problem.