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.

1 files changed, 634 insertions, 438 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;
 }