From 5ee3c8d02e21b1c20bfe56538c4cbe4fed0481eb Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 16 Dec 2019 10:28:51 -0600
Subject: [PATCH] Revert evaluate as node. (#3574)

---
 src/theory/evaluator.cpp | 14 +-------------
 1 file changed, 1 insertion(+), 13 deletions(-)

diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp
index 67ac255ee..406fb5ead 100644
--- a/src/theory/evaluator.cpp
+++ b/src/theory/evaluator.cpp
@@ -121,19 +121,7 @@ Node Evaluator::eval(TNode n,
   Trace("evaluator") << "Evaluating " << n << " under substitution " << args
                      << " " << vals << std::endl;
   std::unordered_map<TNode, Node, NodeHashFunction> evalAsNode;
-  Node ret = evalInternal(n, args, vals, evalAsNode).toNode();
-  // if we failed to evaluate
-  if (ret.isNull())
-  {
-    // maybe it was stored in the evaluation-as-node map
-    std::unordered_map<TNode, Node, NodeHashFunction>::iterator itn =
-        evalAsNode.find(n);
-    if (itn != evalAsNode.end())
-    {
-      return itn->second;
-    }
-  }
-  return ret;
+  return evalInternal(n, args, vals, evalAsNode).toNode();
 }
 
 EvalResult Evaluator::evalInternal(
-- 
2.30.2