From d06e48a36163934c8058a1d7491c55a26c7e0a49 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 7 Jul 2017 08:13:14 -0700
Subject: [PATCH] detect overlapping signatures #1134

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/cmd_context/cmd_context.cpp | 26 +++++++++++++++++++++++---
 src/cmd_context/cmd_context.h   |  1 +
 2 files changed, 24 insertions(+), 3 deletions(-)

diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index d252c3629..6a8b7f79b 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -72,14 +72,34 @@ void func_decls::finalize(ast_manager & m) {
     m_decls = 0;
 }
 
+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;
+}
+
 bool func_decls::contains(func_decl * f) const {
     if (GET_TAG(m_decls) == 0) {
-        return UNTAG(func_decl*, m_decls) == f;
+        func_decl* g = UNTAG(func_decl*, m_decls);
+        if (!g) return false;
+        return signatures_collide(f, g);
     }
     else {
         func_decl_set * fs = UNTAG(func_decl_set *, m_decls);
-        return fs->contains(f);
+        for (func_decl* g : *fs) {
+            if (signatures_collide(f, g)) return true;
+        }
     }
+    return false;
 }
 
 bool func_decls::insert(ast_manager & m, func_decl * f) {
@@ -661,7 +681,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";
+        msg += "' (with the given signature) already declared with an overlapping signature";
         throw cmd_exception(msg.c_str());
     }
     if (s != f->get_name()) {
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index b231e3c82..74b2f3fbc 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -42,6 +42,7 @@ Notes:
 
 class func_decls {
     func_decl * m_decls;
+    bool signatures_collide(func_decl* f, func_decl* g) const;
 public:
     func_decls():m_decls(0) {}
     func_decls(ast_manager & m, func_decl * f);