From 22123333fc80bf5d3ee73c6692f3fba44892bcee Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Wed, 12 Jun 2019 17:34:07 +0100
Subject: SMT: Fix missing case for append builtin

---
 src/jib/jib_smt.ml | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'src')

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
-- 
cgit v1.2.3