Avoid spurious list computation

cvc5 · Apr 3, 2024 · bc7facb · bc7facb
1 parent 66e6445
commit bc7facb
Show file tree

Hide file tree

Showing 3 changed files with 22 additions and 0 deletions.
diff --git a/src/kind.cpp b/src/kind.cpp
@@ -224,5 +224,20 @@ bool isLiteralOp(Kind k)
   }
   return false;
 }
+bool isListLiteralOp(Kind k)
+{
+  switch (k)
+  {
+    case Kind::EVAL_NIL:
+    case Kind::EVAL_CONS:
+    case Kind::EVAL_CONCAT:
+    case Kind::EVAL_EXTRACT:
+    case Kind::EVAL_FIND:
+      return true;
+    default:
+      break;
+  }
+  return false;
+}
 
 }  // namespace alfc
diff --git a/src/kind.h b/src/kind.h
@@ -102,6 +102,8 @@ bool isSymbol(Kind k);
 bool isLiteral(Kind k);
 /** */
 bool isLiteralOp(Kind k);
+/** Is k a list literal operator? */
+bool isListLiteralOp(Kind k);
 
 }  // namespace alfc
 

diff --git a/src/type_checker.cpp b/src/type_checker.cpp
@@ -1154,6 +1154,10 @@ Expr TypeChecker::evaluateLiteralOpInternal(
     Trace("type_checker") << "...value-evaluates to " << lit << std::endl;
     return lit;
   }
+  if (!isListLiteralOp(k))
+  {
+    return d_null;
+  }
   // otherwise, maybe a list operation
   ExprValue* op = args[0];
   // strip off parameterized to look up AppInfo
@@ -1398,6 +1402,7 @@ bool TypeChecker::computedParameterizedInternal(AppInfo* ai,
     {
       // if not in an application, we fail
       Warning() << "Failed to determine parameters for " << hd << std::endl;
+      AlwaysAssert(false);
       return false;
     }
     else