Fix bug in evaluator for division by zero (#7942)

Fixes #7917.

diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp
index 3552d0a31ec011283f07957da68b3b7442b0a4f1..6b4176c13e30c2d4af5fe9dd1f2e3fa8c7b22017 100644 (file)
--- a/src/theory/evaluator.cpp
+++ b/src/theory/evaluator.cpp
@@ -469,7 +469,12 @@ EvalResult Evaluator::evalInternal(
             }
             res = res / results[currNode[i]].d_rat;
           }
-          if (!divbyzero)
+          if (divbyzero)
+          {
+            processUnhandled(
+                currNode, currNodeVal, evalAsNode, results, needsReconstruct);
+          }
+          else
           {
             results[currNode] = EvalResult(res);
           }
@@ -894,10 +899,8 @@ EvalResult Evaluator::evalInternal(
         {
           Trace("evaluator") << "Kind " << currNodeVal.getKind()
                              << " not supported" << std::endl;
-          results[currNode] = EvalResult();
-          evalAsNode[currNode] =
-              needsReconstruct ? reconstruct(currNode, results, evalAsNode)
-                               : currNodeVal;
+          processUnhandled(
+              currNode, currNodeVal, evalAsNode, results, needsReconstruct);
         }
       }
     }
@@ -970,5 +973,15 @@ Node Evaluator::reconstruct(TNode n,
   return nn;
 }
 
+void Evaluator::processUnhandled(TNode n,
+                                 TNode nv,
+                                 std::unordered_map<TNode, Node>& evalAsNode,
+                                 std::unordered_map<TNode, EvalResult>& results,
+                                 bool needsReconstruct) const
+{
+  results[n] = EvalResult();
+  evalAsNode[n] = needsReconstruct ? reconstruct(n, results, evalAsNode) : Node(nv);
+}
+
 }  // namespace theory
 }  // namespace cvc5

diff --git a/src/theory/evaluator.h b/src/theory/evaluator.h
index bd10129e2a301466843b5a06c2051dbc8f4356d1..a850712777cfb7b5dbfe811e4aaf1f91be3a6692 100644 (file)
--- a/src/theory/evaluator.h
+++ b/src/theory/evaluator.h
@@ -159,6 +159,17 @@ class Evaluator
   Node reconstruct(TNode n,
                    std::unordered_map<TNode, EvalResult>& eresults,
                    std::unordered_map<TNode, Node>& evalAsNode) const;
+  /**
+   * Process unhandled, called when n cannot be evaluated. This updates
+   * evalAsNode and results with the proper entries for this case. The term
+   * nv is the (Node) value of n if it exists, otherwise if needsReconstruct
+   * is true, the value of n is reconstructed based on evalAsNode and results.
+   */
+  void processUnhandled(TNode n,
+                        TNode nv,
+                        std::unordered_map<TNode, Node>& evalAsNode,
+                        std::unordered_map<TNode, EvalResult>& results,
+                        bool needsReconstruct) const;
   /** The (optional) rewriter to be used */
   Rewriter* d_rr;
   /** The cardinality of the alphabet of strings */