From f005dc6f28ecf13b16636143b57da878fff30dc2 Mon Sep 17 00:00:00 2001 From: Pierrot Date: Fri, 13 Oct 2023 17:39:35 +0200 Subject: [PATCH] Update src/lib/reasoners/shostak.ml MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Basile Clément <129742207+bclement-ocp@users.noreply.github.com> --- src/lib/reasoners/shostak.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/lib/reasoners/shostak.ml b/src/lib/reasoners/shostak.ml index c60508baa0..53c5819ccb 100644 --- a/src/lib/reasoners/shostak.ml +++ b/src/lib/reasoners/shostak.ml @@ -647,7 +647,7 @@ struct List.exists (fun (t,_) -> Expr.const_term t) eq then None else Some (Expr.fresh_name ty, false) (* false <-> not a case-split *) | _ -> - (* There is no mode-generation support for the AC symbols yet. + (* There is no model-generation support for the AC symbols yet. The function [AC.assign_value] always returns [None]. *) AC.assign_value r distincts eq in