From 1d8d58710c0bf9129bbeee43dff43cdab2c1b4a5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 6 Oct 2020 08:41:30 -0700 Subject: [PATCH] fix #4725 Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index fb584d932..4f4d1be6e 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1143,11 +1143,13 @@ func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters case OP_DISTINCT: { func_decl_info info(m_family_id, OP_DISTINCT); info.set_pairwise(); + ptr_buffer sorts; for (unsigned i = 1; i < arity; i++) { if (domain[i] != domain[0]) { - std::ostringstream buffer; - buffer << "Sort mismatch between first argument and argument " << (i+1); - throw ast_exception(buffer.str()); + sort* srt = join(arity, domain); + for (unsigned j = 0; j < arity; ++j) + sorts.push_back(srt); + domain = sorts.c_ptr(); } } return m_manager->mk_func_decl(symbol("distinct"), arity, domain, m_bool_sort, info);