Implement arith_bits bvadd : (%bv, %bv2) -> %bv

[Timmmm]

I can't remember why I added this and I'm not 100% sure it's correct, but I did run into this missing case at some point and had the implementation lying around in my repo so here you go. :-)

[github-actions]

Test Results

   12 files  ±0     24 suites  ±0   0s ⏱️ ±0s
  740 tests ±0    740 ✅ ±0  0 💤 ±0  0 ❌ ±0 
2 468 runs  ±0  2 467 ✅ ±0  1 💤 ±0  0 ❌ ±0 

Results for commit 8d4f885. ± Comparison against base commit c2fe0d4.

[Alasdair]

I think it should be

    | CT_lbits, v2_ctyp, CT_lbits ->
        let* smt2 = signed_size ~into:lbits_size ~from:(bv_size v2_ctyp) smt2 in
        return (Fn ("Bits", [Fn ("len", [smt1]); Fn (op, [Fn ("contents", [smt1]); smt2])]))

With an additional helper it could work for any bitvector type for smt1 as well.

[Alasdair]

There might also be some wrapping corner cases in that function, I'll have to think a bit more carefully about it