diff options
| -rw-r--r-- | src/theory/evaluator.cpp | 4 |
1 files changed, 3 insertions, 1 deletions
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++) |