From f645ef7677cb126ca16400c65c0a60c93a1abdc5 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 2 Jun 2020 18:08:42 -0700
Subject: [PATCH] fix #4461

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

diff --git a/src/tactic/core/reduce_invertible_tactic.cpp b/src/tactic/core/reduce_invertible_tactic.cpp
index ea427145d..80b561d08 100644
--- a/src/tactic/core/reduce_invertible_tactic.cpp
+++ b/src/tactic/core/reduce_invertible_tactic.cpp
@@ -196,7 +196,6 @@ private:
         case OP_BSHL:
         case OP_BASHR:
         case OP_BLSHR:
-        case OP_BOR:
             model = rational::zero();
             return true;