From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Fri, 8 Dec 2017 22:32:16 +0000 (-0800)
Subject: Fixed side conditions for CBQI BV, added unit tests. (#1434)
X-Git-Tag: cvc5-1.0.0~5420
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=707571c8b4a572b9554f9068df796f1257cb587d;p=cvc5.git

Fixed side conditions for CBQI BV, added unit tests. (#1434)

This fixes the side conditions for BITVECTOR_UREM_TOTAL, BITVECTOR_UDIV_TOTAL,
BITVECTOR_LSHR, BITVECTOR_ASHR, BITVECTOR_SHL.

It refactors side condition generation for better readability and unit testing.
It further adds unit tests for all side conditions we generate in order to check if they too weak
or to restrictive (which may result in unsound behavior).

This is achieved by checking the following two implications:
not (exists x. s * x = t => SC) ... if sat, SC is too restrictive
not (SC => exists x. s * x = t) ... if sat SC is too weak

This simplifies to checking not (SC <=> exists x. s * x = t).
---

diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp
index aa3180604..089989e19 100644
--- a/src/theory/bv/theory_bv_utils.cpp
+++ b/src/theory/bv/theory_bv_utils.cpp
@@ -26,7 +26,20 @@ namespace theory {
 namespace bv {
 namespace utils {
 
-Node mkUmulo(TNode t1, TNode t2) {
+Node mkInc(TNode t)
+{
+  return NodeManager::currentNM()->mkNode(
+      kind::BITVECTOR_PLUS, t, bv::utils::mkOne(bv::utils::getSize(t)));
+}
+
+Node mkDec(TNode t)
+{
+  return NodeManager::currentNM()->mkNode(
+      kind::BITVECTOR_SUB, t, bv::utils::mkOne(bv::utils::getSize(t)));
+}
+
+Node mkUmulo(TNode t1, TNode t2)
+{
   unsigned w = getSize(t1);
   if (w == 1) return mkFalse();
 
@@ -35,9 +48,11 @@ Node mkUmulo(TNode t1, TNode t2) {
   std::vector<Node> tmp;
 
   uppc = mkExtract(t1, w - 1, w - 1);
-  for (size_t i = 1; i < w; ++i) {
+  for (size_t i = 1; i < w; ++i)
+  {
     tmp.push_back(nm->mkNode(kind::BITVECTOR_AND, mkExtract(t2, i, i), uppc));
-    uppc = nm->mkNode(kind::BITVECTOR_OR, mkExtract(t1, w-1-i, w-1-i), uppc);
+    uppc = nm->mkNode(
+        kind::BITVECTOR_OR, mkExtract(t1, w - 1 - i, w - 1 - i), uppc);
   }
   Node zext_t1 = mkConcat(mkZero(1), t1);
   Node zext_t2 = mkConcat(mkZero(1), t2);
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 6be0af4a0..fca0a3a47 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -208,6 +208,12 @@ inline Node mkZero(unsigned size) { return mkConst(size, 0u); }
 
 inline Node mkOne(unsigned size) { return mkConst(size, 1u); }
 
+/* Increment */
+Node mkInc(TNode t);
+
+/* Decrement */
+Node mkDec(TNode t);
+
 /* Unsigned multiplication overflow detection.
  * See M.Gok, M.J. Schulte, P.I. Balzola, "Efficient integer multiplication
  * overflow detection circuits", 2001.
diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp
index b5d36eae4..bad26d14f 100644
--- a/src/theory/quantifiers/bv_inverter.cpp
+++ b/src/theory/quantifiers/bv_inverter.cpp
@@ -29,23 +29,7 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-/* Drop child at given index from expression.
- * E.g., dropChild((x + y + z), 1) -> (x + z)  */
-static Node dropChild(Node n, unsigned index)
-{
-  unsigned nchildren = n.getNumChildren();
-  Assert(index < nchildren);
-  Kind k = n.getKind();
-  Assert(k == BITVECTOR_AND || k == BITVECTOR_OR || k == BITVECTOR_MULT
-         || k == BITVECTOR_PLUS);
-  NodeBuilder<> nb(NodeManager::currentNM(), k);
-  for (unsigned i = 0; i < nchildren; ++i)
-  {
-    if (i == index) continue;
-    nb << n[i];
-  }
-  return nb.constructNode();
-}
+/*---------------------------------------------------------------------------*/
 
 Node BvInverter::getSolveVariable(TypeNode tn)
 {
@@ -62,6 +46,8 @@ Node BvInverter::getSolveVariable(TypeNode tn)
   }
 }
 
+/*---------------------------------------------------------------------------*/
+
 Node BvInverter::getInversionNode(Node cond, TypeNode tn, BvInverterQuery* m)
 {
   // condition should be rewritten
@@ -108,7 +94,9 @@ Node BvInverter::getInversionNode(Node cond, TypeNode tn, BvInverterQuery* m)
   return c;
 }
 
-bool BvInverter::isInvertible(Kind k, unsigned index)
+/*---------------------------------------------------------------------------*/
+
+static bool isInvertible(Kind k, unsigned index)
 {
   return  k == NOT
       ||  k == EQUAL
@@ -196,11 +184,412 @@ Node BvInverter::getPathToPv(
   return slit;
 }
 
-Node BvInverter::solve_bv_lit(Node sv,
-                              Node lit,
-                              std::vector<unsigned>& path,
-                              BvInverterQuery* m,
-                              BvInverterStatus& status)
+/*---------------------------------------------------------------------------*/
+
+/* Drop child at given index from expression.
+ * E.g., dropChild((x + y + z), 1) -> (x + z)  */
+static Node dropChild(Node n, unsigned index)
+{
+  unsigned nchildren = n.getNumChildren();
+  Assert(index < nchildren);
+  Kind k = n.getKind();
+  Assert(k == BITVECTOR_AND || k == BITVECTOR_OR || k == BITVECTOR_MULT
+         || k == BITVECTOR_PLUS);
+  NodeBuilder<> nb(NodeManager::currentNM(), k);
+  for (unsigned i = 0; i < nchildren; ++i)
+  {
+    if (i == index) continue;
+    nb << n[i];
+  }
+  return nb.constructNode();
+}
+
+static Node getScBvUlt(bool pol, Kind k, unsigned idx, Node x, Node t)
+{
+  Assert(k == BITVECTOR_ULT);
+
+  NodeManager* nm = NodeManager::currentNM();
+  unsigned w = bv::utils::getSize(t);
+  Node sc;
+
+  if (idx == 0)
+  {
+    if (pol == true)
+    {
+      /* x < t
+       * with side condition:
+       * t != 0  */
+      Node scl = nm->mkNode(DISTINCT, t, bv::utils::mkZero(w));
+      Node scr = nm->mkNode(k, x, t);
+      sc = nm->mkNode(IMPLIES, scl, scr);
+    }
+    else
+    {
+      sc = nm->mkNode(NOT, nm->mkNode(k, x, t));
+    }
+  }
+  else if (idx == 1)
+  {
+    if (pol == true)
+    {
+      /* t < x
+       * with side condition:
+       * t != ~0  */
+      Node scl = nm->mkNode(DISTINCT, t, bv::utils::mkOnes(w));
+      Node scr = nm->mkNode(k, t, x);
+      sc = nm->mkNode(IMPLIES, scl, scr);
+    }
+    else
+    {
+      sc = nm->mkNode(NOT, nm->mkNode(k, t, x));
+    }
+  }
+  Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc << std::endl;
+  return sc;
+}
+
+static Node getScBvSlt(bool pol, Kind k, unsigned idx, Node x, Node t)
+{
+  Assert(k == BITVECTOR_SLT);
+
+  NodeManager* nm = NodeManager::currentNM();
+  unsigned w = bv::utils::getSize(t);
+  Node sc;
+
+  if (idx == 0)
+  {
+    if (pol == true)
+    {
+      /* x < t
+       * with side condition:
+       * t != 10...0 */
+      Node min = bv::utils::mkConst(BitVector(w).setBit(w - 1));
+      Node scl = nm->mkNode(DISTINCT, min, t);
+      Node scr = nm->mkNode(k, x, t);
+      sc = nm->mkNode(IMPLIES, scl, scr);
+    }
+    else
+    {
+      sc = nm->mkNode(NOT, nm->mkNode(k, x, t));
+    }
+  }
+  else if (idx == 1)
+  {
+    if (pol == true)
+    {
+      /* t < x
+       * with side condition:
+       * t != 01...1  */
+      BitVector bv = BitVector(w).setBit(w - 1);
+      Node max = bv::utils::mkConst(~bv);
+      Node scl = nm->mkNode(DISTINCT, t, max);
+      Node scr = nm->mkNode(k, t, x);
+      sc = nm->mkNode(IMPLIES, scl, scr);
+    }
+    else
+    {
+      sc = nm->mkNode(NOT, nm->mkNode(k, t, x));
+    }
+  }
+  Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc << std::endl;
+  return sc;
+}
+
+static Node getScBvEq(bool pol, Kind k, unsigned idx, Node x, Node t)
+{
+  Assert(k == EQUAL);
+  Assert(pol == false);
+
+  NodeManager* nm = NodeManager::currentNM();
+  unsigned w = bv::utils::getSize(t);
+
+  /* x != t
+   * <->
+   * x < t || x > t  (ULT)
+   * with side condition:
+   * t != 0 || t != ~0  */
+  Node scl = nm->mkNode(OR,
+      nm->mkNode(DISTINCT, t, bv::utils::mkZero(w)),
+      nm->mkNode(DISTINCT, t, bv::utils::mkOnes(w)));
+  Node scr = nm->mkNode(DISTINCT, x, t);
+  Node sc = nm->mkNode(IMPLIES, scl, scr);
+  Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc << std::endl;
+  return sc;
+}
+
+static Node getScBvMult(Kind k, unsigned idx, Node x, Node s, Node t)
+{
+  Assert(k == BITVECTOR_MULT);
+
+  NodeManager* nm = NodeManager::currentNM();
+
+  /* x * s = t
+   * with side condition:
+   * ctz(t) >= ctz(s) <-> x * s = t
+   * where
+   * ctz(t) >= ctz(s) -> t = 0 \/ ((t & -t) >= (s & -s) /\ s != 0) */
+  Node zero = bv::utils::mkZero(bv::utils::getSize(s));
+  Node t_uge_s = nm->mkNode(BITVECTOR_UGE,
+      nm->mkNode(BITVECTOR_AND, t, nm->mkNode(BITVECTOR_NEG, t)),
+      nm->mkNode(BITVECTOR_AND, s, nm->mkNode(BITVECTOR_NEG, s)));
+  Node scl = nm->mkNode(OR,
+      t.eqNode(zero),
+      nm->mkNode(AND, t_uge_s, s.eqNode(zero).notNode()));
+  Node scr = nm->mkNode(EQUAL, nm->mkNode(k, x, s), t);
+  Node sc = nm->mkNode(IMPLIES, scl, scr);
+  Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc << std::endl;
+  return sc;
+}
+
+static Node getScBvUrem(Kind k, unsigned idx, Node x, Node s, Node t)
+{
+  Assert(k == BITVECTOR_UREM_TOTAL);
+  Assert(idx == 1);
+
+  NodeManager* nm = NodeManager::currentNM();
+
+  /* s % x = t
+   * with side condition:
+   * s = t
+   * ||
+   * ( s > t
+   *   && s-t > t
+   *   && (t = 0 || t != s-1) )  */
+
+  Node a1 =  // s > t
+    nm->mkNode(BITVECTOR_UGT, s, t);
+  Node a2 =  // s-t > t
+    nm->mkNode(BITVECTOR_UGT, nm->mkNode(BITVECTOR_SUB, s, t), t);
+  Node a3 =  // (t = 0 || t != s-1)
+    nm->mkNode(OR,
+        t.eqNode(bv::utils::mkZero(bv::utils::getSize(t))),
+        t.eqNode(bv::utils::mkDec(s)).notNode());
+
+  Node scl = nm->mkNode(OR,
+        t.eqNode(s),
+        nm->mkNode(AND, a1, nm->mkNode(AND, a2, a3)));
+  Node scr = nm->mkNode(EQUAL, nm->mkNode(k, s, x), t);
+  Node sc = nm->mkNode(IMPLIES, scl, scr);
+
+  Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc << std::endl;
+  return sc;
+}
+
+static Node getScBvUdiv(Kind k, unsigned idx, Node x, Node s, Node t)
+{
+  Assert(k == BITVECTOR_UDIV_TOTAL);
+
+  NodeManager* nm = NodeManager::currentNM();
+  unsigned w = bv::utils::getSize(s);
+  Assert (w == bv::utils::getSize(t));
+  Node scl, scr;
+  Node zero = bv::utils::mkZero(w);
+
+  if (idx == 0)
+  {
+    /* x udiv s = t
+     * with side condition:
+     * t = ~0 && (s = 0 || s = 1)
+     * ||
+     * (t != ~0 && s != 0 && !umulo(s * t)) */
+    Node o1 = nm->mkNode(AND,
+        t.eqNode(bv::utils::mkOnes(w)),
+        nm->mkNode(OR,
+          s.eqNode(bv::utils::mkZero(w)),
+          s.eqNode(bv::utils::mkOne(w))));
+    Node o2 = nm->mkNode(AND,
+        t.eqNode(bv::utils::mkOnes(w)).notNode(),
+        s.eqNode(bv::utils::mkZero(w)).notNode(),
+        nm->mkNode(NOT, bv::utils::mkUmulo(s, t)));
+
+    scl = nm->mkNode(OR, o1, o2);
+    scr = nm->mkNode(EQUAL, nm->mkNode(k, x, s), t);
+  }
+  else
+  {
+    /* s udiv x = t
+     * with side condition:
+     * s = t
+     * ||
+     * t = ~0
+     * ||
+     * (s >= t
+     *  && (s % t = 0 || (s / (t+1) +1) <= s / t)
+     *  && (s = ~0 => t != 0))  */
+
+    Node oo1 = nm->mkNode(EQUAL,
+        nm->mkNode(BITVECTOR_UREM_TOTAL, s, t),
+        bv::utils::mkZero(w));
+
+    Node ule1 = nm->mkNode(BITVECTOR_PLUS,
+        bv::utils::mkOne(w),
+        nm->mkNode(BITVECTOR_UDIV_TOTAL,
+          s, nm->mkNode(BITVECTOR_PLUS, t, bv::utils::mkOne(w))));
+    Node ule2 = nm->mkNode(BITVECTOR_UDIV_TOTAL, s, t);
+    Node oo2 = nm->mkNode(BITVECTOR_ULE, ule1, ule2);
+
+    Node a1 = nm->mkNode(BITVECTOR_UGE, s, t);
+    Node a2 = nm->mkNode(OR, oo1, oo2);
+    Node a3 = nm->mkNode(IMPLIES,
+        s.eqNode(bv::utils::mkOnes(w)),
+        t.eqNode(bv::utils::mkZero(w)).notNode());
+
+    Node o1 = s.eqNode(t);
+    Node o2 = t.eqNode(bv::utils::mkOnes(w));
+    Node o3 = nm->mkNode(AND, a1, a2, a3);
+
+    scl = nm->mkNode(OR, o1, o2, o3);
+    scr = nm->mkNode(EQUAL, nm->mkNode(k, s, x), t);
+  }
+
+  Node sc = nm->mkNode(IMPLIES, scl, scr);
+  Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc << std::endl;
+  return sc;
+}
+
+static Node getScBvAndOr(Kind k, unsigned idx, Node x, Node s, Node t)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  /* with side condition:
+   * t & s = t
+   * t | s = t */
+  Node scl = nm->mkNode(EQUAL, t, nm->mkNode(k, t, s));
+  Node scr = nm->mkNode(EQUAL, nm->mkNode(k, x, s), t);
+  Node sc = nm->mkNode(IMPLIES, scl, scr);
+  Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc << std::endl;
+  return sc;
+}
+
+static Node getScBvLshr(Kind k, unsigned idx, Node x, Node s, Node t)
+{
+  Assert(k == BITVECTOR_LSHR);
+  Assert(idx == 0);
+
+  NodeManager* nm = NodeManager::currentNM();
+  unsigned w = bv::utils::getSize(s);
+  Assert(w == bv::utils::getSize(t));
+  
+  /* x >> s = t
+   * with side condition:
+   * s = 0 || (s < w && clz(t) >=s) || (s >= w && t = 0)
+   * ->
+   * s = 0 || (s < w && ((z o t) << (z o s))[2w-1 : w] = z) || (s >= w && t = 0)
+   * with w = getSize(t) = getSize(s)
+   * and z = 0 with getSize(z) = w  */
+
+  Node z = bv::utils::mkZero(w);
+  Node ww = bv::utils::mkConst(w, w);
+
+  Node z_o_t = nm->mkNode(BITVECTOR_CONCAT, z, t);
+  Node z_o_s = nm->mkNode(BITVECTOR_CONCAT, z, s);
+  Node shl = nm->mkNode(BITVECTOR_SHL, z_o_t, z_o_s);
+  Node ext = bv::utils::mkExtract(shl, 2*w-1, w);
+
+  Node o1 = s.eqNode(z);
+  Node o2 = nm->mkNode(AND, nm->mkNode(BITVECTOR_ULT, s, ww), ext.eqNode(z));
+  Node o3 = nm->mkNode(AND, nm->mkNode(BITVECTOR_UGE, s, ww), t.eqNode(z));
+
+  Node scl = nm->mkNode(OR, o1, o2, o3);
+  Node scr = nm->mkNode(EQUAL, nm->mkNode(k, x, s), t);
+  Node sc = nm->mkNode(IMPLIES, scl, scr);
+  Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc << std::endl;
+  return sc;
+}
+
+static Node getScBvAshr(Kind k, unsigned idx, Node x, Node s, Node t)
+{
+  Assert(k == BITVECTOR_ASHR);
+  Assert(idx == 0);
+
+  NodeManager* nm = NodeManager::currentNM();
+  unsigned w = bv::utils::getSize(s);
+  Assert(w == bv::utils::getSize(t));
+  
+  /* x >> s = t
+   * with side condition:
+   * s = 0
+   * ||
+   * (s < w && (((z o t) << (z o s))[2w-1:w-1] = z
+   *            ||
+   *            ((~z o t) << (z o s))[2w-1:w-1] = ~z))
+   * ||
+   * (s >= w && (t = 0 || t = ~0))
+   * with w = getSize(t) = getSize(s)
+   * and z = 0 with getSize(z) = w  */
+  
+  Node z = bv::utils::mkZero(w);
+  Node zz = bv::utils::mkZero(w+1);
+  Node n = bv::utils::mkOnes(w);
+  Node nn = bv::utils::mkOnes(w+1);
+  Node ww = bv::utils::mkConst(w, w);
+
+  Node z_o_t = bv::utils::mkConcat(z, t);
+  Node z_o_s = bv::utils::mkConcat(z, s);
+  Node n_o_t = bv::utils::mkConcat(n, t);
+
+  Node shlz = nm->mkNode(BITVECTOR_SHL, z_o_t, z_o_s);
+  Node shln = nm->mkNode(BITVECTOR_SHL, n_o_t, z_o_s);
+  Node extz = bv::utils::mkExtract(shlz, 2*w-1, w-1);
+  Node extn = bv::utils::mkExtract(shln, 2*w-1, w-1);
+
+  Node o1 = s.eqNode(z);
+  Node o2 = nm->mkNode(AND,
+      nm->mkNode(BITVECTOR_ULT, s, ww),
+      nm->mkNode(OR, extz.eqNode(zz), extn.eqNode(nn)));
+  Node o3 = nm->mkNode(AND,
+      nm->mkNode(BITVECTOR_UGE, s, ww),
+      nm->mkNode(OR, t.eqNode(z), t.eqNode(n)));
+
+  Node scl = nm->mkNode(OR, o1, o2, o3);
+  Node scr = nm->mkNode(EQUAL, nm->mkNode(k, x, s), t);
+  Node sc = nm->mkNode(IMPLIES, scl, scr);
+  Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc << std::endl;
+  return sc;
+}
+
+static Node getScBvShl(Kind k, unsigned idx, Node x, Node s, Node t)
+{
+  Assert(k == BITVECTOR_SHL);
+  Assert(idx == 0);
+
+  NodeManager* nm = NodeManager::currentNM();
+  unsigned w = bv::utils::getSize(s);
+  Assert(w == bv::utils::getSize(t));
+
+  /* x << s = t
+   * with side condition:
+   * (s = 0 || ctz(t) >= s)
+   * <->
+   * (s = 0 || (s < w && ((t o z) >> (z o s))[w-1:0] = z) || (s >= w && t = 0)
+   *
+   * where
+   * w = getSize(s) = getSize(t) = getSize (z) && z = 0
+   */
+
+  Node z = bv::utils::mkConst(w, 0u);
+  Node ww = bv::utils::mkConst(w, w);
+
+  Node shr = nm->mkNode(BITVECTOR_LSHR,
+      bv::utils::mkConcat(t, z),
+      bv::utils::mkConcat(z, s));
+  Node ext = bv::utils::mkExtract(shr, w - 1, 0);
+
+  Node o1 = nm->mkNode(EQUAL, s, z);
+  Node o2 = nm->mkNode(AND, nm->mkNode(BITVECTOR_ULT, s, ww), ext.eqNode(z));
+  Node o3 = nm->mkNode(AND, nm->mkNode(BITVECTOR_UGE, s, ww), t.eqNode(z));
+
+  Node scl = nm->mkNode(OR, o1, o2, o3);
+  Node scr = nm->mkNode(EQUAL, nm->mkNode(k, x, s), t);
+  Node sc = nm->mkNode(IMPLIES, scl, scr);
+  Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc << std::endl;
+  return sc;
+}
+
+Node BvInverter::solveBvLit(Node sv,
+                            Node lit,
+                            std::vector<unsigned>& path,
+                            BvInverterQuery* m,
+                            BvInverterStatus& status)
 {
   Assert(!path.empty());
 
@@ -245,48 +634,9 @@ Node BvInverter::solve_bv_lit(Node sv,
     case BITVECTOR_ULT:
     {
       TypeNode solve_tn = sv_t.getType();
-      Node x = getSolveVariable(solve_tn);
-      Node sc;
-      if (index == 0)
-      {
-        if (pol == true)
-        {
-          /* x < t
-           * with side condition:
-           * t != 0  */
-          Node scl = nm->mkNode(
-              DISTINCT, t, bv::utils::mkZero(bv::utils::getSize(t)));
-          Node scr = nm->mkNode(k, x, t);
-          sc = nm->mkNode(IMPLIES, scl, scr);
-        }
-        else
-        {
-          sc = nm->mkNode(NOT, nm->mkNode(k, x, t));
-        }
-      }
-      else if (index == 1)
-      {
-        if (pol == true)
-        {
-          /* t < x
-           * with side condition:
-           * t != ~0  */
-          Node scl = nm->mkNode(
-              DISTINCT, t, bv::utils::mkOnes(bv::utils::getSize(t)));
-          Node scr = nm->mkNode(k, t, x);
-          sc = nm->mkNode(IMPLIES, scl, scr);
-        }
-        else
-        {
-          sc = nm->mkNode(NOT, nm->mkNode(k, t, x));
-        }
-      }
-      Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc
-                         << std::endl;
-      status.d_conds.push_back(sc);
-      /* t = skv (fresh skolem constant)  */
-      Node skv = getInversionNode(sc, solve_tn, m);
-      t = skv;
+      Node sc = getScBvUlt(pol, k, index, getSolveVariable(solve_tn), t);
+      /* t = fresh skolem constant  */
+      t = getInversionNode(sc, solve_tn, m);
       if (!path.empty())
       {
         index = path.back();
@@ -301,50 +651,9 @@ Node BvInverter::solve_bv_lit(Node sv,
     case BITVECTOR_SLT:
     {
       TypeNode solve_tn = sv_t.getType();
-      Node x = getSolveVariable(solve_tn);
-      Node sc;
-      unsigned w = bv::utils::getSize(t);
-      if (index == 0)
-      {
-        if (pol == true)
-        {
-          /* x < t
-           * with side condition:
-           * t != 10...0 */
-          Node min = bv::utils::mkConst(BitVector(w).setBit(w - 1));
-          Node scl = nm->mkNode(DISTINCT, min, t);
-          Node scr = nm->mkNode(k, x, t);
-          sc = nm->mkNode(IMPLIES, scl, scr);
-        }
-        else
-        {
-          sc = nm->mkNode(NOT, nm->mkNode(k, x, t));
-        }
-      }
-      else if (index == 1)
-      {
-        if (pol == true)
-        {
-          /* t < x
-           * with side condition:
-           * t != 01...1  */
-          BitVector bv = BitVector(w).setBit(w - 1);
-          Node max = bv::utils::mkConst(~bv);
-          Node scl = nm->mkNode(DISTINCT, t, max);
-          Node scr = nm->mkNode(k, t, x);
-          sc = nm->mkNode(IMPLIES, scl, scr);
-        }
-        else
-        {
-          sc = nm->mkNode(NOT, nm->mkNode(k, t, x));
-        }
-      }
-      Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc
-                         << std::endl;
-      status.d_conds.push_back(sc);
-      /* t = skv (fresh skolem constant)  */
-      Node skv = getInversionNode(sc, solve_tn, m);
-      t = skv;
+      Node sc = getScBvSlt(pol, k, index, getSolveVariable(solve_tn), t);
+      /* t = fresh skolem constant  */
+      t = getInversionNode(sc, solve_tn, m);
       if (!path.empty())
       {
         index = path.back();
@@ -360,26 +669,10 @@ Node BvInverter::solve_bv_lit(Node sv,
       Assert(k == EQUAL);
       if (pol == false)
       {
-        /* x != t
-         * <->
-         * x < t || x > t  (ULT)
-         * with side condition:
-         * t != 0 || t != ~0  */
         TypeNode solve_tn = sv_t.getType();
-        Node x = getSolveVariable(solve_tn);
-        unsigned w = bv::utils::getSize(t);
-        Node scl = nm->mkNode(
-            OR,
-            nm->mkNode(DISTINCT, t, bv::utils::mkZero(w)),
-            nm->mkNode(DISTINCT, t, bv::utils::mkOnes(w)));
-        Node scr = nm->mkNode(DISTINCT, x, t);
-        Node sc = nm->mkNode(IMPLIES, scl, scr);
-        Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc
-                           << std::endl;
-        status.d_conds.push_back(sc);
-        /* t = skv (fresh skolem constant)  */
-        Node skv = getInversionNode(sc, solve_tn, m);
-        t = skv;
+        Node sc = getScBvEq(pol, k, index, getSolveVariable(solve_tn), t);
+        /* t = fresh skolem constant  */
+        t = getInversionNode(sc, solve_tn, m);
         if (!path.empty())
         {
           index = path.back();
@@ -455,45 +748,15 @@ Node BvInverter::solve_bv_lit(Node sv,
 
         case BITVECTOR_MULT:
         {
-          /* with side condition:
-           * ctz(t) >= ctz(s) <-> x * s = t
-           * where
-           * ctz(t) >= ctz(s) -> t = 0 \/ ((t & -t) >= (s & -s) /\ s != 0) */
           TypeNode solve_tn = sv_t[index].getType();
-          Node x = getSolveVariable(solve_tn);
-          Node zero = bv::utils::mkZero(bv::utils::getSize(s));
-          /* left hand side of side condition  */
-          Node t_uge_s = nm->mkNode(
-                   BITVECTOR_UGE,
-                   nm->mkNode(BITVECTOR_AND, t, nm->mkNode(BITVECTOR_NEG, t)),
-                   nm->mkNode(BITVECTOR_AND, s, nm->mkNode(BITVECTOR_NEG, s)));
-          Node scl =
-              nm->mkNode(OR,
-                         t.eqNode(zero),
-                         nm->mkNode(AND, t_uge_s, s.eqNode(zero).notNode()));
-          /* right hand side of side condition  */
-          Node scr = nm->mkNode(EQUAL, nm->mkNode(BITVECTOR_MULT, x, s), t);
-          /* overall side condition  */
-          Node sc = nm->mkNode(IMPLIES, scl, scr);
-          Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc
-                             << std::endl;
-          /* add side condition  */
-          status.d_conds.push_back(sc);
-
-          /* t = skv (fresh skolem constant)
-           * get the skolem node for this side condition  */
-          Node skv = getInversionNode(sc, solve_tn, m);
-          /* now solving with the skolem node as the RHS  */
-          t = skv;
+          Node sc = getScBvMult(k, index, getSolveVariable(solve_tn), s, t);
+          /* t = fresh skolem constant */
+          t = getInversionNode(sc, solve_tn, m);
           break;
         }
 
         case BITVECTOR_UREM_TOTAL:
         {
-          /* t = skv (fresh skolem constant)  */
-          TypeNode solve_tn = sv_t[index].getType();
-          Node x = getSolveVariable(solve_tn);
-          Node scl, scr;
           if (index == 0)
           {
             /* x % s = t is rewritten to x - x / y * y */
@@ -501,90 +764,19 @@ Node BvInverter::solve_bv_lit(Node sv,
                                << ", from " << sv_t << std::endl;
             return Node::null();
           }
-          else
-          {
-            /* s % x = t
-             * with side condition:
-             * s > t
-             * && s-t > t
-             * && (t = 0 || t != s-1)  */
-            Node s_gt_t = nm->mkNode(BITVECTOR_UGT, s, t);
-            Node s_m_t = nm->mkNode(BITVECTOR_SUB, s, t);
-            Node smt_gt_t = nm->mkNode(BITVECTOR_UGT, s_m_t, t);
-            Node t_eq_z = nm->mkNode(EQUAL,
-                t, bv::utils::mkZero(bv::utils::getSize(t)));
-            Node s_m_o = nm->mkNode(BITVECTOR_SUB,
-                s, bv::utils::mkOne(bv::utils::getSize(s)));
-            Node t_d_smo = nm->mkNode(DISTINCT, t, s_m_o);
-
-            scl = nm->mkNode(AND,
-                             nm->mkNode(AND, s_gt_t, smt_gt_t),
-                             nm->mkNode(OR, t_eq_z, t_d_smo));
-            scr = nm->mkNode(EQUAL, nm->mkNode(BITVECTOR_UREM_TOTAL, s, x), t);
-          }
-          Node sc = nm->mkNode(IMPLIES, scl, scr);
-          Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc
-                             << std::endl;
-          status.d_conds.push_back(sc);
-          Node skv = getInversionNode(sc, solve_tn, m);
-          t = skv;
+          TypeNode solve_tn = sv_t[index].getType();
+          Node sc = getScBvUrem(k, index, getSolveVariable(solve_tn), s, t);
+          /* t = skv (fresh skolem constant)  */
+          t = getInversionNode(sc, solve_tn, m);
           break;
         }
 
         case BITVECTOR_UDIV_TOTAL:
         {
           TypeNode solve_tn = sv_t[index].getType();
-          Node x = getSolveVariable(solve_tn);
-          Node s = sv_t[1 - index];
-          unsigned w = bv::utils::getSize(s);
-          Node scl, scr;
-          Node zero = bv::utils::mkZero(w);
-
-          if (index == 0)
-          {
-            /* x udiv s = t
-             * with side condition:
-             * !umulo(s * t)
-             */
-            scl = nm->mkNode(NOT, bv::utils::mkUmulo(s, t));
-            scr = nm->mkNode(EQUAL, nm->mkNode(BITVECTOR_UDIV_TOTAL, x, s), t);
-          }
-          else
-          {
-            /* s udiv x = t
-             * with side condition:
-             * (t = 0 && (s = 0 || s != 2^w-1))
-             * || s >= t
-             * || t = 2^w-1
-             */
-            Node ones = bv::utils::mkOnes(w);
-            Node t_eq_zero = nm->mkNode(EQUAL, t, zero);
-            Node s_eq_zero = nm->mkNode(EQUAL, s, zero);
-            Node s_ne_ones = nm->mkNode(DISTINCT, s, ones);
-            Node s_ge_t = nm->mkNode(BITVECTOR_UGE, s, t);
-            Node t_eq_ones = nm->mkNode(EQUAL, t, ones);
-            scl = nm->mkNode(
-                OR,
-                nm->mkNode(
-                  AND, t_eq_zero, nm->mkNode(OR, s_eq_zero, s_ne_ones)),
-                s_ge_t,
-                t_eq_ones);
-            scr = nm->mkNode(EQUAL, nm->mkNode(BITVECTOR_UDIV_TOTAL, s, x), t);
-          }
-
-          /* overall side condition */
-          Node sc = nm->mkNode(IMPLIES, scl, scr);
-          Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc
-                             << std::endl;
-          status.d_conds.push_back(sc);
-          /* add side condition */
-          status.d_conds.push_back(sc);
-
-          /* t = skv (fresh skolem constant)
-           * get the skolem node for this side condition */
-          Node skv = getInversionNode(sc, solve_tn, m);
-          /* now solving with the skolem node as the RHS */
-          t = skv;
+          Node sc = getScBvUdiv(k, index, getSolveVariable(solve_tn), s, t);
+          /* t = fresh skolem constant */
+          t = getInversionNode(sc, solve_tn, m);
           break;
         }
 
@@ -595,16 +787,9 @@ Node BvInverter::solve_bv_lit(Node sv,
            * t & s = t
            * t | s = t */
           TypeNode solve_tn = sv_t[index].getType();
-          Node x = getSolveVariable(solve_tn);
-          Node scl = nm->mkNode(EQUAL, t, nm->mkNode(k, t, s));
-          Node scr = nm->mkNode(EQUAL, nm->mkNode(k, x, s), t);
-          Node sc = nm->mkNode(IMPLIES, scl, scr);
-          Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc
-                             << std::endl;
-          status.d_conds.push_back(sc);
-          /* t = skv (fresh skolem constant)  */
-          Node skv = getInversionNode(sc, solve_tn, m);
-          t = skv;
+          Node sc = getScBvAndOr(k, index, getSolveVariable(solve_tn), s, t);
+          /* t = fresh skolem constant  */
+          t = getInversionNode(sc, solve_tn, m);
           break;
         }
 
@@ -614,37 +799,7 @@ Node BvInverter::solve_bv_lit(Node sv,
 
         case BITVECTOR_LSHR:
         {
-          TypeNode solve_tn = sv_t[index].getType();
-          Node x = getSolveVariable(solve_tn);
-          Node scl, scr;
-          if (index == 0)
-          {
-            /* x >> s = t
-             * with side condition:
-             * s = 0 || clz(t) >= s
-             * ->
-             * s = 0 || ((z o t) << s)[2w-1 : w] = z
-             * with w = getSize(t) = getSize(s)
-             * and z = 0 with getSize(z) = w  */
-            unsigned w = bv::utils::getSize(s);
-            Node z = bv::utils::mkZero(w);
-            Node z_o_t = nm->mkNode(BITVECTOR_CONCAT, z, t);
-            Node z_o_s = nm->mkNode(BITVECTOR_CONCAT, z, s);
-            Node zot_shl_zos = nm->mkNode(BITVECTOR_SHL, z_o_t, z_o_s);
-            Node ext = bv::utils::mkExtract(zot_shl_zos, 2*w-1, w);
-            scl = nm->mkNode(OR,
-                nm->mkNode(EQUAL, s, z),
-                nm->mkNode(EQUAL, ext, z));
-            scr = nm->mkNode(EQUAL, nm->mkNode(BITVECTOR_LSHR, x, s), t);
-            Node sc = nm->mkNode(IMPLIES, scl, scr);
-            Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc
-                               << std::endl;
-            status.d_conds.push_back(sc);
-            /* t = skv (fresh skolem constant)  */
-            Node skv = getInversionNode(sc, solve_tn, m);
-            t = skv;
-          }
-          else
+          if (index == 1)
           {
             /* s >> x = t
              * with side condition:
@@ -656,41 +811,17 @@ Node BvInverter::solve_bv_lit(Node sv,
                                << ", from " << sv_t << std::endl;
             return Node::null();
           }
+
+          TypeNode solve_tn = sv_t[index].getType();
+          Node sc = getScBvLshr(k, index, getSolveVariable(solve_tn), s, t);
+          /* t = fresh skolem constant  */
+          t = getInversionNode(sc, solve_tn, m);
           break;
         }
 
         case BITVECTOR_ASHR:
         {
-          TypeNode solve_tn = sv_t[index].getType();
-          Node x = getSolveVariable(solve_tn);
-          Node scl, scr;
-          if (index == 0)
-          {
-            /* x >> s = t
-             * with side condition:
-             * s = 0 || (sext(t,w) << s)[2w-1 : w] = sext(t[w-1:w-1], w-1)
-             * with w = getSize(t) = getSize(s)  */
-            unsigned w = bv::utils::getSize(s);
-            Node z = bv::utils::mkZero(w);
-            Node s1 = bv::utils::mkSignExtend(t, w);
-            Node z_o_s = nm->mkNode(BITVECTOR_CONCAT, z, s);
-            Node s1_shl_zos = nm->mkNode(BITVECTOR_SHL, s1, z_o_s);
-            Node msb_t = bv::utils::mkExtract(t, w-1, w-1);
-            Node s2 = bv::utils::mkSignExtend(msb_t, w-1);
-            Node ext = bv::utils::mkExtract(s1_shl_zos, 2*w-1, w);
-            scl = nm->mkNode(OR,
-                nm->mkNode(EQUAL, s, z),
-                nm->mkNode(EQUAL, ext, s2));
-            scr = nm->mkNode(EQUAL, nm->mkNode(BITVECTOR_LSHR, x, s), t);
-            Node sc = nm->mkNode(IMPLIES, scl, scr);
-            Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc
-                               << std::endl;
-            status.d_conds.push_back(sc);
-            /* t = skv (fresh skolem constant)  */
-            Node skv = getInversionNode(sc, solve_tn, m);
-            t = skv;
-          }
-          else
+          if (index == 1)
           {
             /* s >> x = t
              * with side condition:
@@ -704,39 +835,16 @@ Node BvInverter::solve_bv_lit(Node sv,
                                << ", from " << sv_t << std::endl;
             return Node::null();
           }
+          TypeNode solve_tn = sv_t[index].getType();
+          Node sc = getScBvAshr(k, index, getSolveVariable(solve_tn), s, t);
+          /* t = fresh skolem constant  */
+          t = getInversionNode(sc, solve_tn, m);
           break;
         }
 
         case BITVECTOR_SHL:
         {
-          TypeNode solve_tn = sv_t[index].getType();
-          Node x = getSolveVariable(solve_tn);
-          Node s = sv_t[1 - index];
-          unsigned w = bv::utils::getSize(s);
-          Node scl, scr;
-
-          if (index == 0)
-          {
-            /* x << s = t
-             * with side condition:
-             * (s = 0 || ctz(t) >= s)
-             * <->
-             * (s = 0 || ((t o z) >> (z o s))[w-1:0] = z)
-             *
-             * where
-             * w = getSize(s) = getSize(t) = getSize (z) && z = 0
-             */
-            Node zero = bv::utils::mkConst(w, 0u);
-            Node s_eq_zero = nm->mkNode(EQUAL, s, zero);
-            Node t_conc_zero = nm->mkNode(BITVECTOR_CONCAT, t, zero);
-            Node zero_conc_s = nm->mkNode(BITVECTOR_CONCAT, zero, s);
-            Node shr_s = nm->mkNode(BITVECTOR_LSHR, t_conc_zero, zero_conc_s);
-            Node extr_shr_s = bv::utils::mkExtract(shr_s, w - 1, 0);
-            Node ctz_t_ge_s = nm->mkNode(EQUAL, extr_shr_s, zero);
-            scl = nm->mkNode(OR, s_eq_zero, ctz_t_ge_s);
-            scr = nm->mkNode(EQUAL, nm->mkNode(BITVECTOR_SHL, x, s), t);
-          }
-          else
+          if (index == 1)
           {
             /* s << x = t
              * with side condition:
@@ -749,19 +857,10 @@ Node BvInverter::solve_bv_lit(Node sv,
                                << "for bit-vector term " << sv_t << std::endl;
             return Node::null();
           }
-
-          /* overall side condition */
-          Node sc = nm->mkNode(IMPLIES, scl, scr);
-          Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc
-                             << std::endl;
-          /* add side condition */
-          status.d_conds.push_back(sc);
-
-          /* t = skv (fresh skolem constant)
-           * get the skolem node for this side condition */
-          Node skv = getInversionNode(sc, solve_tn, m);
-          /* now solving with the skolem node as the RHS */
-          t = skv;
+          TypeNode solve_tn = sv_t[index].getType();
+          Node sc = getScBvShl(k, index, getSolveVariable(solve_tn), s, t);
+          /* t = fresh skolem constant */
+          t = getInversionNode(sc, solve_tn, m);
           break;
         }
 
@@ -777,6 +876,8 @@ Node BvInverter::solve_bv_lit(Node sv,
   return t;
 }
 
+/*---------------------------------------------------------------------------*/
+
 }  // namespace quantifiers
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/quantifiers/bv_inverter.h b/src/theory/quantifiers/bv_inverter.h
index 56f8d492b..a44d64904 100644
--- a/src/theory/quantifiers/bv_inverter.h
+++ b/src/theory/quantifiers/bv_inverter.h
@@ -50,9 +50,6 @@ class BvInverterStatus {
   BvInverterStatus() : d_status(0) {}
   ~BvInverterStatus() {}
   int d_status;
-  // TODO : may not need this (conditions now appear explicitly in solved
-  // forms) side conditions
-  std::vector<Node> d_conds;
 };
 
 // inverter class
@@ -89,15 +86,15 @@ class BvInverter {
   Node getPathToPv(Node lit, Node pv, Node sv, Node pvs,
                    std::vector<unsigned>& path);
 
-  /** solve_bv_lit
+  /** solveBvLit
    * solve for sv in lit, where lit.path = sv
    * status accumulates side conditions
    */
-  Node solve_bv_lit(Node sv,
-                    Node lit,
-                    std::vector<unsigned>& path,
-                    BvInverterQuery* m,
-                    BvInverterStatus& status);
+  Node solveBvLit(Node sv,
+                  Node lit,
+                  std::vector<unsigned>& path,
+                  BvInverterQuery* m,
+                  BvInverterStatus& status);
 
  private:
   /** dummy variables for each type */
@@ -106,9 +103,6 @@ class BvInverter {
   /** helper function for getPathToPv */
   Node getPathToPv(Node lit, Node pv, Node sv, std::vector<unsigned>& path,
                    std::unordered_set<TNode, TNodeHashFunction>& visited);
-
-  // is operator k invertible?
-  bool isInvertible(Kind k, unsigned index);
 };
 
 }  // namespace quantifiers
diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp
index 4fb31f90b..18086cbd5 100644
--- a/src/theory/quantifiers/ceg_t_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_t_instantiator.cpp
@@ -987,7 +987,8 @@ void BvInstantiator::processLiteral(CegInstantiator* ci,
     CegInstantiatorBvInverterQuery m(ci);
     unsigned iid = d_inst_id_counter;
     Trace("cegqi-bv") << "Solve lit to bv inverter : " << slit << std::endl;
-    Node inst = d_inverter->solve_bv_lit( sv, slit, path, &m, d_inst_id_to_status[iid] );
+    Node inst =
+        d_inverter->solveBvLit(sv, slit, path, &m, d_inst_id_to_status[iid]);
     if( !inst.isNull() ){
       inst = Rewriter::rewrite(inst);
       Trace("cegqi-bv") << "...solved form is " << inst << std::endl;
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-udiv-1.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-udiv-1.smt2
index 0373cf8f3..bf69a8b4a 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-udiv-1.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-udiv-1.smt2
@@ -2,10 +2,10 @@
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
-(declare-fun a () (_ BitVec 16))
-(declare-fun b () (_ BitVec 16))
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
 
-(assert (distinct a b (_ bv0 16)))
-(assert (forall ((x (_ BitVec 16))) (not (= (bvudiv a x) b))))
+(assert (distinct a b (_ bv0 8)))
+(assert (forall ((x (_ BitVec 8))) (not (= (bvudiv a x) b))))
 
 (check-sat)
diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index 9de940a0d..dfa3c79b6 100644
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -13,6 +13,7 @@ UNIT_TESTS += \
 	theory/theory_arith_white \
 	theory/theory_bv_white \
 	theory/theory_bv_bvgauss_white \
+	theory/theory_quantifiers_bv_inverter_white \
 	theory/type_enumerator_white \
 	expr/node_white \
 	expr/node_black \
diff --git a/test/unit/theory/theory_quantifiers_bv_inverter_white.h b/test/unit/theory/theory_quantifiers_bv_inverter_white.h
new file mode 100644
index 000000000..04c97a831
--- /dev/null
+++ b/test/unit/theory/theory_quantifiers_bv_inverter_white.h
@@ -0,0 +1,272 @@
+/*********************                                                        */
+/*! \file theory_quantifiers_bv_inverter_white.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Unit tests for BV inverter.
+ **
+ ** Unit tests for BV inverter.
+ **/
+
+#include "theory/quantifiers/bv_inverter.cpp"
+
+#include "expr/node.h"
+#include "expr/node_manager.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
+#include "util/result.h"
+
+using namespace CVC4;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+using namespace CVC4::smt;
+
+class TheoryQuantifiersBvInverter : public CxxTest::TestSuite
+{
+  ExprManager *d_em;
+  NodeManager *d_nm;
+  SmtEngine *d_smt;
+  SmtScope *d_scope;
+
+  Node d_s;
+  Node d_t;
+  Node d_sk;
+  Node d_x;
+  Node d_bvarlist;
+
+  void runTestPred(bool pol,
+                   Kind k,
+                   unsigned idx,
+                   Node (*getsc)(bool, Kind, unsigned, Node, Node))
+  {
+    Assert(k == kind::BITVECTOR_ULT
+        || k == kind::BITVECTOR_SLT
+        || k == kind::EQUAL);
+    Assert(k != kind::EQUAL || pol == false);
+
+    Node sc = getsc(pol, k, idx, d_sk, d_t);
+    Kind ksc = sc.getKind();
+    TS_ASSERT((k == kind::BITVECTOR_ULT && pol == false)
+           || (k == kind::BITVECTOR_SLT && pol == false)
+           || ksc == kind::IMPLIES);
+    Node scl = ksc == kind::IMPLIES ? sc[0] : bv::utils::mkTrue();
+    if (!pol)
+    {
+      k = k == kind::BITVECTOR_ULT
+        ? kind::BITVECTOR_UGE
+        : (k == kind::BITVECTOR_SLT ? kind::BITVECTOR_SGE : kind::DISTINCT);
+    }
+    Node body = idx == 0
+      ? d_nm->mkNode(k, d_x, d_t)
+      : d_nm->mkNode(k, d_t, d_x);
+    Node scr = d_nm->mkNode(kind::EXISTS, d_bvarlist, body);
+    Expr a = d_nm->mkNode(kind::DISTINCT, scl, scr).toExpr();
+    Result res = d_smt->checkSat(a);
+    TS_ASSERT(res.d_sat == Result::UNSAT);
+  }
+
+  void runTest(Kind k,
+               unsigned idx,
+               Node (*getsc)(Kind, unsigned, Node, Node, Node))
+  {
+    Assert(k == kind::BITVECTOR_MULT
+           || k == kind::BITVECTOR_UREM_TOTAL
+           || k == kind::BITVECTOR_UDIV_TOTAL
+           || k == kind::BITVECTOR_AND
+           || k == kind::BITVECTOR_OR
+           || k == kind::BITVECTOR_LSHR
+           || k == kind::BITVECTOR_ASHR
+           || k == kind::BITVECTOR_SHL);
+    Assert(k != kind::BITVECTOR_UREM_TOTAL || idx == 1);
+    Assert((k != kind::BITVECTOR_LSHR
+            && k != kind::BITVECTOR_ASHR
+            && k != kind::BITVECTOR_SHL)
+           || idx == 0);
+
+    Node sc = getsc(k, idx, d_sk, d_s, d_t);
+    Kind ksc = sc.getKind();
+    TS_ASSERT(ksc == kind::IMPLIES);
+    Node body = idx == 0
+      ? d_nm->mkNode(k, d_x, d_s).eqNode(d_t)
+      : d_nm->mkNode(k, d_s, d_x).eqNode(d_t);
+    Node scr = d_nm->mkNode(kind::EXISTS, d_bvarlist, body);
+    Expr a = d_nm->mkNode(kind::DISTINCT, sc[0], scr).toExpr();
+    Result res = d_smt->checkSat(a);
+    TS_ASSERT(res.d_sat == Result::UNSAT);
+  }
+
+ public:
+  TheoryQuantifiersBvInverter() {}
+
+  void setUp()
+  {
+    d_em = new ExprManager();
+    d_nm = NodeManager::fromExprManager(d_em);
+    d_smt = new SmtEngine(d_em);
+    d_smt->setOption("cbqi-bv", CVC4::SExpr(false));
+    d_scope = new SmtScope(d_smt);
+
+    d_s = d_nm->mkVar("s", d_nm->mkBitVectorType(4));
+    d_t = d_nm->mkVar("t", d_nm->mkBitVectorType(4));
+    d_sk = d_nm->mkSkolem("sk", d_t.getType());
+    d_x = d_nm->mkBoundVar(d_t.getType());
+    d_bvarlist = d_nm->mkNode(kind::BOUND_VAR_LIST, { d_x });
+  }
+
+  void tearDown()
+  {
+    d_bvarlist = Node::null();
+    d_x = Node::null();
+    d_sk = Node::null();
+    d_t = Node::null();
+    d_s = Node::null();
+    delete d_scope;
+    delete d_smt;
+    delete d_em;
+  }
+
+  void testGetScBvUltTrue0()
+  {
+    runTestPred(true, BITVECTOR_ULT, 0, getScBvUlt);
+  }
+
+  void testGetScBvUltTrue1()
+  {
+    runTestPred(true, BITVECTOR_ULT, 1, getScBvUlt);
+  }
+
+  void testGetScBvUltFalse0()
+  {
+    runTestPred(false, BITVECTOR_ULT, 0, getScBvUlt);
+  }
+
+  void testGetScBvUltFalse1()
+  {
+    runTestPred(false, BITVECTOR_ULT, 1, getScBvUlt);
+  }
+
+  void testGetScBvSltTrue0()
+  {
+    runTestPred(true, BITVECTOR_SLT, 0, getScBvSlt);
+  }
+
+  void testGetScBvSltTrue1()
+  {
+    runTestPred(true, BITVECTOR_SLT, 1, getScBvSlt);
+  }
+
+  void testGetScBvSltFalse0()
+  {
+    runTestPred(false, BITVECTOR_SLT, 0, getScBvSlt);
+  }
+
+  void testGetScBvSltFalse1()
+  {
+    runTestPred(false, BITVECTOR_SLT, 1, getScBvSlt);
+  }
+
+  void testGetScBvEq0()
+  {
+    runTestPred(false, EQUAL, 0, getScBvEq);
+    TS_ASSERT_THROWS(runTestPred(true, EQUAL, 0, getScBvEq),
+                     AssertionException);
+  }
+
+  void testGetScBvEq1()
+  {
+    runTestPred(false, EQUAL, 1, getScBvEq);
+    TS_ASSERT_THROWS(runTestPred(true, EQUAL, 1, getScBvEq),
+                     AssertionException);
+  }
+
+  void testGetScBvMult0()
+  {
+    runTest(BITVECTOR_MULT, 0, getScBvMult);
+  }
+
+  void testGetScBvMult1()
+  {
+    runTest(BITVECTOR_MULT, 1, getScBvMult);
+  }
+
+  void testGetScBvUrem0()
+  {
+    TS_ASSERT_THROWS(runTest(BITVECTOR_UREM_TOTAL, 0, getScBvUrem),
+                     AssertionException);
+  }
+
+  void testGetScBvUrem1()
+  {
+    runTest(BITVECTOR_UREM_TOTAL, 1, getScBvUrem);
+  }
+
+  void testGetScBvUdiv0()
+  {
+    runTest(BITVECTOR_UDIV_TOTAL, 0, getScBvUdiv);
+  }
+
+  void testGetScBvUdiv1()
+  {
+    runTest(BITVECTOR_UDIV_TOTAL, 1, getScBvUdiv);
+  }
+
+  void testGetScBvAnd0()
+  {
+    runTest(BITVECTOR_AND, 0, getScBvAndOr);
+  }
+
+  void testGetScBvAnd1()
+  {
+    runTest(BITVECTOR_AND, 1, getScBvAndOr);
+  }
+
+  void testGetScBvOr0()
+  {
+    runTest(BITVECTOR_OR, 0, getScBvAndOr);
+  }
+
+  void testGetScBvOr1()
+  {
+    runTest(BITVECTOR_OR, 1, getScBvAndOr);
+  }
+
+  void testGetScBvLshr0()
+  {
+    runTest(BITVECTOR_LSHR, 0, getScBvLshr);
+  }
+
+  void testGetScBvLshr1()
+  {
+    TS_ASSERT_THROWS(runTest(BITVECTOR_LSHR, 1, getScBvLshr),
+                     AssertionException);
+  }
+
+  void testGetScBvAshr0()
+  {
+    runTest(BITVECTOR_ASHR, 0, getScBvAshr);
+  }
+
+  void testGetScBvAshr1()
+  {
+    TS_ASSERT_THROWS(runTest(BITVECTOR_ASHR, 1, getScBvAshr),
+                     AssertionException);
+  }
+
+  void testGetScBvShl0()
+  {
+    runTest(BITVECTOR_SHL, 0, getScBvShl);
+  }
+
+  void testGetScBvShl1()
+  {
+    TS_ASSERT_THROWS(runTest(BITVECTOR_SHL, 1, getScBvShl),
+                     AssertionException);
+  }
+
+};