mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

fix #5589

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-10-11 11:03:15 -07:00
parent 75702c3631
commit 73102cffcb
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/datatype_decl_plugin.cpp
View file

@ -406,7 +406,7 @@ namespace datatype {
VALIDATE_PARAM(arity == 1 && num_parameters == 1 && parameters[0].is_ast() && is_func_decl(parameters[0].get_ast()));
VALIDATE_PARAM(u().is_datatype(domain[0]));
VALIDATE_PARAM_PP(domain[0] == to_func_decl(parameters[0].get_ast())->get_range(), "invalid sort argument passed to recognizer");
// blindly trust that parameter is a constructor
VALIDATE_PARAM_PP(u().is_constructor(to_func_decl(parameters[0].get_ast())), "expecting constructor argument to recognizer");
sort* range = m_manager->mk_bool_sort();
func_decl_info info(m_family_id, OP_DT_IS, num_parameters, parameters);
info.m_private_parameters = true;