From: yoni206 <yoni206@users.noreply.github.com>
Date: Fri, 16 Oct 2020 15:04:22 +0000 (-0700)
Subject: bv2int: caching introduced terms (#5283)
X-Git-Tag: cvc5-1.0.0~2704
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=eae5bf6a701037238b91476de9f8d26e34976779;p=cvc5.git

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 8906ddeea..dbe751415 100644
--- 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 428d35f8d..e8b85ac31 100644
--- 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
index 000000000..4d0da1dbb
--- /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)