Fixes

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

Hide file tree

Showing 2 changed files with 8 additions and 2 deletions.
diff --git a/src/kind.cpp b/src/kind.cpp
@@ -54,7 +54,7 @@ std::ostream& operator<<(std::ostream& o, Kind k)
     case Kind::EVAL_TYPE_OF: o << "EVAL_TYPE_OF"; break;
     case Kind::EVAL_NAME_OF: o << "EVAL_NAME_OF"; break;
     // lists
-    case Kind::EVAL_NIL: o << "EVAL_EMPTYLIST";break;
+    case Kind::EVAL_NIL: o << "EVAL_NIL";break;
     case Kind::EVAL_CONS: o << "EVAL_CONS"; break;
     // boolean
     case Kind::EVAL_NOT: o << "EVAL_NOT"; break;

diff --git a/src/type_checker.cpp b/src/type_checker.cpp
@@ -1174,7 +1174,13 @@ Expr TypeChecker::evaluateLiteralOpInternal(
   bool isLeft = (ck==Attr::LEFT_ASSOC_NIL);
   Trace("type_checker_debug") << "EVALUATE-LIT (list) " << k << " " << isLeft << " " << args << std::endl;
   // infer the nil expression, which depends on the type of args[1]
-  Expr nilExpr = computeConstructorTermInternal(ac, {Expr(args[0]), Expr(args[1])});
+  std::vector<Expr> eargs;
+  eargs.emplace_back(args[0]);
+  if (args.size()>1)
+  {
+    eargs.emplace_back(args[1]);
+  }
+  Expr nilExpr = computeConstructorTermInternal(ac, eargs);
   if (nilExpr.isNull())
   {
     Trace("type_checker") << "...failed to get nil" << std::endl;