29 points Bluestein 1 day ago 8 comments

greatgib 2 hours ago | parent

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.

Bluestein 2 hours ago | parent

Or a BMW, or a groundbreaking electro mechanical computer, depending :)

number6 2 hours ago | parent

I was hoping for the mechanical computer...

112233 2 hours ago | parent

oh, something new! I thought Z3 is SAT/SMT solver, they must have added something.

Jaxan 2 hours ago | parent

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.

IshKebab 1 hour ago | parent

It is. Look up what SMT stands for.

mcphage 12 minutes ago | parent

Shin Megami Tensei?

NooneAtAll3 4 minutes ago | parent

SMT is SAT+arithmetic, no?