From f805003cf51fce93f0fd35965bd99cc933b14b69 Mon Sep 17 00:00:00 2001 From: Christian Heitman Date: Thu, 17 Aug 2023 14:45:09 -0300 Subject: [PATCH] Fix Bitwuzla VARIABLE_NODE translation --- src/libtriton/ast/bitwuzla/tritonToBitwuzla.cpp | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) diff --git a/src/libtriton/ast/bitwuzla/tritonToBitwuzla.cpp b/src/libtriton/ast/bitwuzla/tritonToBitwuzla.cpp index 73081b189..096196475 100644 --- 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; }