Fix bug involving simulataneous overloading

src/state.cpp

@@ -206,8 +206,10 @@ void State::popScope()
   }
   size_t lastSize = d_declsSizeCtx.back();
   d_declsSizeCtx.pop_back();
-  for (size_t i=lastSize, currSize = d_decls.size(); i<currSize; i++)
+  size_t i = d_decls.size();
+  while (i>lastSize)
   {
+    i--;
     // Check if overloaded, which is the case if the last overloaded
     // declaration had the same name.
     if (!d_overloadedDecls.empty() && d_overloadedDecls.back()==d_decls[i])
@@ -225,6 +227,7 @@ void State::popScope()
       its->second = ai->d_overloads.back();
       continue;
     }
+    Trace("overload") << "** unbind " << d_decls[i] << std::endl;
     d_symTable.erase(d_decls[i]);
   }
   d_decls.resize(lastSize);

tests/CMakeLists.txt

@@ -128,6 +128,7 @@ set(ethos_test_file_list
     simple-lra-reference.eo
     left-cons.eo
     overload-standalone.eo
+    simul-overload.eo
 )
 
 if(ENABLE_ORACLES)

tests/simul-overload.eo

@@ -0,0 +1,19 @@
+
+
+(declare-const = (-> (! Type :var A :implicit) A A Bool))
+
+(declare-rule refl ((T Type) (t T))
+    :args (t)
+    :conclusion (= t t)
+)
+(declare-type @List ())
+(declare-const @list.nil @List)
+(declare-const @list (-> (! Type :var T :implicit) T @List @List) :right-assoc-nil @list.nil)
+(declare-const forall (-> @List Bool Bool) :binder @list)
+
+(declare-type Int ())
+(declare-const a Int)
+(declare-const b Int)
+
+(step @p99 :rule refl :args ((forall ((a Int) (b Int)))))
+(step @p106 :rule refl :args (a))