From 1378e713ba9cadfb1cc36fa5d114e2f038c4516a Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 13 Jul 2022 14:37:04 -0700
Subject: [PATCH] fix #6157

---
 src/smt/theory_bv.cpp | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp
index dba402a6e..196f49281 100644
--- a/src/smt/theory_bv.cpp
+++ b/src/smt/theory_bv.cpp
@@ -667,8 +667,9 @@ namespace smt {
         mk_enode(n);
         theory_var v = ctx.get_enode(n)->get_th_var(get_id()); 
         mk_bits(v);
-        mk_var(ctx.get_enode(n->get_arg(0)));
-
+        enode* k = ctx.get_enode(n->get_arg(0));
+        if (!is_attached_to_var(k))
+            mk_var(k);
         
         if (!ctx.relevancy()) 
             assert_int2bv_axiom(n);