From 0e5efa8c4ff22925d3fc011a3588a3e67c107d0e Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 16 Dec 2019 00:22:40 -0600
Subject: [PATCH] Minor improvement to evaluator (#3570)

Fixes a bug where we don't return the partially evaluated version (for unevaluatable nodes). Also adds `NONLINEAR_MULT` whose semantics is identical to `MULT`.
---
 src/theory/evaluator.cpp | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp
index ae573956f..67ac255ee 100644
--- a/src/theory/evaluator.cpp
+++ b/src/theory/evaluator.cpp
@@ -122,7 +122,8 @@ Node Evaluator::eval(TNode n,
                      << " " << vals << std::endl;
   std::unordered_map<TNode, Node, NodeHashFunction> evalAsNode;
   Node ret = evalInternal(n, args, vals, evalAsNode).toNode();
-  if (!ret.isNull())
+  // 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 =
@@ -357,6 +358,7 @@ EvalResult Evaluator::evalInternal(
           break;
         }
         case kind::MULT:
+        case kind::NONLINEAR_MULT:
         {
           Rational res = results[currNode[0]].d_rat;
           for (size_t i = 1, end = currNode.getNumChildren(); i < end; i++)
-- 
2.30.2