From e10850e66a6122f34a6f2f9c342850ee798c786c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 5 Aug 2021 11:27:03 -0700
Subject: [PATCH] fix #5457

---
 src/tactic/core/reduce_invertible_tactic.cpp | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/tactic/core/reduce_invertible_tactic.cpp b/src/tactic/core/reduce_invertible_tactic.cpp
index 85062b03b..d8dc32809 100644
--- a/src/tactic/core/reduce_invertible_tactic.cpp
+++ b/src/tactic/core/reduce_invertible_tactic.cpp
@@ -327,7 +327,6 @@ private:
             // 
             unsigned sz = m_bv.get_bv_size(p);
             expr_ref bit1(m_bv.mk_numeral(1, 1), m);
-            new_v = m_bv.mk_numeral(0, sz);
 
             
             unsigned sh = 0;
@@ -335,9 +334,10 @@ private:
                 r /= rational(2);
                 ++sh;
             }
-            if (r.is_pos() && sh > 0) {
+            if (r.is_pos() && sh > 0) 
                 new_v = m_bv.mk_concat(m_bv.mk_extract(sz-sh-1, 0, v), m_bv.mk_numeral(0, sh));
-            }
+            else
+                new_v = v;
             if (mc && !r.is_zero()) {
                 ensure_mc(mc);
                 expr_ref def(m);