Turn failure conditions into provable assertions (i.e. that failure never occurs) in Z3 translation

As suggested in #1344 -- I think this isn't a big lift: we'll need to keep some record of what predicates were for assert ops and wire those up to the top level predicate being proven for the function.