diff options
| -rw-r--r-- | src/jib/jib_smt.ml | 2 | ||||
| -rw-r--r-- | test/typecheck/fail/duplicate_ctor.expect | 2 |
2 files changed, 2 insertions, 2 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))) diff --git a/test/typecheck/fail/duplicate_ctor.expect b/test/typecheck/fail/duplicate_ctor.expect index 28253714..ac07c644 100644 --- a/test/typecheck/fail/duplicate_ctor.expect +++ b/test/typecheck/fail/duplicate_ctor.expect @@ -2,5 +2,5 @@ Type error: [[96mduplicate_ctor.sail[0m]:3:15-19 3[96m |[0munion foo2 = { Bar1 : int } [91m |[0m [91m^--^[0m - [91m |[0m Constructor or function already exists for Bar1 + [91m |[0m A union constructor or function already exists with name Bar1 [91m |[0m |