Handle rewrite to bool in BoundInference (#5311)

The BoundInference class did not properly handle rewrites that yield constant Booleans. This PR fixes this issue by explicitly checking for this case.

diff --git a/src/theory/arith/bound_inference.cpp b/src/theory/arith/bound_inference.cpp
index 7cae40bbb9dd1b594b806f42a0a3d4d211d26ff6..92e71bf14a431ffcbc7fd0975bfaab4080313cec 100644 (file)
--- a/src/theory/arith/bound_inference.cpp
+++ b/src/theory/arith/bound_inference.cpp
@@ -95,8 +95,13 @@ Bounds BoundInference::get(const Node& v) const
 const std::map<Node, Bounds>& BoundInference::get() const { return d_bounds; }
 bool BoundInference::add(const Node& n)
 {
+  Node tmp = Rewriter::rewrite(n);
+  if (tmp.getKind() == Kind::CONST_BOOLEAN)
+  {
+    return false;
+  }
   // Parse the node as a comparison
-  auto comp = Comparison::parseNormalForm(Rewriter::rewrite(n));
+  auto comp = Comparison::parseNormalForm(tmp);
   auto dec = comp.decompose(true);
   if (std::get<0>(dec).isVariable())
   {

diff --git a/src/theory/arith/nl/icp/icp_solver.cpp b/src/theory/arith/nl/icp/icp_solver.cpp
index 7f97d51b6e5d3d7f29e6729b0321fe94ae08f437..4ec33c3609bb942cf99c86e6c2369382776b1a37 100644 (file)
--- a/src/theory/arith/nl/icp/icp_solver.cpp
+++ b/src/theory/arith/nl/icp/icp_solver.cpp
@@ -77,8 +77,12 @@ std::vector<Node> ICPSolver::collectVariables(const Node& n) const
 
 std::vector<Candidate> ICPSolver::constructCandidates(const Node& n)
 {
-  auto comp =
-      Comparison::parseNormalForm(Rewriter::rewrite(n)).decompose(false);
+  Node tmp = Rewriter::rewrite(n);
+  if (tmp.isConst())
+  {
+    return {};
+  }
+  auto comp = Comparison::parseNormalForm(tmp).decompose(false);
   Kind k = std::get<1>(comp);
   if (k == Kind::DISTINCT)
   {