Revert evaluate as node. (#3574)

diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp
index 67ac255ee8314843f57610d1b7d844889149a030..406fb5ead7322a4d847450b9a4f3b73525088956 100644 (file)
--- 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(