Relax an assertion in the evaluator (#8751)

In a rare case this can throw after https://github.com/cvc5/cvc5/pull/8740, complaining that `(/ 0.0 0)` and `(/ 0.0 0.0)` are not the same.

diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp
index ab03ba3953731fce8a0180d00708ad3f91546933..51e0357e60ac69c95e561de362b88c6e2eb17946 100644 (file)
--- a/src/theory/evaluator.cpp
+++ b/src/theory/evaluator.cpp
@@ -169,19 +169,24 @@ Node Evaluator::eval(TNode n,
   Node ret =
       evalInternal(n, args, vals, evalAsNode, results).toNode(n.getType());
   // if we failed to evaluate
-  if (ret.isNull() && d_rr != nullptr)
+  if (d_rr != nullptr)
   {
-    // should be stored in the evaluation-as-node map
-    std::unordered_map<TNode, Node>::iterator itn = evalAsNode.find(n);
-    Assert(itn != evalAsNode.end());
-    ret = d_rr->rewrite(itn->second);
+    if (ret.isNull())
+    {
+      // should be stored in the evaluation-as-node map
+      std::unordered_map<TNode, Node>::iterator itn = evalAsNode.find(n);
+      Assert(itn != evalAsNode.end());
+      ret = itn->second;
+    }
+    // always rewrite, which can change if the evaluation was not a constant
+    ret = d_rr->rewrite(ret);
   }
   // should be the same as substitution + rewriting, or possibly null if
-  // d_rr is nullptr
-  Assert((ret.isNull() && d_rr == nullptr)
+  // d_rr is nullptr or non-constant
+  Assert(((ret.isNull() || !ret.isConst()) && d_rr == nullptr)
          || ret
                 == d_rr->rewrite(n.substitute(
-                    args.begin(), args.end(), vals.begin(), vals.end())));
+                       args.begin(), args.end(), vals.begin(), vals.end())));
   return ret;
 }