Merge branch 'main' into dtList

cvc5 · Nov 1, 2024 · a143062 · a143062
2 parents 5ad6c63 + 84dd280
commit a143062
Show file tree

Hide file tree

Showing 4 changed files with 30 additions and 2 deletions.
diff --git a/src/state.cpp b/src/state.cpp
@@ -224,8 +224,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])
@@ -243,6 +245,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/src/type_checker.cpp b/src/type_checker.cpp
@@ -1364,7 +1364,12 @@ Expr TypeChecker::evaluateLiteralOpInternal(
       break;
     case Kind::EVAL_LIST_FIND:
     {
-      getNAryChildren(args[1], op, nil, hargs, isLeft);
+      ExprValue* a = getNAryChildren(args[1], op, nil, hargs, isLeft);
+      if (a==nullptr)
+      {
+        Trace("type_checker") << "...head not in list form" << std::endl;
+        return d_null;
+      }
       std::vector<ExprValue*>::iterator it = std::find(hargs.begin(), hargs.end(), args[2]);
       if (it==hargs.end())
       {

diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt
@@ -130,6 +130,7 @@ set(ethos_test_file_list
     overload-standalone.eo
     datatypes-split-rule.eo
     singular-datatype.eo
+    simul-overload.eo
 )
 
 if(ENABLE_ORACLES)

diff --git a/tests/simul-overload.eo 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)) true)))
+(step @p106 :rule refl :args (a))