diff --git a/src/plugins/instantiate/stdlib/calloc.ml b/src/plugins/instantiate/stdlib/calloc.ml index 86eada6103dfa765956508a1e25c231a346199d9..1e064706c5b6eb1a4230eb414f71e60a1fc9689e 100644 --- a/src/plugins/instantiate/stdlib/calloc.ml +++ b/src/plugins/instantiate/stdlib/calloc.ml @@ -34,7 +34,7 @@ let pset_len_to_zero ?loc alloc_type num size = let value = match Logic_utils.unroll_type t.term_type with | Ctype(TPtr(_)) -> term Tnull t.term_type | Ctype(TFloat(_)) -> treal ?loc 0. - | Ctype(TInt(_)) -> tinteger ?loc 0 + | Ctype(TInt(_) | TEnum (_)) -> tinteger ?loc 0 | _ -> unexpected "non atomic type during equality generation" in prel ?loc (Req, t, value) diff --git a/src/plugins/instantiate/string/memset.ml b/src/plugins/instantiate/string/memset.ml index 3eef4cdd5b9741dd0b14945dc882619acf235574..a8fc72f07a5e07f87da3a60a50c675b67750d6ee 100644 --- a/src/plugins/instantiate/string/memset.ml +++ b/src/plugins/instantiate/string/memset.ml @@ -68,7 +68,7 @@ let pset_len_bytes_to_zero ?loc ptr bytes_len = let value = match Logic_utils.unroll_type t.term_type with | Ctype(TPtr(_)) -> term Tnull t.term_type | Ctype(TFloat(_)) -> treal ?loc 0. - | Ctype(TInt(_)) -> tinteger ?loc 0 + | Ctype(TInt(_) | TEnum (_)) -> tinteger ?loc 0 | _ -> unexpected "non atomic type during equality generation" in prel ?loc (Req, t, value)