From 28a6da4532c952a7077d233421aa498f5ca2ff59 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 18 Dec 2020 14:43:00 -0800
Subject: [PATCH] fix #4902

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/tactic/core/reduce_invertible_tactic.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/tactic/core/reduce_invertible_tactic.cpp b/src/tactic/core/reduce_invertible_tactic.cpp
index bfb5da408..65b0dc36f 100644
--- a/src/tactic/core/reduce_invertible_tactic.cpp
+++ b/src/tactic/core/reduce_invertible_tactic.cpp
@@ -339,7 +339,7 @@ private:
                 ++sh;
             }
             if (r.is_pos() && sh > 0) {
-                new_v = m_bv.mk_concat(m_bv.mk_extract(sz-1, sh, v), m_bv.mk_numeral(0, sh));
+                new_v = m_bv.mk_concat(m_bv.mk_extract(sz-sh-1, 0, v), m_bv.mk_numeral(0, sh));
             }
             if (mc && !r.is_zero()) {
                 ensure_mc(mc);