From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Sun, 14 Jan 2018 06:12:27 +0000 (-0800)
Subject: Remove BITVECTOR_SUB from isInvertible(). (#1513)
X-Git-Tag: cvc5-1.0.0~5357
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a7dc71b4344cc0573997fcb4134ebf242f59bd7e;p=cvc5.git

Remove BITVECTOR_SUB from isInvertible(). (#1513)
---

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