diff options
| -rw-r--r-- | src/type_check.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/type_check.ml b/src/type_check.ml index 92425daa..7af0ecff 100644 --- a/src/type_check.ml +++ b/src/type_check.ml @@ -2210,15 +2210,17 @@ let rec rewrite_sizeof' env (Nexp_aux (aux, l) as nexp) = let exp = rewrite_sizeof' env nexp in mk_exp (E_app (mk_id "pow2", [exp])) + (* SMT solver div/mod is euclidian, so we must use those versions of + div and mod in lib/smt.sail *) | Nexp_app (id, [nexp1; nexp2]) when string_of_id id = "div" -> let exp1 = rewrite_sizeof' env nexp1 in let exp2 = rewrite_sizeof' env nexp2 in - mk_exp (E_app (mk_id "div", [exp1; exp2])) + mk_exp (E_app (mk_id "ediv_int", [exp1; exp2])) | Nexp_app (id, [nexp1; nexp2]) when string_of_id id = "mod" -> let exp1 = rewrite_sizeof' env nexp1 in let exp2 = rewrite_sizeof' env nexp2 in - mk_exp (E_app (mk_id "mod", [exp1; exp2])) + mk_exp (E_app (mk_id "emod_int", [exp1; exp2])) | Nexp_app _ | Nexp_id _ -> typ_error env l ("Cannot re-write sizeof(" ^ string_of_nexp nexp ^ ")") |