1 files changed, 9 insertions, 10 deletions
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index cd974d3e4..24ea16c9f 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -287,17 +287,16 @@ void TheoryUF::preRegisterTerm(TNode node)
   case kind::COMBINED_CARDINALITY_CONSTRAINT:
     //do nothing
     break;
-  case kind::UNINTERPRETED_CONSTANT:
+  case kind::ABSTRACT_VALUE:
   {
-    // Uninterpreted constants should only appear in models, and should
-    // never appear in constraints. They are unallowed to ever appear in
-    // constraints since the cardinality of an uninterpreted sort may have
-    // an upper bound, e.g. if (forall ((x U) (y U)) (= x y)) holds, then
-    // @uc_U_2 is a ill-formed term, as its existence cannot be assumed.
-    // The parser prevents the user from ever constructing uninterpreted
-    // constants. However, they may be exported via models to API users.
-    // It is thus possible that these uninterpreted constants are asserted
-    // back in constraints, hence this check is necessary.
+    // Abstract values should only appear in models, and should never appear in
+    // constraints. They are unallowed to ever appear in constraints since the
+    // cardinality of an uninterpreted sort may have an upper bound, e.g. if
+    // (forall ((x U) (y U)) (= x y)) holds, then @uc_U_2 is a ill-formed term,
+    // as its existence cannot be assumed.  The parser prevents the user from
+    // ever constructing abstract values. However, they may be exported via
+    // models to API users.  It is thus possible that these abstract values are
+    // asserted back in constraints, hence this check is necessary.
     throw LogicException(
         "An uninterpreted constant was preregistered to the UF theory.");
   }