1 files changed, 20 insertions, 10 deletions
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index da0048d7..6308a73f 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -536,6 +536,11 @@ let builtin_min_int ctx v1 v2 ret_ctyp =
           smt1,
           smt2)
 
+let bvmask ctx len =
+  let all_ones = bvones (lbits_size ctx) in
+  let shift = Fn ("concat", [bvzero (lbits_size ctx - ctx.lbits_index); len]) in
+  bvnot (bvshl all_ones shift)
+
 let builtin_eq_bits ctx v1 v2 =
   match cval_ctyp v1, cval_ctyp v2 with
   | CT_fbits (n, _), CT_fbits (m, _) ->
@@ -545,15 +550,20 @@ let builtin_eq_bits ctx v1 v2 =
      Fn ("=", [smt1; smt2])
 
   | CT_lbits _, CT_lbits _ ->
-     Fn ("=", [smt_cval ctx v1; smt_cval ctx v2])
+     let len1 = Fn ("len", [smt_cval ctx v1]) in
+     let contents1 = Fn ("contents", [smt_cval ctx v1]) in
+     let len2 = Fn ("len", [smt_cval ctx v1]) in
+     let contents2 = Fn ("contents", [smt_cval ctx v1]) in
+     Fn ("and", [Fn ("=", [len1; len2]);
+                 Fn ("=", [Fn ("bvand", [bvmask ctx len1; contents1]); Fn ("bvand", [bvmask ctx len2; contents2])])])
 
   | CT_lbits _, CT_fbits (n, _) ->
-     let smt2 = unsigned_size ctx (lbits_size ctx) n (smt_cval ctx v2) in
-     Fn ("=", [Fn ("contents", [smt_cval ctx v1]); smt2])
+     let smt1 = unsigned_size ctx n (lbits_size ctx) (Fn ("contents", [smt_cval ctx v1])) in
+     Fn ("=", [smt1; smt_cval ctx v2])
 
   | CT_fbits (n, _), CT_lbits _ ->
-     let smt1 = unsigned_size ctx (lbits_size ctx) n (smt_cval ctx v1) in
-     Fn ("=", [smt1; Fn ("contents", [smt_cval ctx v2])])
+     let smt2 = unsigned_size ctx n (lbits_size ctx) (Fn ("contents", [smt_cval ctx v2])) in
+     Fn ("=", [smt_cval ctx v1; smt2])
 
   | _ -> builtin_type_error ctx "eq_bits" [v1; v2] None
 
@@ -566,11 +576,6 @@ let builtin_zeros ctx v ret_ctyp =
      Fn ("Bits", [extract (ctx.lbits_index - 1) 0 (smt_cval ctx v); bvzero (lbits_size ctx)])
   | _ -> builtin_type_error ctx "zeros" [v] (Some ret_ctyp)
 
-let bvmask ctx len =
-  let all_ones = bvones (lbits_size ctx) in
-  let shift = Fn ("concat", [bvzero (lbits_size ctx - ctx.lbits_index); len]) in
-  bvnot (bvshl all_ones shift)
-
 let builtin_ones ctx cval = function
   | CT_fbits (n, _) -> bvones n
   | CT_lbits _ ->
@@ -747,6 +752,9 @@ let builtin_vector_subrange ctx vec i j ret_ctyp =
   | CT_fbits (n, _), CT_constant i, CT_constant j ->
      Extract (Big_int.to_int i, Big_int.to_int j, smt_cval ctx vec)
 
+  | CT_lbits _, CT_constant i, CT_constant j ->
+     Extract (Big_int.to_int i, Big_int.to_int j, Fn ("contents", [smt_cval ctx vec]))
+
   | _ -> builtin_type_error ctx "vector_subrange" [vec; i; j] (Some ret_ctyp)
 
 let builtin_vector_access ctx vec i ret_ctyp =
@@ -1162,6 +1170,8 @@ let rec smt_conversion ctx from_ctyp to_ctyp x =
      bvint ctx.lint_size c
   | CT_fint sz, CT_lint ->
      force_size ctx ctx.lint_size sz x
+  | CT_lbits _, CT_fbits (n, _) ->
+     unsigned_size ctx n (lbits_size ctx) (Fn ("contents", [x]))
   | _, _ -> failwith (Printf.sprintf "Cannot perform conversion from %s to %s" (string_of_ctyp from_ctyp) (string_of_ctyp to_ctyp))
 
 let define_const ctx id ctyp exp = Define_const (zencode_name id, smt_ctyp ctx ctyp, exp)