Add comment about AC model-generation support

OCamlPro · Oct 9, 2023 · 25defb2 · 25defb2
1 parent 403a4d3
commit 25defb2
Showing 1 changed file with 4 additions and 1 deletion.
diff --git 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