From 6c0a79057664cc4099c75eb8a135a8289a31390b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 2 Aug 2021 09:22:54 -0700
Subject: [PATCH] #5445

---
 src/sat/smt/bv_solver.cpp | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp
index 4df92596e..d030394a8 100644
--- a/src/sat/smt/bv_solver.cpp
+++ b/src/sat/smt/bv_solver.cpp
@@ -478,6 +478,9 @@ namespace bv {
             if (!assign_bit(bit2, v1, v2, idx, bit1, false))
                 break;
         }
+        if (s().value(m_bits[v1][m_wpos[v1]]) != l_undef)
+            find_wpos(v1);
+
         return num_assigned > 0;
     }