Fix Bitwuzla VARIABLE_NODE translation

cnheitman · Sep 29, 2023 · f805003 · f805003
1 parent 8a6ee2f
commit f805003
Showing 1 changed file with 14 additions and 2 deletions.
diff --git a/src/libtriton/ast/bitwuzla/tritonToBitwuzla.cpp b/src/libtriton/ast/bitwuzla/tritonToBitwuzla.cpp
@@ -289,8 +289,20 @@ namespace triton {
             return bitwuzla_mk_bv_value(sort->second, triton::utils::toString(value).c_str(), 10);
           }
 
-          auto n = bitwuzla_mk_const(sort->second, symVar->getName().c_str());
-          variables[n] = symVar;
+          auto n = (BitwuzlaTerm) 0;
+          /* If we already translated the node, return that. */
+          for (auto it = variables.begin(); it != variables.end(); ++it) {
+            if (it->second == symVar) {
+              n = it->first;
+              break;
+            }
+          }
+
+          if (n == 0) {
+            n = bitwuzla_mk_const(sort->second, symVar->getName().c_str());
+            variables[n] = symVar;
+          }
+
           return n;
         }