mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-14 18:06:15 +00:00
Code Activity

fix #4725

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-10-06 08:41:30 -07:00
parent 1131fedb23
commit 1d8d58710c
1 changed files with 5 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/ast/ast.cpp
View file

@ -1143,11 +1143,13 @@ func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
case OP_DISTINCT: { case OP_DISTINCT: {
func_decl_info info(m_family_id, OP_DISTINCT); func_decl_info info(m_family_id, OP_DISTINCT);
info.set_pairwise(); info.set_pairwise();
ptr_buffer<sort> sorts;
for (unsigned i = 1; i < arity; i++) { for (unsigned i = 1; i < arity; i++) {
if (domain[i] != domain[0]) { if (domain[i] != domain[0]) {
std::ostringstream buffer; sort* srt = join(arity, domain);
buffer << "Sort mismatch between first argument and argument " << (i+1); for (unsigned j = 0; j < arity; ++j)
throw ast_exception(buffer.str()); sorts.push_back(srt);
domain = sorts.c_ptr();
} }
} }
return m_manager->mk_func_decl(symbol("distinct"), arity, domain, m_bool_sort, info); return m_manager->mk_func_decl(symbol("distinct"), arity, domain, m_bool_sort, info);