SMT: Fix missing case for append builtin

1 files changed, 6 insertions, 0 deletions

diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index 6ace9d96..f9ac05bf 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -697,6 +697,12 @@ let builtin_append ctx v1 v2 ret_ctyp =
      Fn ("Bits", [bvadd (bvint ctx.lbits_index (Big_int.of_int n)) (Fn ("len", [smt1]));
                   Extract (lbits_size ctx - 1, 0, Fn ("concat", [Fn ("contents", [smt1]); smt2]))])
 
+  | CT_fbits (n, _), CT_fbits (m, _), CT_lbits _ ->
+     let smt1 = smt_cval ctx v1 in
+     let smt2 = smt_cval ctx v2 in
+     Fn ("Bits", [bvint ctx.lbits_index (Big_int.of_int (n + m));
+                  unsigned_size ctx (lbits_size ctx) (n + m) (Fn ("concat", [smt1; smt2]))])
+
   | CT_lbits _, CT_lbits _, CT_lbits _ ->
      let smt1 = smt_cval ctx v1 in
      let smt2 = smt_cval ctx v2 in