diff options
| -rw-r--r-- | src/theory/quantifiers/bv_inverter.cpp | 4 |
1 files changed, 1 insertions, 3 deletions
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 |