bv2int: caching introduced terms (#5283)

The bv-to-int preprocessing pass has a cache that maps each BV node to its translated integer node.
In case the BV node is a function symbol, it's translated integer node is a fresh function symbol.
On current master, if we later process this fresh function symbol in the preprocessing pass, we again create a fresh function symbol as its translation. This is unsound, and was discovered in #5281, whose benchmark is added to regressions.
Closes #5281 if merged.

diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index 8906ddeeafc89ac7724bef0439016cfab871cdd7..dbe7514156b3352d7c645b14eb5df422a4d76b01 100644 (file)
--- a/src/preprocessing/passes/bv_to_int.cpp
+++ b/src/preprocessing/passes/bv_to_int.cpp
@@ -302,10 +302,10 @@ Node BVToInt::bvToInt(Node n)
       {
         // We are now visiting current on the way back up.
         // This is when we do the actual translation.
+        Node translation;
         if (currentNumChildren == 0)
         {
-          Node translation = translateNoChildren(current);
-          d_bvToIntCache[current] = translation;
+          translation = translateNoChildren(current);
         }
         else
         {
@@ -328,10 +328,12 @@ Node BVToInt::bvToInt(Node n)
           {
             translated_children.push_back(d_bvToIntCache[current[i]]);
           }
-          Node translation =
-              translateWithChildren(current, translated_children);
-          d_bvToIntCache[current] = translation;
+          translation = translateWithChildren(current, translated_children);
         }
+        // Map the current node to its translation in the cache.
+        d_bvToIntCache[current] = translation;
+        // Also map the translation to itself.
+        d_bvToIntCache[translation] = translation;
         toVisit.pop_back();
       }
     }

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 428d35f8d8281aefc3912b05b9f7a5388d35e94d..e8b85ac3121fd394d39abbacc4b96aae81cb2da7 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -224,6 +224,7 @@ set(regress_0_tests
   regress0/bv/bv_to_int_5230_shift_const.smt2
   regress0/bv/bv_to_int_5230_binary.smt2
   regress0/bv/bv_to_int_5230_missing_op.smt2
+  regress0/bv/bv_to_int_5281.smt2
   regress0/bv/bv_to_int_bvmul2.smt2
   regress0/bv/bv_to_int_bvuf_to_intuf.smt2
   regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2

diff --git a/test/regress/regress0/bv/bv_to_int_5281.smt2 b/test/regress/regress0/bv/bv_to_int_5281.smt2
new file mode 100644 (file)
index 0000000..4d0da1d
--- /dev/null
+++ b/test/regress/regress0/bv/bv_to_int_5281.smt2
@@ -0,0 +1,12 @@
+; COMMAND: --check-models --incremental
+; EXPECT: sat
+(set-logic ALL)
+(set-option :check-models true)
+(set-option :incremental true)
+(set-option :solve-bv-as-int sum)
+(declare-fun uf6 (Bool) Bool)
+(declare-fun uf7 (Bool) Bool)
+(assert (uf7 true))
+(push 1)
+(assert (uf6 (uf7 true)))
+(check-sat)