Fix for non-symbols

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

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())
     {

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)

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)))