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