Remove redundant assertion in int-blaster (#8639)

When translating nodes with no children, the default case does not change the original node, and so we do not need to assume anything about the node. fixes cvc5/cvc5-projects#416 . The example from the issue is added as a unit test.

diff --git a/src/theory/bv/int_blaster.cpp b/src/theory/bv/int_blaster.cpp
index c954bdbcf71276a91735711df492018c8d593d65..246b70d8a399bface6855948f9a241f7691b3958 100644 (file)
--- a/src/theory/bv/int_blaster.cpp
+++ b/src/theory/bv/int_blaster.cpp
@@ -666,7 +666,6 @@ Node IntBlaster::translateNoChildren(Node original,
 
   // The translation is done differently for variables (bound or free)  and
   // constants (values)
-  Assert(original.isVar() || original.isConst() || original.isNullaryOp());
   if (original.isVar())
   {
     if (original.getType().isBitVector())
@@ -719,7 +718,7 @@ Node IntBlaster::translateNoChildren(Node original,
   }
   else
   {
-    // original is a constant (value) or a nullary op (e.g., PI)
+    // original is a constant (value) or an operator with no arguments (e.g., PI)
     if (original.getKind() == kind::CONST_BITVECTOR)
     {
       // Bit-vector constants are transformed into their integer value.
@@ -730,7 +729,7 @@ Node IntBlaster::translateNoChildren(Node original,
     }
     else
     {
-      // Other constants or nullary ops stay the same.
+      // Other constants or operators stay the same.
       translation = original;
     }
   }

diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index fbbf715952ab7abef6544c4131e0fe071b5f93e9..9b560535c29dfe180e18761aaf221ec95ff0ecdf 100644 (file)
--- a/test/unit/api/cpp/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -27,6 +27,20 @@ class TestApiBlackSolver : public TestApi
 {
 };
 
+TEST_F(TestApiBlackSolver, proj_issue416)
+{
+  Solver slv;
+  slv.setOption("solve-bv-as-int", "sum");
+  slv.setOption("strings-exp", "true");
+  Sort s1 = slv.getStringSort();
+  Term t27 = slv.mkConst(s1, "_x50");
+  Term t333 = slv.mkRegexpAll();
+  Term t1243 = slv.mkTerm(Kind::STRING_REPLACE_RE_ALL, {t27, t333, t27});
+  Term t1291 = slv.mkTerm(Kind::EQUAL, {t1243, t27});
+  slv.assertFormula(t1291);
+  slv.checkSat();
+}
+
 TEST_F(TestApiBlackSolver, pow2Large1)
 {
   // Based on https://github.com/cvc5/cvc5-projects/issues/371