3 files changed, 17 insertions, 2 deletions
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index fca79aff0..6a6fb2e31 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -300,7 +300,12 @@ operator SEXPR 0: "a symbolic expression"
 
 operator LAMBDA 2 "lambda"
 
-parameterized CHAIN BUILTIN 2: "chain operator"
+parameterized CHAIN CHAIN_OP 2: "chained operator"
+constant CHAIN_OP \
+    ::CVC4::Chain \
+    ::CVC4::ChainHashFunction \
+    "util/chain.h" \
+    "the chained operator"
 
 constant TYPE_CONSTANT \
     ::CVC4::TypeConstant \
@@ -344,6 +349,7 @@ typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule
 typerule SEXPR ::CVC4::theory::builtin::SExprTypeRule
 typerule LAMBDA ::CVC4::theory::builtin::LambdaTypeRule
 typerule CHAIN ::CVC4::theory::builtin::ChainTypeRule
+typerule CHAIN_OP ::CVC4::theory::builtin::ChainedOperatorTypeRule
 
 constant SUBTYPE_TYPE \
     ::CVC4::Predicate \
diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp
index 4d62ce511..392e146ba 100644
--- a/src/theory/builtin/theory_builtin_rewriter.cpp
+++ b/src/theory/builtin/theory_builtin_rewriter.cpp
@@ -16,6 +16,7 @@
  **/
 
 #include "theory/builtin/theory_builtin_rewriter.h"
+#include "util/chain.h"
 
 using namespace std;
 
@@ -53,7 +54,7 @@ Node TheoryBuiltinRewriter::blastChain(TNode in) {
 
   Assert(in.getKind() == kind::CHAIN);
 
-  Kind chainedOp = in.getOperator().getConst<Kind>();
+  Kind chainedOp = in.getOperator().getConst<Chain>().getOperator();
 
   if(in.getNumChildren() == 2) {
     // if this is the case exactly 1 pair will be generated so the
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 2a4e07528..a04f9f88a 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -220,6 +220,14 @@ public:
   }
 };/* class ChainTypeRule */
 
+class ChainedOperatorTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
+    Assert(n.getKind() == kind::CHAIN_OP);
+    return nodeManager->getType(nodeManager->operatorOf(n.getConst<Chain>().getOperator()), check);
+  }
+};/* class ChainedOperatorTypeRule */
+
 class SortProperties {
 public:
   inline static bool isWellFounded(TypeNode type) {