diff --git a/src/kernel_services/abstract_interp/abstract_memory.ml b/src/kernel_services/abstract_interp/abstract_memory.ml index eda3508918218396e5d96fe2e462cbf82f40f3ab..a250acd10d3dbc8ef2708abc90c9b5cebabf49d6 100644 --- a/src/kernel_services/abstract_interp/abstract_memory.ml +++ b/src/kernel_services/abstract_interp/abstract_memory.ml @@ -331,6 +331,8 @@ struct let pretty fmt : t -> unit = function | Const i -> Integer.pretty fmt i | Exp (e,i) when Integer.is_zero i -> Exp.pretty fmt e + | Exp (e,i) when Integer.(lt i zero) -> + Format.fprintf fmt "%a - %a" Exp.pretty e Integer.pretty (Integer.neg i) | Exp (e,i) -> Format.fprintf fmt "%a + %a" Exp.pretty e Integer.pretty i | _ -> raise Not_implemented