Minor

cvc5 · Jan 24, 2025 · d4c7f5a · d4c7f5a
1 parent 15c4873
commit d4c7f5a
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/src/state.cpp b/src/state.cpp
@@ -919,11 +919,12 @@ Expr State::mkExpr(Kind k, const std::vector<Expr>& children)
   else if (k==Kind::AS_RETURN)
   {
     // (as nil (List Int)) --> (_ nil (List Int))
-    if (getConstructorKind(vchildren[0]) == Attr::AMB_DATATYPE_CONSTRUCTOR)
+    if (getConstructorKind(vchildren[0]) == Attr::AMB_DATATYPE_CONSTRUCTOR && children.size()==2)
     {
       Trace("overload") << "...type arg for ambiguous constructor" << std::endl;
       return mkExpr(Kind::APPLY_OPAQUE, {children[0], children[1]});
     }
+    // note we don't support other uses of `as` for symbol disambiguation yet
   }
   else if (k==Kind::AS)
   {