Papers/information on "sat.euf"

[zimmski]

"sat.euf" pops up from time to time in issues/PRs and the changelog. Is there any information for the eager follower of Z3 to get to know why "sat.euf" is important? What it is actually good for? Maybe some papers?

Also, how can we help to bring it out of the unstable phase?

TLDR: Why should a Z3 user care about "sat.euf"?

[NikolajBjorner]

sat.euf enables a new SMT core. It uses a more efficient (at least in main cases) SAT solver as the core. It contains all theories except strings, transitivity. But quantifiers has some way to go before being debugged. Getting performance on par with the legacy core is a very significant effort so ETA is sometime late next year. It can be used for some tasks at this point, but it is a bit premature of me to advertise it.

[zimmski]

@NikolajBjorner thank you for your answer. Are there any papers one can read to understand why the new SMT core and SAT solver are needed and why they are more efficient? In general if there are any papers/articles on where the Z3 changes are going, that would be extremely helpful as a power user, and as a person who is also into SAT/SMT.