diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/jib/jib_smt.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml index 78ab67a3..4b868050 100644 --- a/src/jib/jib_smt.ml +++ b/src/jib/jib_smt.ml @@ -691,6 +691,11 @@ let builtin_append ctx v1 v2 ret_ctyp = Fn ("Bits", [bvadd (bvint ctx.lbits_index (Big_int.of_int n)) (Fn ("len", [smt2])); bvor (bvshl x shift) (Fn ("contents", [smt2]))]) + | CT_lbits _, CT_fbits (n, _), CT_fbits (m, _) -> + let smt1 = smt_cval ctx v1 in + let smt2 = smt_cval ctx v2 in + Extract (m - 1, 0, Fn ("concat", [Fn ("contents", [smt1]); smt2])) + | CT_lbits _, CT_fbits (n, _), CT_lbits _ -> let smt1 = smt_cval ctx v1 in let smt2 = smt_cval ctx v2 in |