From ea331ebfbedf47381df1b3fd2ef296c850de3405 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 7 Jul 2017 08:29:16 -0700 Subject: [PATCH] revert update to #1134 Signed-off-by: Nikolaj Bjorner --- src/cmd_context/cmd_context.cpp | 18 +++--------------- 1 file changed, 3 insertions(+), 15 deletions(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 6a8b7f79b..a053fc8e6 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -73,25 +73,13 @@ void func_decls::finalize(ast_manager & m) { } bool func_decls::signatures_collide(func_decl* f, func_decl* g) const { - if (f == g) { - return true; - } - if (f->get_arity() != g->get_arity() || f->get_range() == g->get_range()) { - return false; - } - for (unsigned i = 0; i < f->get_arity(); ++i) { - if (f->get_domain(i) != g->get_domain(i)) - return false; - } - // they have the same type arguments, but different range types. - return true; + return f == g; } bool func_decls::contains(func_decl * f) const { if (GET_TAG(m_decls) == 0) { func_decl* g = UNTAG(func_decl*, m_decls); - if (!g) return false; - return signatures_collide(f, g); + return g && signatures_collide(f, g); } else { func_decl_set * fs = UNTAG(func_decl_set *, m_decls); @@ -681,7 +669,7 @@ void cmd_context::insert(symbol const & s, func_decl * f) { msg += f->get_arity() == 0 ? "constant" : "function"; msg += " '"; msg += s.str(); - msg += "' (with the given signature) already declared with an overlapping signature"; + msg += "' (with the given signature) already declared"; throw cmd_exception(msg.c_str()); } if (s != f->get_name()) {