From bb56443e71c3c29c7fe03696a7b915560365d371 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 8 Jan 2021 15:24:12 -0800
Subject: [PATCH] more #4932

---
 src/sat/tactic/goal2sat.cpp                  | 9 ++++++---
 src/tactic/core/reduce_invertible_tactic.cpp | 3 ---
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index bfcf7ff0f..47c28de16 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -1019,6 +1019,7 @@ void sat2goal::mc::flush_gmc() {
     sat::literal_vector clause;
     expr_ref_vector tail(m);
     expr_ref def(m);
+    auto is_literal = [&](expr* e) { expr* r; return is_uninterp_const(e) || (m.is_not(e, r) && is_uninterp_const(r)); };
     for (unsigned i = 0; i < updates.size(); ++i) {
         sat::literal l = updates[i];
         if (l == sat::null_literal) {
@@ -1032,8 +1033,7 @@ void sat2goal::mc::flush_gmc() {
                 def = m.mk_not(def);
             }
             expr_ref e = lit2expr(lit0);
-            expr* r = nullptr;
-            if (is_uninterp_const(e) || (m.is_not(e, r) && is_uninterp_const(r)))
+            if (is_literal(e))
                 m_gmc->add(e, def);
             clause.reset();
             tail.reset();
@@ -1050,7 +1050,10 @@ void sat2goal::mc::flush_gmc() {
                 l.neg(); 
                 r.neg(); 
             }
-            m_gmc->add(lit2expr(l), lit2expr(r));
+            
+            expr* a = lit2expr(l);
+            if (is_literal(a))
+                m_gmc->add(a, lit2expr(r));
             i += 5;
         }
         else {
diff --git a/src/tactic/core/reduce_invertible_tactic.cpp b/src/tactic/core/reduce_invertible_tactic.cpp
index 65b0dc36f..dbed42ff2 100644
--- a/src/tactic/core/reduce_invertible_tactic.cpp
+++ b/src/tactic/core/reduce_invertible_tactic.cpp
@@ -193,9 +193,6 @@ private:
         switch (f->get_decl_kind()) {
         case OP_BADD:
         case OP_BSUB:
-        case OP_BSHL:
-        case OP_BASHR:
-        case OP_BLSHR:
             model = rational::zero();
             return true;