---
# System prepended metadata

title: z3

---

These notes are available at [tjcsec.club/pres](https://tjcsec.club/pres)!
# Math is hard
Math that is completed by hand is often prone to errors, and sometimes problems will be far too difficult to solve on paper. This is where [z3](https://github.com/Z3Prover/z3) comes in! z3 is a program developed by Microsoft which allows you to solve equations with integer answers. While the backend is written in C++, there are several bindings available, and the most convenient of these is the Python one, which I will cover here.
## Installation
z3 can be installed via `pip install z3-solver`.

**IMPORTANT NOTE:** The package found by using `pip install z3` is **NOT** the same thing, and will not help you solve equations. Be careful to install the right one!

## Usage
The library is available to be imported using `import z3`. Variables can be declared using the syntax `some_var = z3.Int("name")`, with `Int` replaced with `Real`, `Bool`, etc. if necessary. Then, simple expressions can be solved by passing multiple constraints to `z3.solve`:
```python
from z3 import *
x = Int("x")
y = Int("y")
solve(x > 2, y < 10, x + 2*y == 7)
```
However, this can quickly become unwieldy when we have too many constraints. For larger problems, a `z3.Solver` object is usually better:
```python
from z3 import *

x, y, z = Ints('x y z') # shorthand for Int('x'), Int('y')...

s = Solver()

s.add(x+y==9)
s.add(x-2==z)

print(s.check())  # "sat" if there is a solution, "unsat" if none
print(s.model())  # prints the actual answer

```
z3 can also do basic simplification of expressions through  `z3.simplify`:
```python
from z3 import *
a = Bool("a")
print(simplify(And(a, True)))
```
Some rev challenges will involve unsigned integer types with a fixed number of bits. These types wrap around after overflowing, so a normal `z3.Int` won't work. In this case, a `z3.BitVec` is better. This type will operate exactly the same as a C `int`, `long`, etc. if you choose the same number of bits. One key distinction is that a `z3.BitVec` uses signed operations by default, so if the challenge uses an unsigned number, you need to use the unsigned version. `a > b` turns into `UGT(a, b)`, where `UGT` stands for *U*nsigned *G*reater *T*han, and the same thing applies for `<`, `<=`, `>=`, `/`, `%` and `>>`.  See [here](https://microsoft.github.io/z3guide/programming/Z3%20Python%20-%20Readonly/Introduction/#machine-arithmetic) for more information. 
### Limitations
z3 only works on polynomial expressions, so if you ask it to solve something like `2**x==4`, it will throw an error. Also, on numbers larger than 32 bits, it may take too long to solve non-trivial expressions to be useful.
### More information
- [official z3 python docs](https://microsoft.github.io/z3guide/programming/Z3%20Python%20-%20Readonly/Introduction/)
- [github page](https://github.com/Z3Prover/z3)

Go work on today's challenges at [ctf.tjcsec.club](https://ctf.tjcsec.club)!