Another

cvc5 · Jan 15, 2025 · c37d439 · c37d439
1 parent 2014ae5
commit c37d439
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/src/type_checker.cpp b/src/type_checker.cpp
@@ -1217,7 +1217,9 @@ Expr TypeChecker::evaluateLiteralOpInternal(
     case Kind::EVAL_DT_CONSTRUCTORS:
     case Kind::EVAL_DT_SELECTORS:
     {
-      AppInfo* ac = d_state.getAppInfo(args[0]);
+      Expr sym(args[0]);
+      sym = sym.getKind()==Kind::APPLY_OPAQUE ? sym[0] : sym;
+      AppInfo* ac = d_state.getAppInfo(sym.getValue());
       if (ac != nullptr)
       {
         Assert(args[0]->isGround());