From 25defb235f5f4fc40601c0db52f86fa360665d40 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Mon, 9 Oct 2023 09:53:50 +0200 Subject: [PATCH] Add comment about AC model-generation support --- src/lib/reasoners/shostak.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/lib/reasoners/shostak.ml b/src/lib/reasoners/shostak.ml index 95938cdfb..969c89d51 100644 --- a/src/lib/reasoners/shostak.ml +++ b/src/lib/reasoners/shostak.ml @@ -635,7 +635,10 @@ struct if Expr.const_term t || List.exists (fun (t,_) -> Expr.const_term t) eq then None else Some (Expr.fresh_name ty, false) (* false <-> not a case-split *) - | _ -> AC.assign_value r distincts eq + | _ -> + (* There is no mode-generation support for the AC symbols yet. + The function [AC.assign_value] always returns [None]. *) + AC.assign_value r distincts eq in if Options.get_debug_interpretation () then Printer.print_dbg