Translate assert IR node to Z3

We'll need to figure out how to convert assert nodes to z3, right now it just gives an "unhandled node" conversion error so all of the prove_unopt_eq_opt tests have to be disabled when they have `fail!` constructs.

I guess can make their predicates outputs of the boolean circuit and optionally say "these should always be zero" in the assertion set? This is probably one of the places a distinction between assert (I don't expect you to be able to SMT prove this) vs prove (please SMT prove this for me) would be useful. cc @meheff @RobSpringer