From: yoni206 <yoni206@users.noreply.github.com>
Date: Wed, 20 Apr 2022 14:48:31 +0000 (+0300)
Subject: Remove redundant assertion in int-blaster (#8639)
X-Git-Tag: cvc5-1.0.1~242
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f68d074187bd78f11204ce0f4480c7116100af19;p=cvc5.git

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 c954bdbcf..246b70d8a 100644
--- 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 fbbf71595..9b560535c 100644
--- 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