16 points | by Bluestein 2 days ago ago
6 comments
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.
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.
Or a BMW, or a groundbreaking electro mechanical computer, depending :)
I was hoping for the mechanical computer...
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.
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.
Or a BMW, or a groundbreaking electro mechanical computer, depending :)
I was hoping for the mechanical computer...