Markus Scherer

Indeed, that did the trick! Since that is currently not mentioned in the documentation's chapter on stateful functors: shall I add a sentence or two about compiling them correctly?

Hello @agurfinkel! Since you where wondering how many people are using CHC with non-linear div constraints I wanted to provide another data point: we are using them in our static...

While discussing @wert310's recent pull request (https://github.com/Z3Prover/z3/pull/5821) he and I had the idea that this issue could be solved in a similar manner (basically we could allow `div` and `mod`...

I currently implemented what I wanted to do by listing all the branches that I might want to match. I imagine that this (in the end: asking if a grounded...