# NOTE: a little bit Z3 solver

Satisfiability Modulo Theories(SMT) problem is a decision problem for logical formulas with respect to combinations of background theories such as arithmetic, bit-vectors, arrays, and uninterpreted functions. Z3 is an efficient SMT solver with specialized algorithms for solving background theories.

Wow, many words. But for me, right now, Z3 is a theorem prover from Microsoft. Use SMT-LIB this lisp-like language.

```
(declare-const x Int)
(declare-const y Int)
(assert (= 5 (+ x y 3)))
(check-sat)
```

The program produce: `sat`

as result. If we didn't provide a possible
constraint:

(declare-const x Int) (assert (= 5 (+ x 3))) (assert (= 5 (+ x 2))) (check-sat)

The result would be `unsat`

, not surprising.

As title, **a little bit** z3, this is the end, I hadn't know where can I
use z3, XD.