mirror of
https://github.com/Z3Prover/z3
synced 2026-02-09 10:35:36 +00:00
Add explanatory comment for parameter count validation
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
parent
087e475722
commit
ac22b4822a
1 changed files with 3 additions and 0 deletions
|
|
@ -322,6 +322,9 @@ namespace datatype {
|
|||
}
|
||||
}
|
||||
|
||||
// Check if the datatype has already been registered with a different number of parameters.
|
||||
// Note: num_parameters includes the datatype name as the first parameter, so we subtract 1
|
||||
// to compare with the def's parameter count which doesn't include the name.
|
||||
def* d = nullptr;
|
||||
if (m_defs.find(name.get_symbol(), d) && d->params().size() != num_parameters - 1) {
|
||||
throw default_exception("datatype has already been registered but with a different number of parameters");
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue