Format

cvc5 · Jan 24, 2025 · 4b9f66c · 4b9f66c
1 parent d4c7f5a
commit 4b9f66c
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 3 deletions.
diff --git a/src/kind.h b/src/kind.h
@@ -34,7 +34,7 @@ enum class Kind
   LAMBDA,
   TUPLE,
   PROGRAM,
-  AS,   // (eo::as t T), where T is the type of t
+  AS,         // (eo::as t T), where T is the type of t
   AS_RETURN,  // SMT-LIB (as t T), where T is the return type of t
   PARAMETERIZED,
   APPLY_OPAQUE,

diff --git a/src/state.cpp b/src/state.cpp
@@ -916,10 +916,11 @@ Expr State::mkExpr(Kind k, const std::vector<Expr>& children)
                 << ", " << children.size() << " arguments" << std::endl;
     }
   }
-  else if (k==Kind::AS_RETURN)
+  else if (k == Kind::AS_RETURN)
   {
     // (as nil (List Int)) --> (_ nil (List Int))
-    if (getConstructorKind(vchildren[0]) == Attr::AMB_DATATYPE_CONSTRUCTOR && children.size()==2)
+    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]});