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?
Satisfiability Modulo Theories
well a SAT solver is kinda sorta a theorem prover right...?
Or a BMW, or a groundbreaking electro mechanical computer, depending :)