Fix for symbol overloading

src/state.cpp

@@ -213,18 +213,15 @@ void State::popScope()
     if (!d_overloadedDecls.empty() && d_overloadedDecls.back()==d_decls[i])
     {
       d_overloadedDecls.pop_back();
+      std::map<std::string, Expr>::iterator its = d_symTable.find(d_decls[i]);
+      Assert (its!=d_symTable.end());
       // it should be overloaded
-      AppInfo* ai = getAppInfo(d_symTable[d_decls[i]].getValue());
+      AppInfo* ai = getAppInfo(its->second.getValue());
       Assert (ai!=nullptr);
-      Assert (!ai->d_overloads.empty());
+      Assert (ai->d_overloads.size()>=2);
+      // was overloaded, we revert the binding
       ai->d_overloads.pop_back();
-      if (ai->d_overloads.size()==1)
-      {
-        Trace("overload") << "** no-overload: " << d_decls[i] << std::endl;
-        // no longer overloaded since the overload vector is now size one
-        ai->d_overloads.clear();
-      }
-      // was overloaded, so we don't unbind
+      its->second = ai->d_overloads.back();
       continue;
     }
     d_symTable.erase(d_decls[i]);
@@ -723,7 +720,7 @@ Expr State::mkExpr(Kind k, const std::vector<Expr>& children)
               }
               i++;
             }
-            Trace("type_checker") << "...return for " << children[0] << std::endl;// << ": " << Expr(curr) << std::endl;
+            Trace("type_checker") << "...return for " << children[0] << std::endl;
             return Expr(curr);
           }
           // otherwise partial??
@@ -1080,22 +1077,27 @@ bool State::bind(const std::string& name, const Expr& e)
   std::map<std::string, Expr>::iterator its = d_symTable.find(name);
   if (its!=d_symTable.end())
   {
+    Trace("overload") << "** overload: " << name << std::endl;
     // if already bound, we overload
     AppInfo& ai = d_appData[its->second.getValue()];
-    // if the first time overloading, add the original
-    if (ai.d_overloads.empty())
+    std::vector<Expr>& ov = ai.d_overloads;
+    AppInfo& ain = d_appData[e.getValue()];
+    std::vector<Expr>& ovn = ain.d_overloads;
+    if (ov.empty())
+    {
+      // if first time overloading, add the original symbol
+      ovn.emplace_back(its->second);
+    }
+    else
     {
-      Trace("overload") << "** overload: " << name << std::endl;
-      ai.d_overloads.push_back(its->second);
+      ovn.insert(ovn.end(), ov.begin(), ov.end());
     }
-    ai.d_overloads.push_back(e);
+    ovn.emplace_back(e);
     // add to declaration
     if (!d_declsSizeCtx.empty())
     {
-      d_decls.emplace_back(name);
       d_overloadedDecls.emplace_back(name);
     }
-    return true;
   }
   // Trace("state-debug") << "bind " << name << " -> " << &e << std::endl;
   d_symTable[name] = e;