From 9a8df8f80d6f8883ded8bdc9c2cfda8e148312c6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 14 Oct 2025 18:13:16 +0200 Subject: [PATCH] Update comments on parameter handling in api_datatype.cpp Clarify usage of parameters in API documentation. --- src/api/api_datatype.cpp | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/api/api_datatype.cpp b/src/api/api_datatype.cpp index c474bea37..886165455 100644 --- a/src/api/api_datatype.cpp +++ b/src/api/api_datatype.cpp @@ -317,12 +317,12 @@ extern "C" { sort_ref_vector params(m); - // If parameters are provided explicitly, use them - if (num_parameters > 0 && parameters) { - for (unsigned i = 0; i < num_parameters; ++i) { + // A correct use of the API is to always provide parameters explicitly. + // implicit parameters through polymorphic type variables does not work + // because the order of polymorphic variables in the parameters is ambiguous. + if (num_parameters > 0 && parameters) + for (unsigned i = 0; i < num_parameters; ++i) params.push_back(to_sort(parameters[i])); - } - } ptr_vector constrs; for (unsigned i = 0; i < num_constructors; ++i) {