## Stream: Program verification

### Topic: SMT (Z3) bindings

#### Alcides Fonseca (Jun 03 2020 at 13:12):

I understand at some point there was a smt tactic in lean. Is there any documentation on how to use an smt solver (z3 would be ideal for me) from Lean?

#### Johan Commelin (Jun 03 2020 at 13:27):

There is still a bunch of smt stuff in core

#### Johan Commelin (Jun 03 2020 at 13:27):

I've never used it

#### Bryan Gin-ge Chen (Jun 03 2020 at 13:30):

I remember Mario recently saying that nobody has ever used it.

If you figure it out, please let us know!

#### Alcides Fonseca (Jun 03 2020 at 13:47):

There is just a tactic that provides debugging for seeing the SMT state. But as far as I know, SMT is only used inside the c++ core.

-- This tactic is just a placeholder, designed to be modified for specific performance experiments

#### Simon Hudon (Jun 03 2020 at 14:35):

I think @Jesse Michael Han uses it frequently

#### Gabriel Ebner (Jun 03 2020 at 14:42):

There are two different questions here:

1. About the internal SMT state (i.e. begin[smt] ... end, by cc): calling this SMT is a bit of a stretch. There is no SAT solver, and it only knows about congruence closure (with AC) and heuristic instantiation. At least by cc is used somewhat often in mathlib.
2. Interfacing with external SMT solvers. Jared had an unverified interface to Z3 at one point: https://github.com/leanprover/smt2_interface This allows you to call Z3 on Lean goals (including some arithmetic), but it doesn't do proofs.

#### Gabriel Ebner (Jun 03 2020 at 14:42):

The Z3 interface is completely unused, AFAIK.

#### Alcides Fonseca (Jun 03 2020 at 15:16):

Thanks! I was looking for that second one!

#### Bryan Gin-ge Chen (Jun 03 2020 at 15:19):

#1083 is related, but uses Vampire, not Z3.

#### Jesse Michael Han (Jun 03 2020 at 18:45):

any invocation of finish dips into the internal SMT state (via heuristic instantiation + congruence closure)

#### Joe Hendrix (Jun 18 2020 at 21:37):

I used the lean3 SMT tactic for congruence-closure type-problems -- it worked fine, but as noted it's not really the same as an SMT solver.

Last updated: May 08 2021 at 22:13 UTC