# Simple SMT solver for use in an optimizing compiler

Posted on December 31, 2014This is a second blog post in a series about engineering optimizing compilers; the previous was Quasi-quoting DSLs for free. In this blog we will see how we might write a very simple SMT solver that will allow us to write an optimization pass that can turn something like

```
if a == 0 then
if !(a == 0) && b == 1 then
write 1
else
write 2
else
write 3
```

into

```
if a == 0 then
write 2
else
write 3
```

without much effort at all. Read more at well-typed.com