diff options
author | yoni206 <yoni206@users.noreply.github.com> | 2020-10-16 08:04:22 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-10-16 10:04:22 -0500 |
commit | eae5bf6a701037238b91476de9f8d26e34976779 (patch) | |
tree | 913fcf50efb33e68d46c48c99b62367b645aa69a /src/preprocessing | |
parent | 56f0e3c3455cc522bd18f41664591cae2c564be3 (diff) |
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.
Diffstat (limited to 'src/preprocessing')
-rw-r--r-- | src/preprocessing/passes/bv_to_int.cpp | 12 |
1 files changed, 7 insertions, 5 deletions
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(); } } |