In order to combine PRECONDS + Expr we need to use the SMT solver

This is potential future work.

It turns out we could do better in determining branching statically. Currently, in `SymExec.hs` we have:

```
PleaseAskSMT cond _ continue -> do
case cond of
-- is the condition concrete?
Lit c ->
```

Where `_` is the set of path conditions, and `cond` has been simplified (after https://github.com/ethereum/hevm/pull/329 is merged). However, if e.g. the preconditions say `a=b` and the `cond` is `a==b` then of course we should have this evaluate to `TRUE`. Unfortunately, we don't do that, mostly because our simplifier is not capable of catching some things. For example,

```
ghci> Expr.simplify (Expr.and (Expr.eq (Var "a") (Lit 1)) (Expr.eq (Var "a") (Lit 0)))
And (Eq (Lit 0x1) (Var "a")) (Eq (Lit 0x0) (Var "a"))
```

which is clearly FALSE, since `a` is both 0 and 1. So, we can't just do e.g. a `fold' (Expr.and) (Lit 1) (cond:pathConds)`.

In other words, we need a more sophisticated constant folding system and then we can do better static path condition checking.