diff options
| -rw-r--r-- | src/jib/jib_smt.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml index f9ac05bf..78ab67a3 100644 --- a/src/jib/jib_smt.ml +++ b/src/jib/jib_smt.ml @@ -789,9 +789,12 @@ let builtin_unsigned ctx v ret_ctyp = let builtin_signed ctx v ret_ctyp = match cval_ctyp v, ret_ctyp with - | CT_fbits (n, _), CT_fint m when m > n -> + | CT_fbits (n, _), CT_fint m when m >= n -> SignExtend(m - n, smt_cval ctx v) + | CT_fbits (n, _), CT_lint -> + SignExtend(ctx.lint_size - n, smt_cval ctx v) + | ctyp, _ -> builtin_type_error ctx "signed" [v] (Some ret_ctyp) let builtin_add_bits ctx v1 v2 ret_ctyp = |