From a7dc71b4344cc0573997fcb4134ebf242f59bd7e Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Sat, 13 Jan 2018 22:12:27 -0800
Subject: Remove BITVECTOR_SUB from isInvertible(). (#1513)

---
 src/theory/quantifiers/bv_inverter.cpp | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'src')

diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp
index a96f05a35..ec88f229e 100644
--- a/src/theory/quantifiers/bv_inverter.cpp
+++ b/src/theory/quantifiers/bv_inverter.cpp
@@ -78,8 +78,7 @@ Node BvInverter::getInversionNode(Node cond, TypeNode tn, BvInverterQuery* m)
       }
     }
   }
-  // TODO : compute the value if the condition is deterministic, e.g. calc
-  // multiplicative inverse of 2 constants
+  
   if (c.isNull())
   {
     NodeManager* nm = NodeManager::currentNM();
@@ -117,7 +116,6 @@ static bool isInvertible(Kind k, unsigned index)
       ||  k == BITVECTOR_CONCAT
       ||  k == BITVECTOR_SIGN_EXTEND
       ||  k == BITVECTOR_PLUS
-      ||  k == BITVECTOR_SUB
       ||  k == BITVECTOR_MULT
       ||  k == BITVECTOR_UREM_TOTAL
       ||  k == BITVECTOR_UDIV_TOTAL
-- 
cgit v1.2.3