Slightly more complicated than the toy examples shown in the documentation above, and hints at one of the real world use cases for Z3 - red teaming cryptography.
That said, I'm not sure the documentation linked above is really doing it any favors in terms of helping popularizing it.
Sometimes you can use SMT for “theorem proving”. It is a rather broad term. I don’t think they added something much different than what they already had.
I like Z3 a lot. I think it's criminally underappreciated and underused. Here is a fairly interesting use I put it to a few years ago:
https://www.oranlooney.com/post/playfair/#known-plaintext-at...
Slightly more complicated than the toy examples shown in the documentation above, and hints at one of the real world use cases for Z3 - red teaming cryptography.
That said, I'm not sure the documentation linked above is really doing it any favors in terms of helping popularizing it.
If anyone wondering, because it took me a few hops to find out:
Z3 is a high-performance theorem prover being developed at Microsoft Research.
Or a BMW, or a groundbreaking electro mechanical computer, depending :)
I was hoping for the mechanical computer...
oh, something new! I thought Z3 is SAT/SMT solver, they must have added something.
Sometimes you can use SMT for “theorem proving”. It is a rather broad term. I don’t think they added something much different than what they already had.
It is. Look up what SMT stands for.
Shin Megami Tensei?
SMT is SAT+arithmetic, no?