Z3 diverges on this query

[ranjitjhala]

Hi all,

@michaelborkowski and I found this query where z3 seems to hang.

https://www.dropbox.com/s/j5rw8jqej95j801/z3_hang.smt2?dl=0

I've whittled it down to a minimal query with many declarations and

• 3 asserts
• 1 push
• 1 check-sat

Deleting any of the assert or push makes the query finish instantaneously.

The assert are quite large conjunctions -- I could probably shrink them further if you need.

Any idea what may be going on?

[ranjitjhala]

Thanks @NikolajBjorner!