Add explicit disequality handling when generating side condition for CBQI BV. (#1447)

This refactors solveBvLit to support explicit handling of disequalities (and, in the next step, inequalities) when generating side conditions.

48 files changed, 1121 insertions, 675 deletions

diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp
index 0ac22a3e4..11d6ba85d 100644
--- a/src/theory/quantifiers/bv_inverter.cpp
+++ b/src/theory/quantifiers/bv_inverter.cpp
@@ -50,6 +50,8 @@ Node BvInverter::getSolveVariable(TypeNode tn)
 
 Node BvInverter::getInversionNode(Node cond, TypeNode tn, BvInverterQuery* m)
 {
+  TNode solve_var = getSolveVariable(tn);
+
   // condition should be rewritten
   Node new_cond = Rewriter::rewrite(cond);
   if (new_cond != cond)
@@ -58,11 +60,10 @@ Node BvInverter::getInversionNode(Node cond, TypeNode tn, BvInverterQuery* m)
                                    << " was rewritten to " << new_cond
                                    << std::endl;
   }
+  // optimization : if condition is ( x = solve_var ) should just return
+  // solve_var and not introduce a Skolem this can happen when we ask for
+  // the multiplicative inversion with bv1
   Node c;
-  // optimization : if condition is ( x = v ) should just return v and not
-  // introduce a Skolem this can happen when we ask for the multiplicative
-  // inversion with bv1
-  TNode solve_var = getSolveVariable(tn);
   if (new_cond.getKind() == EQUAL)
   {
     for (unsigned i = 0; i < 2; i++)
@@ -225,6 +226,8 @@ static Node getScBvUlt(bool pol, Kind k, unsigned idx, Node x, Node t)
     }
     else
     {
+      /* x >= t
+       * no side condition  */
       sc = nm->mkNode(NOT, nm->mkNode(k, x, t));
     }
   }
@@ -241,6 +244,8 @@ static Node getScBvUlt(bool pol, Kind k, unsigned idx, Node x, Node t)
     }
     else
     {
+      /* t >= x
+       * no side condition */
       sc = nm->mkNode(NOT, nm->mkNode(k, t, x));
     }
   }
@@ -270,6 +275,8 @@ static Node getScBvSlt(bool pol, Kind k, unsigned idx, Node x, Node t)
     }
     else
     {
+      /* x >= t
+       * no side condition */
       sc = nm->mkNode(NOT, nm->mkNode(k, x, t));
     }
   }
@@ -288,6 +295,8 @@ static Node getScBvSlt(bool pol, Kind k, unsigned idx, Node x, Node t)
     }
     else
     {
+      /* t >= x
+       * no side condition */
       sc = nm->mkNode(NOT, nm->mkNode(k, t, x));
     }
   }
@@ -295,392 +304,617 @@ static Node getScBvSlt(bool pol, Kind k, unsigned idx, Node x, Node t)
   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)
+static Node getScBvMult(bool pol,
+                        Kind litk,
+                        Kind k,
+                        unsigned idx,
+                        Node x,
+                        Node s,
+                        Node t)
 {
   Assert(k == BITVECTOR_MULT);
 
+  if (litk != EQUAL)
+  {
+    return Node::null();
+  }
+
   NodeManager* nm = NodeManager::currentNM();
+  Node scl, scr;
+  Node z = bv::utils::mkZero(bv::utils::getSize(s));
+
+  if (pol)
+  {
+    /* 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 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)));
+    scl = nm->mkNode(OR,
+        t.eqNode(z),
+        nm->mkNode(AND, t_uge_s, s.eqNode(z).notNode()));
+    scr = nm->mkNode(EQUAL, nm->mkNode(k, x, s), t);
+  }
+  else
+  {
+    /* x * s != t
+     * with side condition:
+     * t != 0 || s != 0 */
+    scl = nm->mkNode(OR, t.eqNode(z).notNode(), s.eqNode(z).notNode());
+    scr = nm->mkNode(DISTINCT, nm->mkNode(k, x, s), t);
+  }
 
-  /* 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)
+static Node getScBvUrem(bool pol,
+                        Kind litk,
+                        Kind k,
+                        unsigned idx,
+                        Node x,
+                        Node s,
+                        Node t)
 {
   Assert(k == BITVECTOR_UREM_TOTAL);
-  Assert(idx == 1);
+  Assert(pol == false || idx == 1);
+
+  if (litk != EQUAL)
+  {
+    return Node::null();
+  }
 
   NodeManager* nm = NodeManager::currentNM();
+  Node scl, scr;
+  unsigned w = bv::utils::getSize(s);
+  Assert (w == bv::utils::getSize(t));
+  Node z = bv::utils::mkZero(w);
 
-  /* 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);
+  if (idx == 0)
+  {
+    Assert (pol == false);
+    /* x % s != t
+     * with side condition:
+     * s != 1 || t != 0  */
+    scl = nm->mkNode(OR,
+        s.eqNode(bv::utils::mkOne(w)).notNode(),
+        t.eqNode(z).notNode());
+    scr = nm->mkNode(DISTINCT, nm->mkNode(k, x, s), t);
+  }
+  else
+  {
+    if (pol)
+    {
+      /* s % x = t
+       * with side condition:
+       * s = t
+       * ||
+       * ( s > t
+       *   && s-t > t
+       *   && (t = 0 || t != s-1) )  */
+
+      Node a1 = nm->mkNode(BITVECTOR_UGT, s, t);
+      Node a2 = nm->mkNode(BITVECTOR_UGT, nm->mkNode(BITVECTOR_SUB, s, t), t);
+      Node a3 = nm->mkNode(OR,
+          t.eqNode(z),
+          t.eqNode(bv::utils::mkDec(s)).notNode());
+
+      scl = nm->mkNode(OR,
+            t.eqNode(s),
+            nm->mkNode(AND, a1, nm->mkNode(AND, a2, a3)));
+      scr = nm->mkNode(EQUAL, nm->mkNode(k, s, x), t);
+    }
+    else
+    {
+      /* s % x != t
+       * with side condition:
+       * s != 0 || t != 0  */
+      scl = nm->mkNode(OR, s.eqNode(z).notNode(), t.eqNode(z).notNode());
+      scr = nm->mkNode(DISTINCT, 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)
+static Node getScBvUdiv(bool pol,
+                        Kind litk,
+                        Kind k,
+                        unsigned idx,
+                        Node x,
+                        Node s,
+                        Node t)
 {
   Assert(k == BITVECTOR_UDIV_TOTAL);
 
+  if (litk != EQUAL)
+  {
+    return Node::null();
+  }
+
   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);
+  Node sc, scl, scr;
+  Node z = bv::utils::mkZero(w);
+  Node n = bv::utils::mkOnes(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);
+    if (pol)
+    {
+      /* x udiv s = t
+       * with side condition:
+       * t = ~0 && (s = 0 || s = 1)
+       * ||
+       * (t != ~0 && s != 0 && !umulo(s * t)) */
+      Node one = bv::utils::mkOne(w);
+      Node o1 = nm->mkNode(AND,
+          t.eqNode(n),
+          nm->mkNode(OR, s.eqNode(z), s.eqNode(one)));
+      Node o2 = nm->mkNode(AND,
+          t.eqNode(n).notNode(),
+          s.eqNode(z).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
+    {
+      /* x udiv s != t
+       * with side condition:
+       * s != 0 || t != ~0  */
+      scl = nm->mkNode(OR, s.eqNode(z).notNode(), t.eqNode(n).notNode());
+      scr = nm->mkNode(DISTINCT, nm->mkNode(k, x, s), t);
+    }
+    sc = nm->mkNode(IMPLIES, scl, scr);
   }
   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);
+    if (pol)
+    {
+      /* 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), z); 
+      Node udiv = nm->mkNode(BITVECTOR_UDIV_TOTAL, s, bv::utils::mkInc(t));
+      Node ule1 = bv::utils::mkInc(udiv);
+      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(n), t.eqNode(z).notNode());
+
+      Node o1 = s.eqNode(t);
+      Node o2 = t.eqNode(n);
+      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);
+      sc = nm->mkNode(IMPLIES, scl, scr);
+    }
+    else
+    {
+      sc = nm->mkNode(DISTINCT, 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)
+static Node getScBvAndOr(bool pol,
+                         Kind litk,
+                         Kind k,
+                         unsigned idx,
+                         Node x,
+                         Node s,
+                         Node t)
 {
+  Assert (k == BITVECTOR_AND || k == BITVECTOR_OR);
+
+  if (litk != EQUAL)
+  {
+    return Node::null();
+  }
+
   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 scl, scr;
+
+  if (pol)
+  {
+    /* x & s = t
+     * x | s = t
+     * with side condition:
+     * t & s = t
+     * t | s = t */
+    scl = nm->mkNode(EQUAL, t, nm->mkNode(k, t, s));
+    scr = nm->mkNode(EQUAL, nm->mkNode(k, x, s), t);
+  }
+  else
+  {
+    unsigned w = bv::utils::getSize(s);
+    Assert (w == bv::utils::getSize(t));
+
+    if (k == BITVECTOR_AND)
+    {
+      /* x & s = t
+       * with side condition:
+       * s != 0 || t != 0  */
+      Node z = bv::utils::mkZero(w);
+      scl = nm->mkNode(OR, s.eqNode(z).notNode(), t.eqNode(z).notNode());
+    }
+    else
+    {
+      /* x | s = t
+       * with side condition:
+       * s != ~0 || t != ~0  */
+      Node n = bv::utils::mkOnes(w);
+      scl = nm->mkNode(OR, s.eqNode(n).notNode(), t.eqNode(n).notNode());
+    }
+    scr = nm->mkNode(DISTINCT, 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)
+static Node getScBvLshr(bool pol,
+                        Kind litk,
+                        Kind k,
+                        unsigned idx,
+                        Node x,
+                        Node s,
+                        Node t)
 {
   Assert(k == BITVECTOR_LSHR);
 
+  if (litk != EQUAL)
+  {
+    return Node::null();
+  }
+
   NodeManager* nm = NodeManager::currentNM();
   Node scl, scr;
   unsigned w = bv::utils::getSize(s);
   Assert(w == bv::utils::getSize(t));
   Node z = bv::utils::mkZero(w);
-  
+
   if (idx == 0)
   {
-    /* 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 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));
-
-    scl = nm->mkNode(OR, o1, o2, o3);
-    scr = nm->mkNode(EQUAL, nm->mkNode(k, x, s), t);
+    if (pol)
+    {
+      /* 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_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));
+
+      scl = nm->mkNode(OR, o1, o2, o3);
+      scr = nm->mkNode(EQUAL, nm->mkNode(k, x, s), t);
+    }
+    else
+    {
+      /* x >> s != t
+       * with side condition:
+       * t != 0 || s < w
+       * with
+       * w = getSize(s) = getSize(t)
+       */
+      scl = nm->mkNode(OR,
+          t.eqNode(z).notNode(),
+          nm->mkNode(BITVECTOR_ULT, s, ww));
+      scr = nm->mkNode(DISTINCT, nm->mkNode(k, x, s), t);
+    }
   }
   else
   {
-    /* s >> x = t
-     * with side condition:
-     * t = 0
-     * ||
-     * s = t
-     * || 
-     * \/ (t[w-1-i:0] = s[w-1:i] && t[w-1:w-i] = 0) for 0 < i < w
-     * where
-     * w = getSize(s) = getSize(t)
-     */
-    NodeBuilder<> nb(nm, OR);
-    nb << nm->mkNode(EQUAL, t, s);
-    for (unsigned i = 1; i < w; ++i)
-    {
-      nb << nm->mkNode(AND,
-          nm->mkNode(EQUAL,
-            bv::utils::mkExtract(t, w-1-i, 0), bv::utils::mkExtract(s, w-1, i)),
-          nm->mkNode(EQUAL,
-            bv::utils::mkExtract(t, w-1, w-i), bv::utils::mkZero(i)));
-    }
-    nb << t.eqNode(z);
-    scl = nb.constructNode();
-    scr = nm->mkNode(EQUAL, nm->mkNode(k, s, x), t);
+    if (pol)
+    {
+      /* s >> x = t
+       * with side condition:
+       * t = 0
+       * ||
+       * s = t
+       * || 
+       * \/ (t[w-1-i:0] = s[w-1:i] && t[w-1:w-i] = 0) for 0 < i < w
+       * where
+       * w = getSize(s) = getSize(t)
+       */
+      NodeBuilder<> nb(nm, OR);
+      nb << nm->mkNode(EQUAL, t, s);
+      for (unsigned i = 1; i < w; ++i)
+      {
+        nb << nm->mkNode(AND,
+            nm->mkNode(EQUAL,
+              bv::utils::mkExtract(t, w - 1 - i, 0),
+              bv::utils::mkExtract(s, w - 1, i)),
+            nm->mkNode(EQUAL,
+              bv::utils::mkExtract(t, w - 1, w - i),
+              bv::utils::mkZero(i)));
+      }
+      nb << t.eqNode(z);
+      scl = nb.constructNode();
+      scr = nm->mkNode(EQUAL, nm->mkNode(k, s, x), t);
+    }
+    else
+    {
+      /* s >> x != t
+       * with side condition:
+       * s != 0 || t != 0  */
+      scl = nm->mkNode(OR, s.eqNode(z).notNode(), t.eqNode(z).notNode());
+      scr = nm->mkNode(DISTINCT, 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 getScBvAshr(Kind k, unsigned idx, Node x, Node s, Node t)
+static Node getScBvAshr(bool pol,
+                        Kind litk,
+                        Kind k,
+                        unsigned idx,
+                        Node x,
+                        Node s,
+                        Node t)
 {
   Assert(k == BITVECTOR_ASHR);
 
+  if (litk != EQUAL)
+  {
+    return Node::null();
+  }
+
   NodeManager* nm = NodeManager::currentNM();
   Node scl, scr;
   unsigned w = bv::utils::getSize(s);
   Assert(w == bv::utils::getSize(t));
   Node z = bv::utils::mkZero(w);
   Node n = bv::utils::mkOnes(w);
-  
+
   if (idx == 0)
   {
-    /* 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 zz = bv::utils::mkZero(w+1);
-    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)));
-
-    scl = nm->mkNode(OR, o1, o2, o3);
-    scr = nm->mkNode(EQUAL, nm->mkNode(k, x, s), t);
+    if (pol)
+    {
+      /* 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 zz = bv::utils::mkZero(w+1);
+      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)));
+
+      scl = nm->mkNode(OR, o1, o2, o3);
+      scr = nm->mkNode(EQUAL, nm->mkNode(k, x, s), t);
+    }
+    else
+    {
+      /* x >> s != t
+       * no side condition */
+      scr = nm->mkNode(DISTINCT, nm->mkNode(k, x, s), t);
+    }
   }
   else
   {
-    /* s >> x = t
-     * with side condition:
-     * (s[w-1:w-1] = 0 && t = 0)
-     * ||
-     * (s[w-1:w-1] = 1 && t == ~0)
-     * ||
-     * s = t
-     * || 
-     * \/ (t[w-1-i:0] = s[w-1:i]
-     *     && ((s[w-1:w-1] = 0 && t[w-1:w-i] = 0)
-     *         ||
-     *         (s[w-1:w-1] = 1 &&  t[w-1:w-i] = ~0)))
-     * for 0 < i < w
-     * where
-     * w = getSize(s) = getSize(t)
-     */
-    Node msbz = bv::utils::mkExtract(s, w-1, w-1).eqNode(bv::utils::mkZero(1));
-    Node msbn = bv::utils::mkExtract(s, w-1, w-1).eqNode(bv::utils::mkOnes(1));
-    NodeBuilder<> nb(nm, OR);
-    nb << nm->mkNode(EQUAL, t, s);
-    for (unsigned i = 1; i < w; ++i)
+    if (pol)
     {
+      /* s >> x = t
+       * with side condition:
+       * (s[w-1:w-1] = 0 && t = 0)
+       * ||
+       * (s[w-1:w-1] = 1 && t == ~0)
+       * ||
+       * s = t
+       * || 
+       * \/ (t[w-1-i:0] = s[w-1:i]
+       *     && ((s[w-1:w-1] = 0 && t[w-1:w-i] = 0)
+       *         ||
+       *         (s[w-1:w-1] = 1 &&  t[w-1:w-i] = ~0)))
+       * for 0 < i < w
+       * where
+       * w = getSize(s) = getSize(t)
+       */
+      Node msbz = bv::utils::mkExtract(
+          s, w-1, w-1).eqNode(bv::utils::mkZero(1));
+      Node msbn = bv::utils::mkExtract(
+          s, w-1, w-1).eqNode(bv::utils::mkOnes(1));
+      NodeBuilder<> nb(nm, OR);
+      nb << nm->mkNode(EQUAL, t, s);
+      for (unsigned i = 1; i < w; ++i)
+      {
+        Node ext = bv::utils::mkExtract(t, w-1, w-i);
 
-      Node ext = bv::utils::mkExtract(t, w-1, w-i);
-
-      Node o1 = nm->mkNode(AND, msbz, ext.eqNode(bv::utils::mkZero(i)));
-      Node o2 = nm->mkNode(AND, msbn, ext.eqNode(bv::utils::mkOnes(i)));
-      Node o = nm->mkNode(OR, o1, o2);
+        Node o1 = nm->mkNode(AND, msbz, ext.eqNode(bv::utils::mkZero(i)));
+        Node o2 = nm->mkNode(AND, msbn, ext.eqNode(bv::utils::mkOnes(i)));
+        Node o = nm->mkNode(OR, o1, o2);
 
-      Node e = nm->mkNode(EQUAL,
-          bv::utils::mkExtract(t, w-1-i, 0), bv::utils::mkExtract(s, w-1, i));
+        Node e = nm->mkNode(EQUAL,
+            bv::utils::mkExtract(t, w-1-i, 0), bv::utils::mkExtract(s, w-1, i));
 
-      nb << nm->mkNode(AND, e, o);
+        nb << nm->mkNode(AND, e, o);
+      }
+      nb << nm->mkNode(AND, msbz, t.eqNode(z));
+      nb << nm->mkNode(AND, msbn, t.eqNode(n));
+      scl = nb.constructNode();
+      scr = nm->mkNode(EQUAL, nm->mkNode(k, s, x), t);
+    }
+    else
+    {
+      /* s >> x != t
+       * with side condition:
+       * (t != 0 || s != 0) && (t != ~0 || s != ~0)  */
+      scl = nm->mkNode(AND,
+          nm->mkNode(OR, t.eqNode(z).notNode(), s.eqNode(z).notNode()),
+          nm->mkNode(OR, t.eqNode(n).notNode(), s.eqNode(n).notNode()));
+      scr = nm->mkNode(DISTINCT, nm->mkNode(k, s, x), t);
     }
-    nb << nm->mkNode(AND, msbz, t.eqNode(z));
-    nb << nm->mkNode(AND, msbn, t.eqNode(n));
-    scl = nb.constructNode();
-    scr = nm->mkNode(EQUAL, nm->mkNode(k, s, x), t);
   }
-  Node sc = nm->mkNode(IMPLIES, scl, scr);
+  Node sc = scl.isNull() ? scr : 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)
+static Node getScBvShl(bool pol,
+                       Kind litk,
+                       Kind k,
+                       unsigned idx,
+                       Node x,
+                       Node s,
+                       Node t)
 {
   Assert(k == BITVECTOR_SHL);
 
+  if (litk != EQUAL)
+  {
+    return Node::null();
+  }
+
   NodeManager* nm = NodeManager::currentNM();
   Node scl, scr;
   unsigned w = bv::utils::getSize(s);
   Assert(w == bv::utils::getSize(t));
-  Node z = bv::utils::mkConst(w, 0u);
+  Node z = bv::utils::mkZero(w);
 
   if (idx == 0)
   {
-    /* 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 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));
-
-    scl = nm->mkNode(OR, o1, o2, o3);
-    scr = nm->mkNode(EQUAL, nm->mkNode(k, x, s), t);
+    if (pol)
+    {
+      /* 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 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));
+
+      scl = nm->mkNode(OR, o1, o2, o3);
+      scr = nm->mkNode(EQUAL, nm->mkNode(k, x, s), t);
+    }
+    else
+    {
+      /* x << s != t
+       * with side condition:
+       * t != 0 || s < w
+       * with
+       * w = getSize(s) = getSize(t)
+       */
+      scl = nm->mkNode(OR,
+          t.eqNode(z).notNode(),
+          nm->mkNode(BITVECTOR_ULT, s, ww));
+      scr = nm->mkNode(DISTINCT, nm->mkNode(k, x, s), t);
+    }
   }
   else
   {
-    /* s << x = t
-     * with side condition:
-     * t = 0
-     * ||
-     * s = t
-     * || 
-     * \/ (t[w-1:i] = s[w-1-i:0] && t[i-1:0] = 0) for 0 < i < w
-     * where
-     * w = getSize(s) = getSize(t)
-     */
-    NodeBuilder<> nb(nm, OR);
-    nb << nm->mkNode(EQUAL, t, s);
-    for (unsigned i = 1; i < w; ++i)
-    {
-      nb << nm->mkNode(AND,
-          nm->mkNode(EQUAL,
-            bv::utils::mkExtract(t, w-1, i), bv::utils::mkExtract(s, w-1-i, 0)),
-          nm->mkNode(EQUAL,
-            bv::utils::mkExtract(t, i-1, 0), bv::utils::mkZero(i)));
-    }
-    nb << t.eqNode(z);
-    scl = nb.constructNode();
-    scr = nm->mkNode(EQUAL, nm->mkNode(k, s, x), t);
+    if (pol)
+    {
+      /* s << x = t
+       * with side condition:
+       * t = 0
+       * ||
+       * s = t
+       * || 
+       * \/ (t[w-1:i] = s[w-1-i:0] && t[i-1:0] = 0) for 0 < i < w
+       * where
+       * w = getSize(s) = getSize(t)
+       */
+      NodeBuilder<> nb(nm, OR);
+      nb << nm->mkNode(EQUAL, t, s);
+      for (unsigned i = 1; i < w; ++i)
+      {
+        nb << nm->mkNode(AND,
+            nm->mkNode(EQUAL,
+              bv::utils::mkExtract(t, w-1, i), bv::utils::mkExtract(s, w-1-i, 0)),
+            nm->mkNode(EQUAL,
+              bv::utils::mkExtract(t, i-1, 0), bv::utils::mkZero(i)));
+      }
+      nb << t.eqNode(z);
+      scl = nb.constructNode();
+      scr = nm->mkNode(EQUAL, nm->mkNode(k, s, x), t);
+    }
+    else
+    {
+      /* s << x != t
+       * with side condition:
+       * s != 0 || t != 0  */
+      scl = nm->mkNode(OR, s.eqNode(z).notNode(), t.eqNode(z).notNode());
+      scr = nm->mkNode(DISTINCT, nm->mkNode(k, s, x), t);
+    }
   }
   Node sc = nm->mkNode(IMPLIES, scl, scr);
   Trace("bv-invert") << "Add SC_" << k << "(" << x << "): " << sc << std::endl;
@@ -690,28 +924,27 @@ static Node getScBvShl(Kind k, unsigned idx, Node x, Node s, Node t)
 Node BvInverter::solveBvLit(Node sv,
                             Node lit,
                             std::vector<unsigned>& path,
-                            BvInverterQuery* m,
-                            BvInverterStatus& status)
+                            BvInverterQuery* m)
 {
   Assert(!path.empty());
 
   bool pol = true;
   unsigned index, nchildren;
   NodeManager* nm = NodeManager::currentNM();
-  Kind k;
+  Kind k, litk;
 
   Assert(!path.empty());
   index = path.back();
   Assert(index < lit.getNumChildren());
   path.pop_back();
-  k = lit.getKind();
-  
+  litk = k = lit.getKind();
+
   /* Note: option --bool-to-bv is currently disabled when CBQI BV
    *       is enabled. We currently do not support Boolean operators
    *       that are interpreted as bit-vector operators of width 1.  */
 
   /* Boolean layer ----------------------------------------------- */
-  
+
   if (k == NOT)
   {
     pol = !pol;
@@ -720,72 +953,16 @@ Node BvInverter::solveBvLit(Node sv,
     index = path.back();
     Assert(index < lit.getNumChildren());
     path.pop_back();
-    k = lit.getKind();
+    litk = k = lit.getKind();
   }
 
   Assert(k == EQUAL
       || k == BITVECTOR_ULT
-      || k == BITVECTOR_SLT
-      || k == BITVECTOR_COMP);
+      || k == BITVECTOR_SLT);
 
   Node sv_t = lit[index];
   Node t = lit[1-index];
 
-  switch (k)
-  {
-    case BITVECTOR_ULT:
-    {
-      TypeNode solve_tn = sv_t.getType();
-      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();
-        Assert(index < sv_t.getNumChildren());
-        path.pop_back();
-        sv_t = sv_t[index];
-        k = sv_t.getKind();
-      }
-      break;
-    }
-
-    case BITVECTOR_SLT:
-    {
-      TypeNode solve_tn = sv_t.getType();
-      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();
-        Assert(index < sv_t.getNumChildren());
-        path.pop_back();
-        sv_t = sv_t[index];
-        k = sv_t.getKind();
-      }
-      break;
-    }
-
-    default:
-      Assert(k == EQUAL);
-      if (pol == false)
-      {
-        TypeNode solve_tn = sv_t.getType();
-        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();
-          Assert(index < sv_t.getNumChildren());
-          path.pop_back();
-          sv_t = sv_t[index];
-          k = sv_t.getKind();
-        }
-      }
-  }
-
   /* Bit-vector layer -------------------------------------------- */
 
   while (!path.empty())
@@ -822,7 +999,7 @@ Node BvInverter::solveBvLit(Node sv,
     {
       t = bv::utils::mkExtract(t, bv::utils::getSize(sv_t[index]) - 1, 0);
     }
-    else if (k == BITVECTOR_EXTRACT)
+    else if (k == BITVECTOR_EXTRACT || k == BITVECTOR_COMP)
     {
       Trace("bv-invert") << "bv-invert : Unsupported for index " << index
                          << ", from " << sv_t << std::endl;
@@ -834,107 +1011,126 @@ Node BvInverter::solveBvLit(Node sv,
       Node s = nchildren == 2 ? sv_t[1 - index] : dropChild(sv_t, index);
       /* Note: All n-ary kinds except for CONCAT (i.e., AND, OR, MULT, PLUS)
        *       are commutative (no case split based on index). */
-      switch (k)
+      if (k == BITVECTOR_PLUS)
       {
-        case BITVECTOR_COMP:
-          t = s;
-          break;
-
-        case BITVECTOR_PLUS:
-          t = nm->mkNode(BITVECTOR_SUB, t, s);
-          break;
-
-        case BITVECTOR_SUB:
-          t = nm->mkNode(BITVECTOR_PLUS, t, s);
-          break;
+        t = nm->mkNode(BITVECTOR_SUB, t, s);
+      }
+      else if (k == BITVECTOR_SUB)
+      {
+        t = nm->mkNode(BITVECTOR_PLUS, t, s);
+      }
+      else if (k == BITVECTOR_XOR)
+      {
+        t = nm->mkNode(BITVECTOR_XOR, t, s);
+      }
+      else
+      {
+        TypeNode solve_tn = sv_t[index].getType();
+        Node sc;
 
-        case BITVECTOR_MULT:
+        switch (k)
         {
-          TypeNode solve_tn = sv_t[index].getType();
-          Node sc = getScBvMult(k, index, getSolveVariable(solve_tn), s, t);
-          /* t = fresh skolem constant */
-          t = getInversionNode(sc, solve_tn, m);
-          break;
+          case BITVECTOR_MULT:
+            sc = getScBvMult(
+                pol, litk, k, index, getSolveVariable(solve_tn), s, t);
+            break;
+
+          case BITVECTOR_SHL:
+            sc = getScBvShl(
+                pol, litk, k, index, getSolveVariable(solve_tn), s, t);
+            break;
+
+          case BITVECTOR_UREM_TOTAL:
+            if (index == 0)
+            {
+              /* x % s = t is rewritten to x - x / y * y */
+              Trace("bv-invert") << "bv-invert : Unsupported for index "
+                                 << index << ", from " << sv_t << std::endl;
+              return Node::null();
+            }
+            sc = getScBvUrem(
+                pol, litk, k, index, getSolveVariable(solve_tn), s, t);
+            break;
+
+          case BITVECTOR_UDIV_TOTAL:
+            sc = getScBvUdiv(
+                pol, litk, k, index, getSolveVariable(solve_tn), s, t);
+            break;
+
+          case BITVECTOR_AND:
+          case BITVECTOR_OR:
+            sc = getScBvAndOr(
+                pol, litk, k, index, getSolveVariable(solve_tn), s, t);
+            break;
+
+          case BITVECTOR_LSHR:
+            sc = getScBvLshr(
+                pol, litk, k, index, getSolveVariable(solve_tn), s, t);
+            break;
+
+          case BITVECTOR_ASHR:
+            sc = getScBvAshr(
+                pol, litk, k, index, getSolveVariable(solve_tn), s, t);
+            break;
+
+          default:
+            Trace("bv-invert") << "bv-invert : Unknown kind " << k
+                               << " for bit-vector term " << sv_t << std::endl;
+            return Node::null();
         }
-
-        case BITVECTOR_UREM_TOTAL:
+        Assert (litk != EQUAL || !sc.isNull());
+        /* No specific handling for litk and operator k, generate generic
+         * side condition. */
+        if (sc.isNull())
         {
-          if (index == 0)
+          solve_tn = sv_t.getType();
+          if (litk == BITVECTOR_ULT)
           {
-            /* x % s = t is rewritten to x - x / y * y */
-            Trace("bv-invert") << "bv-invert : Unsupported for index " << index
-                               << ", from " << sv_t << std::endl;
-            return Node::null();
+            sc = getScBvUlt(
+                pol, litk, index, getSolveVariable(solve_tn), t);
+          }
+          else
+          {
+            Assert (litk == BITVECTOR_SLT);
+            sc = getScBvSlt(
+                pol, litk, index, getSolveVariable(solve_tn), t);
           }
-          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 sc = getScBvUdiv(k, index, getSolveVariable(solve_tn), s, t);
-          /* t = fresh skolem constant */
-          t = getInversionNode(sc, solve_tn, m);
-          break;
-        }
-
-        case BITVECTOR_AND:
-        case BITVECTOR_OR:
-        {
-          /* with side condition:
-           * t & s = t
-           * t | s = t */
-          TypeNode solve_tn = sv_t[index].getType();
-          Node sc = getScBvAndOr(k, index, getSolveVariable(solve_tn), s, t);
-          /* t = fresh skolem constant  */
-          t = getInversionNode(sc, solve_tn, m);
-          break;
-        }
-
-        case BITVECTOR_XOR:
-          t = nm->mkNode(BITVECTOR_XOR, t, s);
-          break;
-
-        case BITVECTOR_LSHR:
-        {
-          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 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 sc = getScBvShl(k, index, getSolveVariable(solve_tn), s, t);
-          /* t = fresh skolem constant */
-          t = getInversionNode(sc, solve_tn, m);
-          break;
         }
-
-        default:
-          Trace("bv-invert") << "bv-invert : Unknown kind " << k
-                             << " for bit-vector term " << sv_t << std::endl;
-          return Node::null();
+        /* We generate a choice term (choice x0. SC => x0 <k> s <litk> t) for
+         * x <k> s <litk> t. When traversing down, this choice term determines
+         * the value for x <k> s = (choice x0. SC => x0 <k> s <litk> t), i.e.,
+         * from here on, the propagated literal is a positive equality. */
+        litk = EQUAL;
+        pol = true;
+        /* t = fresh skolem constant */
+        t = getInversionNode(sc, solve_tn, m);
       }
     }
     sv_t = sv_t[index];
   }
   Assert(sv_t == sv);
+  if (litk == BITVECTOR_ULT)
+  {
+    TypeNode solve_tn = sv_t.getType();
+    Node sc = getScBvUlt(pol, litk, index, getSolveVariable(solve_tn), t);
+    t = getInversionNode(sc, solve_tn, m);
+  }
+  else if (litk == BITVECTOR_SLT)
+  {
+    TypeNode solve_tn = sv_t.getType();
+    Node sc = getScBvSlt(pol, litk, index, getSolveVariable(solve_tn), t);
+    t = getInversionNode(sc, solve_tn, m);
+  }
+  else if (pol == false)
+  {
+    Assert (litk == EQUAL);
+    TypeNode solve_tn = sv_t.getType();
+    Node x = getSolveVariable(solve_tn);
+    Node sc = nm->mkNode(DISTINCT, x, t);
+    Trace("bv-invert") << "Add SC_" << litk << "(" << x << "): " << sc
+                       << std::endl;
+    t = getInversionNode(sc, solve_tn, m);
+  }
   return t;
 }
 
diff --git a/src/theory/quantifiers/bv_inverter.h b/src/theory/quantifiers/bv_inverter.h
index a44d64904..ce2a58695 100644
--- a/src/theory/quantifiers/bv_inverter.h
+++ b/src/theory/quantifiers/bv_inverter.h
@@ -44,47 +44,22 @@ class BvInverterQuery
   virtual Node getBoundVariable(TypeNode tn) = 0;
 };
 
-// class for storing information about the solved status
-class BvInverterStatus {
- public:
-  BvInverterStatus() : d_status(0) {}
-  ~BvInverterStatus() {}
-  int d_status;
-};
-
 // inverter class
 // TODO : move to theory/bv/ if generally useful?
-class BvInverter {
+class BvInverter
+{
  public:
   BvInverter() {}
   ~BvInverter() {}
   /** get dummy fresh variable of type tn, used as argument for sv */
   Node getSolveVariable(TypeNode tn);
 
-  /** get inversion node
-   *
-   * This expects a condition cond where:
-   *   (exists x. cond)
-   * is a BV tautology where x is getSolveVariable( tn ).
-   *
-   * It returns a term of the form:
-   *   (choice y. cond { x -> y })
-   * where y is a bound variable and x is getSolveVariable( tn ).
-   *
-   * In some cases, we may return a term t
-   * if cond implies an equality on the solve variable.
-   * For example, if cond is x = t where x is
-   * getSolveVariable( tn ), then we return t
-   * instead of introducing the choice function.
-   */
-  Node getInversionNode(Node cond, TypeNode tn, BvInverterQuery* m);
-
   /** Get path to pv in lit, replace that occurrence by sv and all others by
    * pvs. If return value R is non-null, then : lit.path = pv R.path = sv
    *   R.path' = pvs for all lit.path' = pv, where path' != path
    */
-  Node getPathToPv(Node lit, Node pv, Node sv, Node pvs,
-                   std::vector<unsigned>& path);
+  Node getPathToPv(
+      Node lit, Node pv, Node sv, Node pvs, std::vector<unsigned>& path);
 
   /** solveBvLit
    * solve for sv in lit, where lit.path = sv
@@ -93,16 +68,35 @@ class BvInverter {
   Node solveBvLit(Node sv,
                   Node lit,
                   std::vector<unsigned>& path,
-                  BvInverterQuery* m,
-                  BvInverterStatus& status);
+                  BvInverterQuery* m);
 
  private:
-  /** dummy variables for each type */
+  /** Dummy variables for each type */
   std::map<TypeNode, Node> d_solve_var;
 
-  /** helper function for getPathToPv */
-  Node getPathToPv(Node lit, Node pv, Node sv, std::vector<unsigned>& path,
+  /** Helper function for getPathToPv */
+  Node getPathToPv(Node lit,
+                   Node pv,
+                   Node sv,
+                   std::vector<unsigned>& path,
                    std::unordered_set<TNode, TNodeHashFunction>& visited);
+
+  /** Helper function for getInv.
+   *
+   * This expects a condition cond where:
+   *   (exists x. cond)
+   * is a BV tautology where x is getSolveVariable( tn ).
+   *
+   * It returns a term of the form:
+   *   (choice y. cond { x -> y })
+   * where y is a bound variable and x is getSolveVariable( tn ).
+   *
+   * In some cases, we may return a term t if cond implies an equality on
+   * the solve variable. For example, if cond is x = t where x is
+   * getSolveVariable(tn), then we return t instead of introducing the choice
+   * function.
+   */
+  Node getInversionNode(Node cond, TypeNode tn, BvInverterQuery* m);
 };
 
 }  // namespace quantifiers
diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp
index 55cc59c51..e4bc9adb8 100644
--- a/src/theory/quantifiers/ceg_t_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_t_instantiator.cpp
@@ -965,7 +965,6 @@ void BvInstantiator::reset(CegInstantiator* ci,
   d_inst_id_counter = 0;
   d_var_to_inst_id.clear();
   d_inst_id_to_term.clear();
-  d_inst_id_to_status.clear();
   d_inst_id_to_alit.clear();
   d_var_to_curr_inst_id.clear();
   d_alit_to_model_slack.clear();
@@ -979,31 +978,32 @@ void BvInstantiator::processLiteral(CegInstantiator* ci,
                                     Node alit,
                                     CegInstEffort effort)
 {
-  Assert( d_inverter!=NULL );
+  Assert(d_inverter != NULL);
   // find path to pv
-  std::vector< unsigned > path;
-  Node sv = d_inverter->getSolveVariable( pv.getType() );
-  Node pvs = ci->getModelValue( pv );
+  std::vector<unsigned> path;
+  Node sv = d_inverter->getSolveVariable(pv.getType());
+  Node pvs = ci->getModelValue(pv);
   Trace("cegqi-bv") << "Get path to pv : " << lit << std::endl;
-  Node slit = d_inverter->getPathToPv( lit, pv, sv, pvs, path );
-  if( !slit.isNull() ){
+  Node slit = d_inverter->getPathToPv(lit, pv, sv, pvs, path);
+  if (!slit.isNull())
+  {
     CegInstantiatorBvInverterQuery m(ci);
     unsigned iid = d_inst_id_counter;
     Trace("cegqi-bv") << "Solve lit to bv inverter : " << slit << std::endl;
-    Node inst =
-        d_inverter->solveBvLit(sv, slit, path, &m, d_inst_id_to_status[iid]);
-    if( !inst.isNull() ){
+    Node inst = d_inverter->solveBvLit(sv, slit, path, &m);
+    if (!inst.isNull())
+    {
       inst = Rewriter::rewrite(inst);
       Trace("cegqi-bv") << "...solved form is " << inst << std::endl;
       // store information for id and increment
-      d_var_to_inst_id[pv].push_back( iid );
+      d_var_to_inst_id[pv].push_back(iid);
       d_inst_id_to_term[iid] = inst;
       d_inst_id_to_alit[iid] = alit;
       d_inst_id_counter++;
-    }else{
+    }
+    else
+    {
       Trace("cegqi-bv") << "...failed to solve." << std::endl;
-      // cleanup information if we failed to solve
-      d_inst_id_to_status.erase( iid );
     }
   }
 }
diff --git a/src/theory/quantifiers/ceg_t_instantiator.h b/src/theory/quantifiers/ceg_t_instantiator.h
index c2864acc5..0648942e8 100644
--- a/src/theory/quantifiers/ceg_t_instantiator.h
+++ b/src/theory/quantifiers/ceg_t_instantiator.h
@@ -231,7 +231,6 @@ class BvInstantiator : public Instantiator {
   /** information about solved forms */
   std::unordered_map< Node, std::vector< unsigned >, NodeHashFunction > d_var_to_inst_id;
   std::unordered_map< unsigned, Node > d_inst_id_to_term;
-  std::unordered_map< unsigned, BvInverterStatus > d_inst_id_to_status;
   std::unordered_map<unsigned, Node> d_inst_id_to_alit;
   // variable to current id we are processing
   std::unordered_map< Node, unsigned, NodeHashFunction > d_var_to_curr_inst_id;
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index c59570651..bb43d6c1c 100644
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -90,25 +90,38 @@ TESTS =	\
 	qbv-simp.smt2 \
 	psyco-001-bv.smt2 \
 	bug822.smt2 \
-	qbv-test-invert-mul.smt2 \
+	qbv-disequality3.smt2 \
+	qbv-inequality2.smt2 \
+	qbv-simple-2vars-vo.smt2 \
+	qbv-test-invert-bvadd-neq.smt2 \
 	qbv-test-invert-bvand.smt2 \
-	qbv-test-invert-bvcomp.smt2 \
-	qbv-test-invert-bvor.smt2 \
-	qbv-test-invert-bvlshr-0.smt2 \
+	qbv-test-invert-bvand-neq.smt2 \
 	qbv-test-invert-bvashr-0.smt2 \
+	qbv-test-invert-bvashr-0-neq.smt2 \
+	qbv-test-invert-bvashr-1.smt2 \
+	qbv-test-invert-bvashr-1-neq.smt2 \
+	qbv-test-invert-bvlshr-0.smt2 \
+	qbv-test-invert-bvlshr-0-neq.smt2 \
+	qbv-test-invert-bvlshr-1.smt2 \
+	qbv-test-invert-bvlshr-1-neq.smt2 \
+	qbv-test-invert-bvmul.smt2 \
+	qbv-test-invert-bvmul-neq.smt2 \
+	qbv-test-invert-bvor.smt2 \
+	qbv-test-invert-bvor-neq.smt2 \
+	qbv-test-invert-bvshl-0.smt2 \
+	qbv-test-invert-bvudiv-0.smt2 \
+	qbv-test-invert-bvudiv-0-neq.smt2 \
+	qbv-test-invert-bvudiv-1.smt2 \
+	qbv-test-invert-bvudiv-1-neq.smt2 \
+	qbv-test-invert-bvult-1.smt2 \
  	qbv-test-invert-bvurem-1.smt2 \
+	qbv-test-invert-bvurem-1-neq.smt2 \
+	qbv-test-invert-bvxor.smt2 \
+	qbv-test-invert-bvxor-neq.smt2 \
 	qbv-test-invert-concat-0.smt2 \
 	qbv-test-invert-concat-1.smt2 \
-	qbv-test-invert-disequality.smt2 \
-	qbv-test-invert-shl.smt2 \
-	qbv-test-invert-udiv-0.smt2 \
-	qbv-test-invert-udiv-1.smt2 \
 	qbv-test-invert-sign-extend.smt2 \
-	qbv-test-invert-bvxor.smt2 \
-	qbv-simple-2vars-vo.smt2 \
 	qbv-test-urem-rewrite.smt2 \
-	qbv-inequality2.smt2 \
-	qbv-test-invert-bvult-1.smt2 \
 	intersection-example-onelane.proof-node22337.smt2 \
  	nested9_true-unreach-call.i_575.smt2 \
  	small-pipeline-fixpoint-3.smt2 \
@@ -127,6 +140,8 @@ TESTS =	\
 # regression can be solved with --finite-model-find --fmf-inst-engine
 # set3.smt2
 
+# disabled since bvcomp handling is currently disabled
+# qbv-test-invert-bvcomp.smt2
 
 # removed because they take more than 20s
 #		javafe.ast.ArrayInit.35.smt2
diff --git a/test/regress/regress0/quantifiers/qbv-disequality3.smt2 b/test/regress/regress0/quantifiers/qbv-disequality3.smt2
new file mode 100644
index 000000000..d16157509
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-disequality3.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; EXPECT: sat
+(set-logic BV)
+(set-info :status sat)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+
+(assert (forall ((x (_ BitVec 8))) (= (bvmul (bvadd x b) a)  b)))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-inequality2.smt2 b/test/regress/regress0/quantifiers/qbv-inequality2.smt2
index d53715a2d..1486e176d 100644
--- a/test/regress/regress0/quantifiers/qbv-inequality2.smt2
+++ b/test/regress/regress0/quantifiers/qbv-inequality2.smt2
@@ -1,11 +1,10 @@
-; COMMAND-LINE: --cbqi-bv
+; COMMAND-LINE: --cbqi-bv --no-cbqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
-(declare-fun a () (_ BitVec 32))
-(declare-fun b () (_ BitVec 32))
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
 
-
-(assert (forall ((x (_ BitVec 32))) (or (bvuge x (bvadd a b)) (bvule x b))))
+(assert (forall ((x (_ BitVec 8))) (or (bvuge x (bvadd a b)) (bvule x b))))
 
 (check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-multi-lit-uge.smt2 b/test/regress/regress0/quantifiers/qbv-multi-lit-uge.smt2
index d74a6cfea..3c4f93243 100644
--- a/test/regress/regress0/quantifiers/qbv-multi-lit-uge.smt2
+++ b/test/regress/regress0/quantifiers/qbv-multi-lit-uge.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv
+; COMMAND-LINE: --cbqi-bv --no-cbqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
diff --git a/test/regress/regress0/quantifiers/qbv-simp.smt2 b/test/regress/regress0/quantifiers/qbv-simp.smt2
index 1f72d44e4..ec4626f52 100644
--- a/test/regress/regress0/quantifiers/qbv-simp.smt2
+++ b/test/regress/regress0/quantifiers/qbv-simp.smt2
@@ -1,9 +1,11 @@
+; COMMAND-LINE: --cbqi-bv --no-cbqi-full
+; EXPECT: unsat
 (set-logic BV)
 (set-info :status unsat)
 (assert
    (forall
-    ((A (_ BitVec 32)) (B (_ BitVec 32)) (C (_ BitVec 32)) (D (_ BitVec 32)))
+    ((A (_ BitVec 8)) (B (_ BitVec 8)) (C (_ BitVec 8)) (D (_ BitVec 8)))
       (or (and (= A B) (= C D)) (and (= A C) (= B D)))))
-      
+
 (check-sat)
-      
+
diff --git a/test/regress/regress0/quantifiers/qbv-simple-2vars-vo.smt2 b/test/regress/regress0/quantifiers/qbv-simple-2vars-vo.smt2
index b6ae95fec..c36322aac 100644
--- a/test/regress/regress0/quantifiers/qbv-simple-2vars-vo.smt2
+++ b/test/regress/regress0/quantifiers/qbv-simple-2vars-vo.smt2
@@ -1,16 +1,16 @@
-; COMMAND-LINE: --cbqi-bv
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
-(declare-fun a () (_ BitVec 32))
-(declare-fun b () (_ BitVec 32))
-(declare-fun c () (_ BitVec 32))
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+(declare-fun c () (_ BitVec 8))
 
-(assert (not (= a #x00000000)))
+(assert (not (= a #x00)))
 
-(assert (forall ((x (_ BitVec 32)) (y (_ BitVec 32))) (or 
-(not (= (bvmul x y) #x0000000A))
-(not (= (bvadd y a) #x00000010))
+(assert (forall ((x (_ BitVec 8)) (y (_ BitVec 8))) (or 
+(not (= (bvmul x y) #x0A))
+(not (= (bvadd y a) #x10))
 )))
 
 (check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvadd-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvadd-neq.smt2
new file mode 100644
index 000000000..216a98531
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvadd-neq.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; EXPECT: unsat
+(set-logic BV)
+(set-info :status unsat)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+
+(assert (forall ((x (_ BitVec 8))) (= (bvadd x a) b)))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvand-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvand-neq.smt2
new file mode 100644
index 000000000..ad3b9a9e5
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvand-neq.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; EXPECT: sat
+(set-logic BV)
+(set-info :status sat)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+
+(assert (forall ((x (_ BitVec 8))) (= (bvand x a) b)))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2
index d611fcd68..8dd50b1be 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2
@@ -1,10 +1,10 @@
-; COMMAND-LINE: --cbqi-bv
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
-(declare-fun a () (_ BitVec 32))
-(declare-fun b () (_ BitVec 32))
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
 
-(assert (forall ((x (_ BitVec 32))) (not (= (bvand x a) b))))
+(assert (forall ((x (_ BitVec 8))) (not (= (bvand x a) b))))
 
 (check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0-neq.smt2
new file mode 100644
index 000000000..e05c3446d
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0-neq.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; EXPECT: unsat
+(set-logic BV)
+(set-info :status unsat)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+
+(assert (forall ((x (_ BitVec 8))) (= (bvashr x a) b)))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0.smt2
index db7725896..30e7c2f8b 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0.smt2
@@ -1,10 +1,10 @@
-; COMMAND-LINE: --cbqi-bv
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
-(declare-fun a () (_ BitVec 32))
-(declare-fun b () (_ BitVec 32))
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
 
-(assert (forall ((x (_ BitVec 32))) (not (= (bvashr x a) b))))
+(assert (forall ((x (_ BitVec 8))) (not (= (bvashr x a) b))))
 
 (check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-1-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-1-neq.smt2
new file mode 100644
index 000000000..2835e5956
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-1-neq.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; EXPECT: sat
+(set-logic BV)
+(set-info :status sat)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+
+(assert (forall ((x (_ BitVec 8))) (= (bvashr a x) b)))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-1.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-1.smt2
new file mode 100644
index 000000000..c3de64c4c
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-1.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; EXPECT: sat
+(set-logic BV)
+(set-info :status sat)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+
+(assert (forall ((x (_ BitVec 8))) (not (= (bvashr a x) b))))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvcomp.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvcomp.smt2
index e8f7c25db..3b55c0b9a 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-bvcomp.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvcomp.smt2
@@ -1,11 +1,11 @@
-; COMMAND-LINE: --cbqi-bv
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
 ; EXPECT: unsat
 (set-logic BV)
 (set-info :status sat)
-(declare-fun a () (_ BitVec 32))
-(declare-fun b () (_ BitVec 32))
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
 (declare-fun c () (_ BitVec 1))
 
-(assert (forall ((x (_ BitVec 32))) (not (= (bvcomp x a) (bvcomp x b)))))
+(assert (forall ((x (_ BitVec 8))) (not (= (bvcomp x a) ((_ extract 7 7) (bvmul a b))))))
 
 (check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0-neq.smt2
new file mode 100644
index 000000000..e05c3446d
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0-neq.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; EXPECT: unsat
+(set-logic BV)
+(set-info :status unsat)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+
+(assert (forall ((x (_ BitVec 8))) (= (bvashr x a) b)))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2
index db7725896..1018ce72c 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2
@@ -1,10 +1,10 @@
-; COMMAND-LINE: --cbqi-bv
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
-(declare-fun a () (_ BitVec 32))
-(declare-fun b () (_ BitVec 32))
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
 
-(assert (forall ((x (_ BitVec 32))) (not (= (bvashr x a) b))))
+(assert (forall ((x (_ BitVec 8))) (not (= (bvlshr x a) b))))
 
 (check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-1-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-1-neq.smt2
new file mode 100644
index 000000000..503bc9852
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-1-neq.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; EXPECT: sat
+(set-logic BV)
+(set-info :status sat)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+
+(assert (forall ((x (_ BitVec 8))) (= (bvlshr a x) b)))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-1.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-1.smt2
new file mode 100644
index 000000000..08479d90e
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-1.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; EXPECT: sat
+(set-logic BV)
+(set-info :status sat)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+
+(assert (forall ((x (_ BitVec 8))) (not (= (bvlshr a x) b))))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvmul-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvmul-neq.smt2
new file mode 100644
index 000000000..9dc9f98ac
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvmul-neq.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; EXPECT: sat
+(set-logic BV)
+(set-info :status sat)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+
+(assert (forall ((x (_ BitVec 8))) (= (bvmul x a) b)))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvmul.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvmul.smt2
new file mode 100644
index 000000000..f3dad679b
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvmul.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; EXPECT: sat
+(set-logic BV)
+(set-info :status sat)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+
+(assert (forall ((x (_ BitVec 8))) (not (= (bvmul x a) b))))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvor-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvor-neq.smt2
new file mode 100644
index 000000000..74c2891cf
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvor-neq.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; EXPECT: sat
+(set-logic BV)
+(set-info :status sat)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+
+(assert (forall ((x (_ BitVec 8))) (= (bvor x a) b)))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvor.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvor.smt2
index 287da08c7..4145c68b1 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-bvor.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvor.smt2
@@ -1,10 +1,10 @@
-; COMMAND-LINE: --cbqi-bv
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
-(declare-fun a () (_ BitVec 32))
-(declare-fun b () (_ BitVec 32))
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
 
-(assert (forall ((x (_ BitVec 32))) (not (= (bvor x a) b))))
+(assert (forall ((x (_ BitVec 8))) (not (= (bvor x a) b))))
 
 (check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0-neq.smt2
new file mode 100644
index 000000000..e85ecc7de
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0-neq.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; EXPECT: sat
+(set-logic BV)
+(set-info :status sat)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+
+(assert (forall ((x (_ BitVec 8))) (= (bvshl x a) b)))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0.smt2
new file mode 100644
index 000000000..abef84da2
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; EXPECT: sat
+(set-logic BV)
+(set-info :status sat)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+
+(assert (forall ((x (_ BitVec 8))) (not (= (bvshl x a) b))))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-0-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-0-neq.smt2
new file mode 100644
index 000000000..3748eca24
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-0-neq.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; EXPECT: unsat
+(set-logic BV)
+(set-info :status unsat)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+
+(assert (distinct a b (_ bv0 8)))
+(assert (forall ((x (_ BitVec 8))) (= (bvudiv x a) b)))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-0.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-0.smt2
new file mode 100644
index 000000000..2cabb502e
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-0.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; EXPECT: sat
+(set-logic BV)
+(set-info :status sat)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+
+(assert (distinct a b (_ bv0 8)))
+(assert (forall ((x (_ BitVec 8))) (not (= (bvudiv x a) b))))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-1-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-1-neq.smt2
new file mode 100644
index 000000000..a0e1b62c2
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-1-neq.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full --bv-div-zero-const
+; EXPECT: unsat
+(set-logic BV)
+(set-info :status unsat)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+
+(assert (distinct a b (_ bv0 8)))
+(assert (forall ((x (_ BitVec 8))) (= (bvudiv a x) b)))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-udiv-1.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-1.smt2
index bf69a8b4a..2690a0ac9 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-udiv-1.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv --bv-div-zero-const
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full --bv-div-zero-const
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvult-1.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvult-1.smt2
index 13c1bf10a..a1dca469a 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-bvult-1.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvult-1.smt2
@@ -1,9 +1,9 @@
-; COMMAND-LINE: --cbqi-bv
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
-(declare-fun a () (_ BitVec 32))
+(declare-fun a () (_ BitVec 8))
 
-(assert (forall ((x (_ BitVec 32))) (not (bvult a x))))
+(assert (forall ((x (_ BitVec 8))) (not (bvult a x))))
 
 (check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1-neq.smt2
new file mode 100644
index 000000000..871df4827
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1-neq.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; EXPECT: sat
+(set-logic BV)
+(set-info :status sat)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+
+(assert (forall ((x (_ BitVec 8))) (= (bvurem a x) b)))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1.smt2
index f7fe54e3e..22bd306ee 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1.smt2
@@ -1,10 +1,10 @@
-; COMMAND-LINE: --cbqi-bv --bv-div-zero-const
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
-(declare-fun a () (_ BitVec 32))
-(declare-fun b () (_ BitVec 32))
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
 
-(assert (forall ((x (_ BitVec 32))) (not (= (bvurem a x) b))))
+(assert (forall ((x (_ BitVec 8))) (not (= (bvurem a x) b))))
 
 (check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvxor-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvxor-neq.smt2
new file mode 100644
index 000000000..4f9c6edc3
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvxor-neq.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; EXPECT: unsat
+(set-logic BV)
+(set-info :status unsat)
+(declare-fun a () (_ BitVec 8))
+
+(assert (forall ((x (_ BitVec 8))) (not (= (bvxor x a) (bvmul a a)))))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvxor.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvxor.smt2
index eec40a425..ef41eecdd 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-bvxor.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvxor.smt2
@@ -1,9 +1,9 @@
-; COMMAND-LINE: --cbqi-bv
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
 ; EXPECT: unsat
 (set-logic BV)
 (set-info :status sat)
-(declare-fun a () (_ BitVec 32))
+(declare-fun a () (_ BitVec 8))
 
-(assert (forall ((x (_ BitVec 32))) (not (= (bvxor x a) (bvmul a a)))))
+(assert (forall ((x (_ BitVec 8))) (not (= (bvxor x a) (bvmul a a)))))
 
 (check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-concat-0-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-concat-0-neq.smt2
new file mode 100644
index 000000000..769854f6f
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-concat-0-neq.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; EXPECT: unsat
+(set-logic BV)
+(set-info :status unsat)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 16))
+
+(assert (forall ((x (_ BitVec 8))) (= (concat x a) b)))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-concat-0.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-concat-0.smt2
index f4e19fc52..7b66bd859 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-concat-0.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-concat-0.smt2
@@ -1,10 +1,10 @@
-; COMMAND-LINE: --cbqi-bv
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
-(declare-fun a () (_ BitVec 32))
-(declare-fun b () (_ BitVec 64))
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 16))
 
-(assert (forall ((x (_ BitVec 32))) (not (= (concat x a) b))))
+(assert (forall ((x (_ BitVec 8))) (not (= (concat x a) b))))
 
 (check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-concat-1-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-concat-1-neq.smt2
new file mode 100644
index 000000000..7dab5637e
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-concat-1-neq.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; EXPECT: unsat
+(set-logic BV)
+(set-info :status unsat)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 16))
+
+(assert (forall ((x (_ BitVec 8))) (= (concat a x) b)))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-concat-1.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-concat-1.smt2
index 827e74605..13fb3e1c2 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-concat-1.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-concat-1.smt2
@@ -1,10 +1,10 @@
-; COMMAND-LINE: --cbqi-bv
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
-(declare-fun a () (_ BitVec 32))
-(declare-fun b () (_ BitVec 64))
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 16))
 
-(assert (forall ((x (_ BitVec 32))) (not (= (concat a x) b))))
+(assert (forall ((x (_ BitVec 8))) (not (= (concat a x) b))))
 
 (check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-disequality.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-disequality.smt2
deleted file mode 100644
index 6ba782597..000000000
--- a/test/regress/regress0/quantifiers/qbv-test-invert-disequality.smt2
+++ /dev/null
@@ -1,10 +0,0 @@
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep
-; EXPECT: sat
-(set-logic BV)
-(set-info :status sat)
-(declare-fun a () (_ BitVec 32))
-(declare-fun b () (_ BitVec 32))
-
-(assert (forall ((x (_ BitVec 32))) (= (bvand x a) b)))
-
-(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-mul.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-mul.smt2
deleted file mode 100644
index 84e9fa7ce..000000000
--- a/test/regress/regress0/quantifiers/qbv-test-invert-mul.smt2
+++ /dev/null
@@ -1,10 +0,0 @@
-; COMMAND-LINE: --cbqi-bv
-; EXPECT: sat
-(set-logic BV)
-(set-info :status sat)
-(declare-fun a () (_ BitVec 32))
-(declare-fun b () (_ BitVec 32))
-
-(assert (forall ((x (_ BitVec 32))) (not (= (bvmul x a) b))))
-
-(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-shl.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-shl.smt2
deleted file mode 100644
index 97a0662eb..000000000
--- a/test/regress/regress0/quantifiers/qbv-test-invert-shl.smt2
+++ /dev/null
@@ -1,10 +0,0 @@
-; COMMAND-LINE: --cbqi-bv
-; EXPECT: sat
-(set-logic BV)
-(set-info :status sat)
-(declare-fun a () (_ BitVec 32))
-(declare-fun b () (_ BitVec 32))
-
-(assert (forall ((x (_ BitVec 32))) (not (= (bvshl x a) b))))
-
-(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-sign-extend.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-sign-extend.smt2
index 21aa519ad..43019c4cb 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-sign-extend.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-sign-extend.smt2
@@ -1,10 +1,10 @@
-; COMMAND-LINE: --cbqi-bv
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
-(declare-fun a () (_ BitVec 32))
-(declare-fun b () (_ BitVec 64))
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 16))
 
-(assert (forall ((x (_ BitVec 32))) (not (= ((_ sign_extend 32) x) b))))
+(assert (forall ((x (_ BitVec 8))) (not (= ((_ sign_extend 8) x) b))))
 
 (check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-udiv-0.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-udiv-0.smt2
deleted file mode 100644
index becfc5315..000000000
--- a/test/regress/regress0/quantifiers/qbv-test-invert-udiv-0.smt2
+++ /dev/null
@@ -1,11 +0,0 @@
-; COMMAND-LINE: --cbqi-bv --bv-div-zero-const
-; EXPECT: sat
-(set-logic BV)
-(set-info :status sat)
-(declare-fun a () (_ BitVec 16))
-(declare-fun b () (_ BitVec 16))
-
-(assert (distinct a b (_ bv0 16)))
-(assert (forall ((x (_ BitVec 16))) (not (= (bvudiv x a) b))))
-
-(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-urem-rewrite.smt2 b/test/regress/regress0/quantifiers/qbv-test-urem-rewrite.smt2
index 6df69d80b..e57352b8f 100644
--- a/test/regress/regress0/quantifiers/qbv-test-urem-rewrite.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-urem-rewrite.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv --bv-div-zero-const
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
diff --git a/test/unit/theory/theory_quantifiers_bv_inverter_white.h b/test/unit/theory/theory_quantifiers_bv_inverter_white.h
index ce01c17e4..5e1d404dc 100644
--- a/test/unit/theory/theory_quantifiers_bv_inverter_white.h
+++ b/test/unit/theory/theory_quantifiers_bv_inverter_white.h
@@ -23,6 +23,7 @@
 #include "util/result.h"
 
 using namespace CVC4;
+using namespace CVC4::kind;
 using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 using namespace CVC4::smt;
@@ -45,58 +46,63 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite
                    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);
+    Assert(k == BITVECTOR_ULT || k == BITVECTOR_SLT || k == EQUAL);
+    Assert(k != 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();
+    TS_ASSERT((k == BITVECTOR_ULT && pol == false)
+           || (k == BITVECTOR_SLT && pol == false)
+           || ksc == IMPLIES);
+    Node scl = ksc == 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);
+      k = k == BITVECTOR_ULT
+        ? BITVECTOR_UGE
+        : (k == BITVECTOR_SLT ? BITVECTOR_SGE : 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();
+    Node scr = d_nm->mkNode(EXISTS, d_bvarlist, body);
+    Expr a = d_nm->mkNode(DISTINCT, scl, scr).toExpr();
     Result res = d_smt->checkSat(a);
     TS_ASSERT(res.d_sat == Result::UNSAT);
   }
 
-  void runTest(Kind k,
+  void runTest(bool pol,
+               Kind litk,
+               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);
-
-    Node sc = getsc(k, idx, d_sk, d_s, d_t);
+               Node (*getsc)(bool, Kind, Kind, unsigned, Node, Node, Node))
+  {
+    Assert(k == BITVECTOR_MULT
+           || k == BITVECTOR_UREM_TOTAL
+           || k == BITVECTOR_UDIV_TOTAL
+           || k == BITVECTOR_AND
+           || k == BITVECTOR_OR
+           || k == BITVECTOR_LSHR
+           || k == BITVECTOR_ASHR
+           || k == BITVECTOR_SHL);
+    Assert(k != BITVECTOR_UREM_TOTAL || pol == false || idx == 1);
+
+    Node sc = getsc(pol, litk, k, idx, d_sk, d_s, d_t);
+    TS_ASSERT (litk != EQUAL || sc != Node::null());
     Kind ksc = sc.getKind();
-    TS_ASSERT(ksc == kind::IMPLIES);
+    TS_ASSERT((k == BITVECTOR_UDIV_TOTAL && idx == 1 && pol == false)
+              || (k == BITVECTOR_ASHR && idx == 0 && pol == false)
+              || ksc == IMPLIES);
+    Node scl = ksc == IMPLIES ? sc[0] : bv::utils::mkTrue();
     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();
+      ? d_nm->mkNode(pol ? EQUAL : DISTINCT, d_nm->mkNode(k, d_x, d_s), d_t)
+      : d_nm->mkNode(pol ? EQUAL : DISTINCT, d_nm->mkNode(k, d_s, d_x), d_t);
+    Node scr = d_nm->mkNode(EXISTS, d_bvarlist, body);
+    Expr a = d_nm->mkNode(DISTINCT, scl, scr).toExpr();
     Result res = d_smt->checkSat(a);
     if (res.d_sat == Result::SAT)
     {
-      std::cout << std::endl << "s " << d_smt->getValue(d_s.toExpr()) << std::endl;
+      std::cout << std::endl;
+      std::cout << "s " << d_smt->getValue(d_s.toExpr()) << std::endl;
       std::cout << "t " << d_smt->getValue(d_t.toExpr()) << std::endl;
       std::cout << "x " << d_smt->getValue(d_x.toExpr()) << std::endl;
     }
@@ -119,7 +125,7 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite
     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 });
+    d_bvarlist = d_nm->mkNode(BOUND_VAR_LIST, { d_x });
   }
 
   void tearDown()
@@ -174,99 +180,163 @@ class TheoryQuantifiersBvInverter : public CxxTest::TestSuite
     runTestPred(false, BITVECTOR_SLT, 1, getScBvSlt);
   }
 
-  void testGetScBvEq0()
+  void testGetScBvMultEqTrue0()
   {
-    runTestPred(false, EQUAL, 0, getScBvEq);
-    TS_ASSERT_THROWS(runTestPred(true, EQUAL, 0, getScBvEq),
-                     AssertionException);
+    runTest(true, EQUAL, BITVECTOR_MULT, 0, getScBvMult);
   }
 
-  void testGetScBvEq1()
+  void testGetScBvMultEqTrue1()
   {
-    runTestPred(false, EQUAL, 1, getScBvEq);
-    TS_ASSERT_THROWS(runTestPred(true, EQUAL, 1, getScBvEq),
-                     AssertionException);
+    runTest(true, EQUAL, BITVECTOR_MULT, 1, getScBvMult);
   }
 
-  void testGetScBvMult0()
+  void testGetScBvMultEqFalse0()
   {
-    runTest(BITVECTOR_MULT, 0, getScBvMult);
+    runTest(false, EQUAL, BITVECTOR_MULT, 0, getScBvMult);
   }
 
-  void testGetScBvMult1()
+  void testGetScBvMultEqFalse1()
   {
-    runTest(BITVECTOR_MULT, 1, getScBvMult);
+    runTest(false, EQUAL, BITVECTOR_MULT, 1, getScBvMult);
   }
 
-  void testGetScBvUrem0()
+  void testGetScBvUremEqTrue0()
   {
-    TS_ASSERT_THROWS(runTest(BITVECTOR_UREM_TOTAL, 0, getScBvUrem),
+    TS_ASSERT_THROWS(runTest(true, EQUAL, BITVECTOR_UREM_TOTAL, 0, getScBvUrem),
                      AssertionException);
   }
 
-  void testGetScBvUrem1()
+  void testGetScBvUremEqTrue1()
+  {
+    runTest(true, EQUAL, BITVECTOR_UREM_TOTAL, 1, getScBvUrem);
+  }
+
+  void testGetScBvUremEqFalse0()
+  {
+    runTest(false, EQUAL, BITVECTOR_UREM_TOTAL, 0, getScBvUrem);
+  }
+
+  void testGetScBvUremEqFalse1()
+  {
+    runTest(false, EQUAL, BITVECTOR_UREM_TOTAL, 1, getScBvUrem);
+  }
+  void testGetScBvUdivEqTrue0()
+  {
+    runTest(true, EQUAL, BITVECTOR_UDIV_TOTAL, 0, getScBvUdiv);
+  }
+
+  void testGetScBvUdivEqTrue1()
+  {
+    runTest(true, EQUAL, BITVECTOR_UDIV_TOTAL, 1, getScBvUdiv);
+  }
+
+  void testGetScBvUdivFalse0()
   {
-    runTest(BITVECTOR_UREM_TOTAL, 1, getScBvUrem);
+    runTest(false, EQUAL, BITVECTOR_UDIV_TOTAL, 0, getScBvUdiv);
   }
 
-  void testGetScBvUdiv0()
+  void testGetScBvUdivFalse1()
   {
-    runTest(BITVECTOR_UDIV_TOTAL, 0, getScBvUdiv);
+    runTest(false, EQUAL, BITVECTOR_UDIV_TOTAL, 1, getScBvUdiv);
   }
 
-  void testGetScBvUdiv1()
+  void testGetScBvAndEqTrue0()
   {
-    runTest(BITVECTOR_UDIV_TOTAL, 1, getScBvUdiv);
+    runTest(true, EQUAL, BITVECTOR_AND, 0, getScBvAndOr);
   }
 
-  void testGetScBvAnd0()
+  void testGetScBvAndEqTrue1()
   {
-    runTest(BITVECTOR_AND, 0, getScBvAndOr);
+    runTest(true, EQUAL, BITVECTOR_AND, 1, getScBvAndOr);
   }
 
-  void testGetScBvAnd1()
+  void testGetScBvAndEqFalse0()
   {
-    runTest(BITVECTOR_AND, 1, getScBvAndOr);
+    runTest(false, EQUAL, BITVECTOR_AND, 0, getScBvAndOr);
   }
 
-  void testGetScBvOr0()
+  void testGetScBvAndEqFalse1()
   {
-    runTest(BITVECTOR_OR, 0, getScBvAndOr);
+    runTest(false, EQUAL, BITVECTOR_AND, 1, getScBvAndOr);
   }
 
-  void testGetScBvOr1()
+  void testGetScBvOrEqTrue0()
   {
-    runTest(BITVECTOR_OR, 1, getScBvAndOr);
+    runTest(true, EQUAL, BITVECTOR_OR, 0, getScBvAndOr);
   }
 
-  void testGetScBvLshr0()
+  void testGetScBvOrEqTrue1()
   {
-    runTest(BITVECTOR_LSHR, 0, getScBvLshr);
+    runTest(true, EQUAL, BITVECTOR_OR, 1, getScBvAndOr);
   }
 
-  void testGetScBvLshr1()
+  void testGetScBvOrEqFalse0()
   {
-    runTest(BITVECTOR_LSHR, 1, getScBvLshr);
+    runTest(false, EQUAL, BITVECTOR_OR, 0, getScBvAndOr);
   }
 
-  void testGetScBvAshr0()
+  void testGetScBvOrEqFalse1()
   {
-    runTest(BITVECTOR_ASHR, 0, getScBvAshr);
+    runTest(false, EQUAL, BITVECTOR_OR, 1, getScBvAndOr);
   }
 
-  void testGetScBvAshr1()
+  void testGetScBvLshrEqTrue0()
   {
-    runTest(BITVECTOR_ASHR, 1, getScBvAshr);
+    runTest(true, EQUAL, BITVECTOR_LSHR, 0, getScBvLshr);
   }
 
-  void testGetScBvShl0()
+  void testGetScBvLshrEqTrue1()
   {
-    runTest(BITVECTOR_SHL, 0, getScBvShl);
+    runTest(true, EQUAL, BITVECTOR_LSHR, 1, getScBvLshr);
   }
 
-  void testGetScBvShl1()
+  void testGetScBvLshrEqFalse0()
   {
-    runTest(BITVECTOR_SHL, 1, getScBvShl);
+    runTest(false, EQUAL, BITVECTOR_LSHR, 0, getScBvLshr);
   }
 
+  void testGetScBvLshrEqFalse1()
+  {
+    runTest(false, EQUAL, BITVECTOR_LSHR, 1, getScBvLshr);
+  }
+
+  void testGetScBvAshrEqTrue0()
+  {
+    runTest(true, EQUAL, BITVECTOR_ASHR, 0, getScBvAshr);
+  }
+
+  void testGetScBvAshrEqTrue1()
+  {
+    runTest(true, EQUAL, BITVECTOR_ASHR, 1, getScBvAshr);
+  }
+
+  void testGetScBvAshrEqFalse0()
+  {
+    runTest(false, EQUAL, BITVECTOR_ASHR, 0, getScBvAshr);
+  }
+
+  void testGetScBvAshrEqFalse1()
+  {
+    runTest(false, EQUAL, BITVECTOR_ASHR, 1, getScBvAshr);
+  }
+
+  void testGetScBvShlEqTrue0()
+  {
+    runTest(true, EQUAL, BITVECTOR_SHL, 0, getScBvShl);
+  }
+
+  void testGetScBvShlEqTrue1()
+  {
+    runTest(true, EQUAL, BITVECTOR_SHL, 1, getScBvShl);
+  }
+
+  void testGetScBvShlEqFalse0()
+  {
+    runTest(false, EQUAL, BITVECTOR_SHL, 0, getScBvShl);
+  }
+
+  void testGetScBvShlEqFalse1()
+  {
+    runTest(false, EQUAL, BITVECTOR_SHL, 1, getScBvShl);
+  }
 };