Nikolaj Bjorner

So far the perf difference is centered around equality propagation. Tuning for this benchmark doesn't seem to help other benchmarks that I tried so far. It might even hurt very...

Overall, the solver has to be rewritten, including for these nested sequence scenarios. The most likely culprit inference rule has been dismembered a bit since the bug was filed. The...

still unsound

@mtrberzi - can you comment on whether issues will be addressed and/or close stale issues.

this is great for z3str3. It is a longer standing issue that the seq solver is very poor on negated contains constraints. I will have to reconsider how to handle...

BTW, z3str3 now diverges or takes a long time on this one.

Checking equality of regular languages S, R reduces to checking emptiness of R \ S and S \ R. Checking emptiness/non-emptiness (difference of regular languages) is handled in seq_regex.cpp using...

There is currently a stream of bugs reported to z3str3 but at this point no reaction on when or whether they are going to be addressed. If there is no...

Based on the discussion in the commit logs I take we should try to change the setting change in the header file. I don't have a reference to the reason...

this slipped away somehow. I thought the issue was in the header if-def of z3.h and it should be changed. The main question is then the implications of such a...