diff options
| author | Alasdair | 2020-07-15 13:55:12 +0100 |
|---|---|---|
| committer | Alasdair | 2020-07-15 13:55:12 +0100 |
| commit | 71db59830383b7db5316b5c99ccebe776fc837dc (patch) | |
| tree | 25fe871ae273ff0da3b8a1f0b871c2d20cb41f31 /src/jib | |
| parent | d7a77f7e13dfcf5c8ef607dbabef801141ffacaa (diff) | |
Update duplicate ctor warning
Diffstat (limited to 'src/jib')
| -rw-r--r-- | src/jib/jib_smt.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml index 359704b0..6cbd1b87 100644 --- a/src/jib/jib_smt.ml +++ b/src/jib/jib_smt.ml @@ -1086,7 +1086,7 @@ let builtin_count_leading_zeros ctx v ret_ctyp = bvint ret_sz (Big_int.zero)) else ( assert (sz land (sz - 1) = 0); - let hsz = sz /2 in + let hsz = sz / 2 in Ite (Fn ("=", [Extract (sz - 1, hsz, smt); bvzero hsz]), Fn ("bvadd", [bvint ret_sz (Big_int.of_int hsz); lzcnt hsz (Extract (hsz - 1, 0, smt))]), lzcnt hsz (Extract (sz - 1, hsz, smt))) |