From 6a3201b01c13c35f1df25d97db2d39e173739cf8 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Wed, 12 Feb 2025 14:22:23 -0600
Subject: [PATCH] Fix for non-symbols

---
 src/expr_info.h          |  7 +++++++
 src/state.cpp            |  5 +++--
 tests/CMakeLists.txt     |  1 +
 tests/overload-define.eo | 10 ++++++++++
 4 files changed, 21 insertions(+), 2 deletions(-)
 create mode 100644 tests/overload-define.eo

diff --git a/src/expr_info.h b/src/expr_info.h
index b0dc510..0a04812 100644
--- a/src/expr_info.h
+++ b/src/expr_info.h
@@ -40,6 +40,13 @@ class AppInfo
    * term.
    */
   bool d_isOverloaded;
+  /**
+   * The name of the symbol, if overloaded. Note this is required to handle
+   * cases where symbols are bound to terms that do not have their given
+   * name, e.g. (define s () (+ 1 1)) maps "s" to the term (+ 1 1), which
+   * does not have the name "s".
+   */
+  std::string d_overloadName;
 };
 
 }  // namespace ethos
diff --git a/src/state.cpp b/src/state.cpp
index b45a6ed..8e743c5 100644
--- a/src/state.cpp
+++ b/src/state.cpp
@@ -671,7 +671,7 @@ Expr State::mkExpr(Kind k, const std::vector<Expr>& children)
       if (ai->d_isOverloaded)
       {
         Trace("overload") << "Use overload when constructing " << k << " " << children << std::endl;
-        std::vector<Expr>& ov = d_overloads[children[0].getSymbol()];
+        std::vector<Expr>& ov = d_overloads[ai->d_overloadName];
         Assert (ov.size()>=2);
         Expr ret = getOverloadInternal(ov, children);
         if (!ret.isNull())
@@ -954,7 +954,7 @@ Expr State::mkExpr(Kind k, const std::vector<Expr>& children)
       if (ai!=nullptr && ai->d_isOverloaded)
       {
         Trace("overload") << "...overloaded" << std::endl;
-        std::vector<Expr>& ov = d_overloads[children[0].getSymbol()];
+        std::vector<Expr>& ov = d_overloads[ai->d_overloadName];
         Assert (ov.size()>=2);
         reto = getOverloadInternal(ov, dummyChildren, ftype.second.getValue());
       }
@@ -1147,6 +1147,7 @@ bool State::bind(const std::string& name, const Expr& e)
     // if already bound, mark as overloaded
     AppInfo& ain = d_appData[e.getValue()];
     ain.d_isOverloaded = true;
+    ain.d_overloadName = name;
     std::vector<Expr>& ov = d_overloads[name];
     if (ov.empty())
     {
diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt
index b2f43d8..ca0871b 100644
--- a/tests/CMakeLists.txt
+++ b/tests/CMakeLists.txt
@@ -139,6 +139,7 @@ set(ethos_test_file_list
     param-dt-parse-amb-fun.eo
     datatypes-split-rule-param.eo
     datatypes-split-rule-param-uinst.eo
+    overload-define.eo
 )
 
 if(ENABLE_ORACLES)
diff --git a/tests/overload-define.eo b/tests/overload-define.eo
new file mode 100644
index 0000000..0ffba64
--- /dev/null
+++ b/tests/overload-define.eo
@@ -0,0 +1,10 @@
+(declare-type Int ())
+(declare-consts <numeral> Int)
+(declare-const f (-> Int Int Int))
+
+(define g () (f 0))
+(define g () (f 1))
+
+(declare-const P (-> Int Bool))
+
+(assume @p0 (P (g 0)))