From fab882d211cd62806930dd2b88f510c09a133fe3 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Wed, 26 Jul 2023 14:35:39 +0200 Subject: [PATCH] The warning has to be a smt-lib comment --- src/lib/frontend/models.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/lib/frontend/models.ml b/src/lib/frontend/models.ml index 5a6cd1f4b..0849ff6c8 100644 --- a/src/lib/frontend/models.ml +++ b/src/lib/frontend/models.ml @@ -483,7 +483,7 @@ let pp_constant ppf (_, t) = let output_concrete_model fmt props ~functions ~constants ~arrays = if ModelMap.(is_suspicious functions || is_suspicious constants || is_suspicious arrays) then - Format.fprintf fmt "This model is a best-effort. It includes symbols + Format.fprintf fmt "; This model is a best-effort. It includes symbols for which model generation is known to be incomplete. @."; Format.fprintf fmt "@[(";