From 61511b89c9f8c03752e1b1247bf6744b8df8d87b Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Fri, 1 Nov 2024 09:58:45 -0500
Subject: [PATCH] Fix bug involving simulataneous overloading

---
 src/state.cpp           |  5 ++++-
 tests/CMakeLists.txt    |  1 +
 tests/simul-overload.eo | 19 +++++++++++++++++++
 3 files changed, 24 insertions(+), 1 deletion(-)
 create mode 100644 tests/simul-overload.eo

diff --git a/src/state.cpp b/src/state.cpp
index d357e359..9b8dabfc 100644
--- a/src/state.cpp
+++ b/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);
diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt
index e074a71d..9bb908b8 100644
--- a/tests/CMakeLists.txt
+++ b/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)
diff --git a/tests/simul-overload.eo b/tests/simul-overload.eo
new file mode 100644
index 00000000..02a15afd
--- /dev/null
+++ b/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))