diff --git a/proofs/eo/cpc/Cpc.eo b/proofs/eo/cpc/Cpc.eo
index ff8d097be6a..33530f63564 100644
--- a/proofs/eo/cpc/Cpc.eo
+++ b/proofs/eo/cpc/Cpc.eo
@@ -81,6 +81,15 @@
 ;   and are used to model cvc5's internal symbols, including its skolems,
 ;   other internally introduced terms, and extensions.
 
+; note: >
+;   @const corresponds to generic abstract constants, which correspond to internally
+;   introduced terms that do not have a formal definition in the signature.
+(declare-const @const (-> (! Int :opaque) (! Type :opaque :var T) T))
+
+; note: >
+;   @var is an alias of eo::var to ensure the cpc proof does not use eo::var.
+(define @var ((s String) (T Type)) (eo::var s T))
+
 ; disclaimer: this function is not in SMT-LIB.
 (declare-const fmf.card (-> Type Int Bool))
 ; disclaimer: this function is not in SMT-LIB.
diff --git a/proofs/eo/cpc/theories/Builtin.eo b/proofs/eo/cpc/theories/Builtin.eo
index 0a005d8907f..645f80c59e6 100644
--- a/proofs/eo/cpc/theories/Builtin.eo
+++ b/proofs/eo/cpc/theories/Builtin.eo
@@ -53,9 +53,5 @@
 
 (declare-const distinct (-> (! Type :var A :implicit) A A Bool) :pairwise and)
 
-; generic variables
-; NOTE: does not check that U is a numeral
-(declare-const const (-> (! Type :var U :implicit) (! U :opaque) (! Type :opaque :var T) T))
-
 ; The purification skolem.
 (declare-const @purify (-> (! Type :var A :implicit) (! A :opaque) A))
diff --git a/src/proof/alf/alf_node_converter.cpp b/src/proof/alf/alf_node_converter.cpp
index 44245570c17..afd4792dee4 100644
--- a/src/proof/alf/alf_node_converter.cpp
+++ b/src/proof/alf/alf_node_converter.cpp
@@ -83,7 +83,14 @@ Node AlfNodeConverter::postConvert(Node n)
     // dummy node, return it
     return n;
   }
-  if (k == Kind::SKOLEM || k == Kind::DUMMY_SKOLEM || k == Kind::INST_CONSTANT)
+  // case for skolems, unhandled variables, and other unhandled terms
+  // These should print as @const, or otherwise be printed as a skolem,
+  // which may need further processing below. In the case of unhandled
+  // terms (e.g. DT_SYGUS_EVAL), we prefer printing them as @const instead
+  // of using their smt2 printer, which would lead to undeclared identifiers in
+  // the proof.
+  if (k == Kind::SKOLEM || k == Kind::DUMMY_SKOLEM || k == Kind::INST_CONSTANT
+      || k == Kind::DT_SYGUS_EVAL)
   {
     TypeNode tn = n.getType();
     // constructors/selectors are represented by skolems, which are defined
@@ -110,7 +117,7 @@ Node AlfNodeConverter::postConvert(Node n)
     // is used as (var N T) throughout.
     Node index = d_nm->mkConstInt(Rational(getOrAssignIndexForConst(n)));
     Node tc = typeAsNode(tn);
-    return mkInternalApp("const", {index, tc}, tn);
+    return mkInternalApp("@const", {index, tc}, tn);
   }
   else if (k == Kind::BOUND_VARIABLE)
   {
@@ -127,7 +134,8 @@ Node AlfNodeConverter::postConvert(Node n)
       ss << n;
       sname = ss.str();
     }
-    // A variable x of type T can unambiguously referred to as (eo::var "x" T).
+    // A variable x of type T can unambiguously referred to as (@var "x" T),
+    // which is a macro for (eo::var "x" T) in the cpc signature.
     // We convert to this representation here, which will often be letified.
     TypeNode tn = n.getType();
     std::vector<Node> args;
@@ -135,7 +143,7 @@ Node AlfNodeConverter::postConvert(Node n)
     args.push_back(nn);
     Node tnn = typeAsNode(tn);
     args.push_back(tnn);
-    return mkInternalApp("eo::var", args, tn);
+    return mkInternalApp("@var", args, tn);
   }
   else if (k == Kind::VARIABLE)
   {
@@ -615,7 +623,6 @@ Node AlfNodeConverter::getOperatorOfTerm(Node n)
 
 size_t AlfNodeConverter::getOrAssignIndexForConst(Node v)
 {
-  Assert(v.isVar());
   std::map<Node, size_t>::iterator it = d_constIndex.find(v);
   if (it != d_constIndex.end())
   {
diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index 23a179b93ea..42be5f0f0ac 100644
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -2830,6 +2830,7 @@ set(regress_1_tests
   regress1/quantifiers/choice-move-delta-relt.smt2
   regress1/quantifiers/const.cvc.smt2
   regress1/quantifiers/constfunc.cvc.smt2
+  regress1/quantifiers/dd_verisec-dt-sygus.smt2
   regress1/quantifiers/dd.binary_trees.adb_1105_16_loop_invariant_init_1.smt2
   regress1/quantifiers/dd.bug812-ieval.smt2
   regress1/quantifiers/dd_ghc_macro_quant_prenex.smt2
diff --git a/test/regress/cli/regress1/quantifiers/dd_verisec-dt-sygus.smt2 b/test/regress/cli/regress1/quantifiers/dd_verisec-dt-sygus.smt2
new file mode 100644
index 00000000000..cc8229d6e77
--- /dev/null
+++ b/test/regress/cli/regress1/quantifiers/dd_verisec-dt-sygus.smt2
@@ -0,0 +1,6 @@
+; EXPECT: unsat
+; DISABLE-TESTER: unsat-core
+(set-logic NIA)
+(declare-const x Int)
+(assert (or (forall ((v Int) (v_ Int)) (or (= 1 v) (< 16777215 (mod (+ v_ (mod (+ x (mod v_ 8)) 53687091)) 33554432))))))
+(check-sat)