4 files changed, 0 insertions, 32 deletions
diff --git a/src/expr/mkexpr b/src/expr/mkexpr
index 010ec9a2e..c5f12f487 100755
--- a/src/expr/mkexpr
+++ b/src/expr/mkexpr
@@ -65,7 +65,6 @@ exportConstant_cases=
 
 typerules=
 construles=
-neverconstrules=
 
 seen_theory=false
 seen_theory_builtin=false
@@ -169,12 +168,6 @@ function construle {
 #line $lineno \"$kf\"
     return $2::computeIsConst(nodeManager, n);
 "
-  neverconstrules="${neverconstrules}
-#line $lineno \"$kf\"
-  case kind::$1:
-#line $lineno \"$kf\"
-    return false;
-"
 }
 
 function sort {
@@ -311,7 +304,6 @@ for var in \
     typechecker_includes \
     typerules \
     construles \
-    neverconstrules \
     ; do
   eval text="\${text//\\\$\\{$var\\}/\${$var}}"
 done
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index de1d5475b..a8fc9d54c 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -91,10 +91,6 @@ bool NodeTemplate<ref_count>::isConst() const {
     Debug("isConst") << "Node::isConst() returning false, it's a VARIABLE" << std::endl;
     return false;
   default:
-    if(expr::TypeChecker::neverIsConst(NodeManager::currentNM(), *this)){
-      Debug("isConst") << "Node::isConst() returning false, the kind is never const" << std::endl;
-      return false;
-    }
     if(getAttribute(IsConstComputedAttr())) {
       bool bval = getAttribute(IsConstAttr());
       Debug("isConst") << "Node::isConst() returning cached value " << (bval ? "true" : "false") << " for: " << *this << std::endl;
diff --git a/src/expr/type_checker.h b/src/expr/type_checker.h
index 8c03cea98..bf0229bf8 100644
--- a/src/expr/type_checker.h
+++ b/src/expr/type_checker.h
@@ -33,8 +33,6 @@ public:
 
  static bool computeIsConst(NodeManager* nodeManager, TNode n);
 
- static bool neverIsConst(NodeManager* nodeManager, TNode n);
-
 };/* class TypeChecker */
 
 }/* CVC4::expr namespace */
diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp
index 375fbd515..3ed12cf6a 100644
--- a/src/expr/type_checker_template.cpp
+++ b/src/expr/type_checker_template.cpp
@@ -77,23 +77,5 @@ ${construles}
 
 }/* TypeChecker::computeIsConst */
 
-bool TypeChecker::neverIsConst(NodeManager* nodeManager, TNode n)
-{
-  Assert(n.getMetaKind() == kind::metakind::OPERATOR
-         || n.getMetaKind() == kind::metakind::PARAMETERIZED
-         || n.getMetaKind() == kind::metakind::NULLARY_OPERATOR);
-
-  switch(n.getKind()) {
-${neverconstrules}
-
-#line 90 "${template}"
-
-    default:;
-  }
-
-  return true;
-
-}/* TypeChecker::neverIsConst */
-
 }/* CVC4::expr namespace */
 }/* CVC4 namespace */