Add UGT/SGT side conditions for AND/OR + other fixes. (#1481)

1 files changed, 349 insertions, 206 deletions

diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp
index 2bc93de60..7f2343df7 100644
--- a/src/theory/quantifiers/bv_inverter.cpp
+++ b/src/theory/quantifiers/bv_inverter.cpp
@@ -220,7 +220,8 @@ static Node getScBvUltUgt(bool pol, Kind k, Node x, Node t)
       /* x < t
        * with side condition:
        * (distinct t z)
-       * where z = 0 with getSize(z) = w  */
+       * where
+       * z = 0 with getSize(z) = w  */
       Node scl = nm->mkNode(DISTINCT, t, bv::utils::mkZero(w));
       Node scr = nm->mkNode(k, x, t);
       sc = nm->mkNode(IMPLIES, scl, scr);
@@ -240,7 +241,8 @@ static Node getScBvUltUgt(bool pol, Kind k, Node x, Node t)
       /* x > t
        * with side condition:
        * (distinct t ones)
-       * where ones = ~0 with getSize(ones) = w  */
+       * where
+       * ones = ~0 with getSize(ones) = w  */
       Node scl = nm->mkNode(DISTINCT, t, bv::utils::mkOnes(w));
       Node scr = nm->mkNode(k, x, t);
       sc = nm->mkNode(IMPLIES, scl, scr);
@@ -248,7 +250,7 @@ static Node getScBvUltUgt(bool pol, Kind k, Node x, Node t)
     else
     {
       /* x <= t
-       * true (no side condition) */
+       * true (no side condition)  */
       sc = nm->mkNode(NOT, nm->mkNode(k, x, t));
     }
   }
@@ -271,7 +273,8 @@ static Node getScBvSltSgt(bool pol, Kind k, Node x, Node t)
       /* x < t
        * with side condition:
        * (distinct t min)
-       * where min is the minimum signed value with getSize(min) = w  */
+       * where
+       * min is the minimum signed value with getSize(min) = w  */
       Node min = bv::utils::mkConst(BitVector(w).setBit(w - 1));
       Node scl = nm->mkNode(DISTINCT, min, t);
       Node scr = nm->mkNode(k, x, t);
@@ -280,7 +283,7 @@ static Node getScBvSltSgt(bool pol, Kind k, Node x, Node t)
     else
     {
       /* x >= t
-       * true (no side condition) */
+       * true (no side condition)  */
       sc = nm->mkNode(NOT, nm->mkNode(k, x, t));
     }
   }
@@ -292,7 +295,8 @@ static Node getScBvSltSgt(bool pol, Kind k, Node x, Node t)
       /* x > t
        * with side condition:
        * (distinct t max)
-       * where max is the maximum signed value with getSize(max) = w  */
+       * where
+       * max is the signed maximum value with getSize(max) = w  */
       BitVector bv = BitVector(w).setBit(w - 1);
       Node max = bv::utils::mkConst(~bv);
       Node scl = nm->mkNode(DISTINCT, t, max);
@@ -302,7 +306,7 @@ static Node getScBvSltSgt(bool pol, Kind k, Node x, Node t)
     else
     {
       /* x <= t
-       * true (no side condition) */
+       * true (no side condition)  */
       sc = nm->mkNode(NOT, nm->mkNode(k, x, t));
     }
   }
@@ -346,7 +350,8 @@ static Node getScBvMult(bool pol,
        *   (and
        *     (bvuge (bvand t (bvneg t)) (bvand s (bvneg s)))
        *     (distinct s z)))
-       * where z = 0 with getSize(z) = w  */
+       * where
+       * z = 0 with getSize(z) = w  */
       Node o = nm->mkNode(BITVECTOR_OR, nm->mkNode(BITVECTOR_NEG, s), s);
       scl = nm->mkNode(EQUAL, nm->mkNode(BITVECTOR_AND, o, t), t);
     }
@@ -355,7 +360,8 @@ static Node getScBvMult(bool pol,
       /* x * s != t
        * with side condition:
        * (or (distinct t z) (distinct s z))
-       * where z = 0 with getSize(z) = w  */
+       * where
+       * z = 0 with getSize(z) = w  */
       scl = nm->mkNode(OR, t.eqNode(z).notNode(), s.eqNode(z).notNode());
     }
   }
@@ -366,7 +372,8 @@ static Node getScBvMult(bool pol,
       /* x * s < t
        * with side condition (synthesized):
        * (distinct t z)
-       * where z = 0 with getSize(z) = w  */
+       * where
+       * z = 0 with getSize(z) = w  */
       Node z = bv::utils::mkZero(w);
       scl =  nm->mkNode(DISTINCT, t, z);
     }
@@ -374,7 +381,7 @@ static Node getScBvMult(bool pol,
     {
       /* x * s >= t
        * with side condition (synthesized):
-       * (not (bvult (bvor (bvneg s) s) t))  */
+       * (bvuge (bvor (bvneg s) s) t)  */
       Node o = nm->mkNode(BITVECTOR_OR, nm->mkNode(BITVECTOR_NEG, s), s);
       scl = nm->mkNode(BITVECTOR_UGE, o, t);
     }
@@ -392,7 +399,7 @@ static Node getScBvMult(bool pol,
     else
     {
       /* x * s <= t
-       * true (no side condition) */
+       * true (no side condition)  */
       scl = nm->mkConst<bool>(true);
     }
   }
@@ -411,8 +418,9 @@ static Node getScBvMult(bool pol,
     {
       /* x * s >= t
        * with side condition (synthesized):
-       * (bvsge (bvand (bvor (bvneg s) s) max) t))
-       * where max is the maximum signed value with getSize(max) = w  */
+       * (bvsge (bvand (bvor (bvneg s) s) max) t)
+       * where
+       * max is the signed maximum value with getSize(max) = w  */
       BitVector bv = BitVector(w).setBit(w - 1);
       Node max = bv::utils::mkConst(~bv);
       Node o = nm->mkNode(BITVECTOR_OR, nm->mkNode(BITVECTOR_NEG, s), s);
@@ -420,7 +428,7 @@ static Node getScBvMult(bool pol,
       scl = nm->mkNode(BITVECTOR_SGE, a, t);
     }
   }
-  else  /* litk == BITVECTOR_SGT  */
+  else  /* litk == BITVECTOR_SGT */
   {
     if (pol)
     {
@@ -437,7 +445,8 @@ static Node getScBvMult(bool pol,
       /* x * s <= t
        * with side condition (synthesized):
        * (not (and (= s z) (bvslt t s)))
-       * where z = 0 with getSize(z) = w  */
+       * where
+       * z = 0 with getSize(z) = w  */
       Node z = bv::utils::mkZero(w);
       scl = nm->mkNode(AND, s.eqNode(z), nm->mkNode(BITVECTOR_SLT, t, s));
       scl = scl.notNode();
@@ -477,7 +486,7 @@ static Node getScBvUrem(bool pol,
       {
         /* x % s = t
          * with side condition (synthesized):
-         * (not (bvult (bvnot (bvneg s)) t))  */
+         * (bvuge (bvnot (bvneg s)) t)  */
         Node neg = nm->mkNode(BITVECTOR_NEG, s);
         scl = nm->mkNode(BITVECTOR_UGE, nm->mkNode(BITVECTOR_NOT, neg), t);
       }
@@ -486,7 +495,8 @@ static Node getScBvUrem(bool pol,
         /* x % s != t
          * with side condition:
          * (or (distinct s (_ bv1 w)) (distinct t z))
-         * where z = 0 with getSize(z) = w  */
+         * where
+         * z = 0 with getSize(z) = w  */
         Node z = bv::utils::mkZero(w);
         scl = nm->mkNode(OR,
             s.eqNode(bv::utils::mkOne(w)).notNode(),
@@ -506,7 +516,8 @@ static Node getScBvUrem(bool pol,
          *     (and (bvugt s t)
          *          (bvugt (bvsub s t) t)
          *          (or (= t z) (distinct (bvsub s (_ bv1 w)) t))))
-         * where z = 0 with getSize(z) = w  */
+         * where
+         * z = 0 with getSize(z) = w  */
         Node add = nm->mkNode(BITVECTOR_PLUS, t, t);
         Node sub = nm->mkNode(BITVECTOR_SUB, add, s);
         Node a = nm->mkNode(BITVECTOR_AND, sub, s);
@@ -517,7 +528,8 @@ static Node getScBvUrem(bool pol,
         /* s % x != t
          * with side condition:
          * (or (distinct s z) (distinct t z))
-         * where z = 0 with getSize(z) = w  */
+         * where
+         * z = 0 with getSize(z) = w  */
         Node z = bv::utils::mkZero(w);
         scl = nm->mkNode(OR, s.eqNode(z).notNode(), t.eqNode(z).notNode());
       }
@@ -532,7 +544,8 @@ static Node getScBvUrem(bool pol,
         /* x % s < t
          * with side condition:
          * (distinct t z)
-         * where z = 0 with getSize(z) = w  */
+         * where
+         * z = 0 with getSize(z) = w  */
         Node z = bv::utils::mkZero(w);
         scl = t.eqNode(z).notNode();
       }
@@ -552,7 +565,8 @@ static Node getScBvUrem(bool pol,
         /* s % x < t
          * with side condition:
          * (distinct t z)
-         * where z = 0 with getSize(z) = w  */
+         * where
+         * z = 0 with getSize(z) = w  */
         Node z = bv::utils::mkZero(w);
         scl = t.eqNode(z).notNode();
       }
@@ -587,7 +601,7 @@ static Node getScBvUrem(bool pol,
       else
       {
         /* x % s <= t
-         * true (no side condition) */
+         * true (no side condition)  */
         scl = nm->mkConst<bool>(true);
       }
     }
@@ -603,7 +617,7 @@ static Node getScBvUrem(bool pol,
       else
       {
         /* s % x <= t
-         * true (no side condition) */
+         * true (no side condition)  */
         scl = nm->mkConst<bool>(true);
       }
     }
@@ -627,7 +641,8 @@ static Node getScBvUrem(bool pol,
         /* x % s >= t
          * with side condition (synthesized):
          * (or (bvslt t s) (bvsge z s))
-         * where z = 0 with getSize(z) = w  */
+         * where
+         * z = 0 with getSize(z) = w  */
         Node z = bv::utils::mkZero(w);
         Node s1 = nm->mkNode(BITVECTOR_SLT, t, s);
         Node s2 = nm->mkNode(BITVECTOR_SGE, z, s);
@@ -643,7 +658,8 @@ static Node getScBvUrem(bool pol,
         /* s % x < t
          * with side condition (synthesized):
          * (or (bvslt s t) (bvslt z t))
-         * where z = 0 with getSize(z) = w  */
+         * where
+         * z = 0 with getSize(z) = w  */
         Node slt1 = nm->mkNode(BITVECTOR_SLT, s, t);
         Node slt2 = nm->mkNode(BITVECTOR_SLT, z, t);
         scl = nm->mkNode(OR, slt1, slt2);
@@ -655,7 +671,8 @@ static Node getScBvUrem(bool pol,
          * (and
          *   (=> (bvsge s z) (bvsge s t))
          *   (=> (and (bvslt s z) (bvsge t z)) (bvugt (bvsub s t) t)))
-         * where z = 0 with getSize(z) = w  */
+         * where
+         * z = 0 with getSize(z) = w  */
         Node i1 = nm->mkNode(IMPLIES,
             nm->mkNode(BITVECTOR_SGE, s, z), nm->mkNode(BITVECTOR_SGE, s, t));
         Node i2 = nm->mkNode(IMPLIES,
@@ -682,7 +699,8 @@ static Node getScBvUrem(bool pol,
          *     (=> (bvsgt s z) (bvslt t (bvnot (bvneg s))))
          *     (=> (bvsle s z) (distinct t max)))
          *   (or (distinct t z) (distinct s (_ bv1 w))))
-         * where z = 0 with getSize(z) = w
+         * where
+         * z = 0 with getSize(z) = w
          * and max is the maximum signed value with getSize(max) = w  */
         BitVector bv_ones = utils::mkBitVectorOnes(w - 1);
         BitVector bv_max = BitVector(1).concat(bv_ones);
@@ -701,23 +719,26 @@ static Node getScBvUrem(bool pol,
       {
         /* x % s <= t
          * with side condition (synthesized):
-         * (bvslt (bvnot z) (bvand (bvneg s) t))
-         * where z = 0 with getSize(z) = w  */
+         * (bvslt ones (bvand (bvneg s) t))
+         * where
+         * z = 0 with getSize(z) = w
+         * and ones = ~0 with getSize(ones) = w  */
         Node a = nm->mkNode(BITVECTOR_AND, nm->mkNode(BITVECTOR_NEG, s), t);
-        scl = nm->mkNode(BITVECTOR_SLT, nm->mkNode(BITVECTOR_NOT, z), a);
+        scl = nm->mkNode(BITVECTOR_SLT, bv::utils::mkOnes(w), a);
       }
     }
     else
     {
       if (pol)
       {
-        /* s % x >= t
+        /* s % x > t
          * with side condition:
          * (and
          *   (=> (bvsge s z) (bvsgt s t))
          *   (=> (bvslt s z)
          *    (bvsgt (bvlshr (bvsub s (_ bv1 w)) (_ bv1 w)) t)))
-         * where z = 0 with getSize(z) = w  */
+         * where
+         * z = 0 with getSize(z) = w  */
         Node z = bv::utils::mkZero(w);
         Node i1 = nm->mkNode(IMPLIES,
             nm->mkNode(BITVECTOR_SGE, s, z), nm->mkNode(BITVECTOR_SGT, s, t));
@@ -729,10 +750,11 @@ static Node getScBvUrem(bool pol,
       }
       else
       {
-        /* s % x < t
+        /* s % x <= t
          * with side condition (synthesized):
          * (or (bvult t min) (bvsge t s))
-         * where min is the minimum signed value with getSize(min) = w  */
+         * where
+         * min is the minimum signed value with getSize(min) = w  */
         BitVector bv_min = BitVector(w).setBit(w - 1);
         Node min = bv::utils::mkConst(bv_min);
         Node o1 = nm->mkNode(BITVECTOR_ULT, t, min);
@@ -786,7 +808,8 @@ static Node getScBvUdiv(bool pol,
          *        (distinct s z)
          *        (not (umulo s t))))
          *
-         * where umulo(s, t) is true if s * t produces and overflow
+         * where
+         * umulo(s, t) is true if s * t produces and overflow
          * and z = 0 with getSize(z) = w  */
         Node mul = nm->mkNode(BITVECTOR_MULT, s, t);
         Node div = nm->mkNode(BITVECTOR_UDIV_TOTAL, mul, s);
@@ -797,7 +820,8 @@ static Node getScBvUdiv(bool pol,
         /* x udiv s != t
          * with side condition:
          * (or (distinct s z) (distinct t ones))
-         * where z = 0 with getSize(z) = w
+         * where
+         * z = 0 with getSize(z) = w
          * and ones = ~0 with getSize(ones) = w  */
         Node ones = bv::utils::mkOnes(w);
         scl = nm->mkNode(OR, s.eqNode(z).notNode(), t.eqNode(ones).notNode());
@@ -823,14 +847,15 @@ static Node getScBvUdiv(bool pol,
          *              (bvudiv s t)))
          *     (=> (= s (bvnot (_ bv0 8))) (distinct t (_ bv0 8)))))
          *
-         * where z = 0 with getSize(z) = w  */
+         * where
+         * z = 0 with getSize(z) = w  */
         Node div = nm->mkNode(BITVECTOR_UDIV_TOTAL, s, t);
         scl = nm->mkNode(EQUAL, nm->mkNode(BITVECTOR_UDIV_TOTAL, s, div), t);
       }
       else
       {
         /* s udiv x != t
-         * true (no side condition) */
+         * true (no side condition)  */
         scl = nm->mkConst<bool>(true);
       }
     }
@@ -844,7 +869,8 @@ static Node getScBvUdiv(bool pol,
         /* x udiv s < t
          * with side condition (synthesized):
          * (and (bvult z s) (bvult z t))
-         * where z = 0 with getSize(z) = w  */
+         * where
+         * z = 0 with getSize(z) = w  */
         Node u1 = nm->mkNode(BITVECTOR_ULT, z, s);
         Node u2 = nm->mkNode(BITVECTOR_ULT, z, t);
         scl = nm->mkNode(AND, u1, u2);
@@ -866,7 +892,8 @@ static Node getScBvUdiv(bool pol,
         /* s udiv x < t
          * with side condition (synthesized):
          * (and (bvult z (bvnot (bvand (bvneg t) s))) (bvult z t))
-         * where z = 0 with getSize(z) = w  */
+         * where
+         * z = 0 with getSize(z) = w  */
         Node a = nm->mkNode(BITVECTOR_AND, nm->mkNode(BITVECTOR_NEG, t), s);
         Node u1 = nm->mkNode(BITVECTOR_ULT, z, nm->mkNode(BITVECTOR_NOT, a));
         Node u2 = nm->mkNode(BITVECTOR_ULT, z, t);
@@ -875,7 +902,7 @@ static Node getScBvUdiv(bool pol,
       else
       {
         /* s udiv x >= t
-         * true (no side condition) */
+         * true (no side condition)  */
         scl = nm->mkConst<bool>(true);
       }
     }
@@ -889,7 +916,8 @@ static Node getScBvUdiv(bool pol,
         /* x udiv s > t
          * with side condition:
          * (bvugt (bvudiv ones s) t)
-         * where ones = ~0 with getSize(ones) = w  */
+         * where
+         * ones = ~0 with getSize(ones) = w  */
         Node ones = bv::utils::mkOnes(w);
         Node div = nm->mkNode(BITVECTOR_UDIV_TOTAL, ones, s);
         scl = nm->mkNode(BITVECTOR_UGT, div, t);
@@ -898,7 +926,7 @@ static Node getScBvUdiv(bool pol,
       {
         /* x udiv s <= t
          * with side condition (synthesized):
-         * (not (bvult (bvor s t) (bvnot (bvneg s))))  */
+         * (bvuge (bvor s t) (bvnot (bvneg s)))  */
         Node u1 = nm->mkNode(BITVECTOR_OR, s, t);
         Node u2 = nm->mkNode(BITVECTOR_NOT, nm->mkNode(BITVECTOR_NEG, s));
         scl = nm->mkNode(BITVECTOR_UGE, u1, u2);
@@ -911,7 +939,8 @@ static Node getScBvUdiv(bool pol,
         /* s udiv x > t
          * with side condition (synthesized):
          * (bvult t ones)
-         * where ones = ~0 with getSize(ones) = w  */
+         * where
+         * ones = ~0 with getSize(ones) = w  */
         Node ones = bv::utils::mkOnes(w);
         scl = nm->mkNode(BITVECTOR_ULT, t, ones);
       }
@@ -920,7 +949,8 @@ static Node getScBvUdiv(bool pol,
         /* s udiv x <= t
          * with side condition (synthesized):
          * (bvult z (bvor (bvnot s) t))
-         * where z = 0 with getSize(z) = w  */
+         * where
+         * z = 0 with getSize(z) = w  */
         scl = nm->mkNode(BITVECTOR_ULT,
             z, nm->mkNode(BITVECTOR_OR, nm->mkNode(BITVECTOR_NOT, s), t));
       }
@@ -935,7 +965,8 @@ static Node getScBvUdiv(bool pol,
         /* x udiv s < t
          * with side condition:
          * (=> (bvsle t z) (bvslt (bvudiv min s) t))
-         * where z = 0 with getSize(z) = w
+         * where
+         * z = 0 with getSize(z) = w
          * and min is the minimum signed value with getSize(min) = w  */
         BitVector bv_min = BitVector(w).setBit(w - 1);
         Node min = bv::utils::mkConst(bv_min);
@@ -951,7 +982,8 @@ static Node getScBvUdiv(bool pol,
          * (or
          *   (bvsge (bvudiv ones s) t)
          *   (bvsge (bvudiv max s) t))
-         * where ones = ~0 with getSize(ones) = w
+         * where
+         * ones = ~0 with getSize(ones) = w
          * and max is the maximum signed value with getSize(max) = w  */
         BitVector bv_ones = utils::mkBitVectorOnes(w - 1);
         BitVector bv_max = BitVector(1).concat(bv_ones);
@@ -971,7 +1003,8 @@ static Node getScBvUdiv(bool pol,
         /* s udiv x < t
          * with side condition (synthesized):
          * (or (bvslt s t) (bvsge t z))
-         * where z = 0 with getSize(z) = w  */
+         * where
+         * z = 0 with getSize(z) = w  */
         Node slt = nm->mkNode(BITVECTOR_SLT, s, t);
         Node sge = nm->mkNode(BITVECTOR_SGE, t, z);
         scl = nm->mkNode(OR, slt, sge);
@@ -983,7 +1016,8 @@ static Node getScBvUdiv(bool pol,
          * (and
          *   (=> (bvsge s z) (bvsge s t))
          *   (=> (bvslt s z) (bvsge (bvudiv s (_ bv2 w)) t)))
-         * where z = 0 with getSize(z) = w  */
+         * where
+         * z = 0 with getSize(z) = w  */
         Node div = nm->mkNode(BITVECTOR_UDIV_TOTAL,
             s, bv::utils::mkConst(w, 2));
         Node i1 = nm->mkNode(IMPLIES,
@@ -994,7 +1028,7 @@ static Node getScBvUdiv(bool pol,
       }
     }
   }
-  else  /* litk == BITVECTOR_SGT  */
+  else  /* litk == BITVECTOR_SGT */
   {
     if (idx == 0)
     {
@@ -1005,7 +1039,8 @@ static Node getScBvUdiv(bool pol,
          * (or
          *   (bvsgt (bvudiv ones s) t)
          *   (bvsgt (bvudiv max s) t))
-         * where ones = ~0 with getSize(ones) = w
+         * where
+         * ones = ~0 with getSize(ones) = w
          * and max is the maximum signed value with getSize(max) = w  */
         BitVector bv_ones = utils::mkBitVectorOnes(w - 1);
         BitVector bv_max = BitVector(1).concat(bv_ones);
@@ -1024,7 +1059,8 @@ static Node getScBvUdiv(bool pol,
          * (or
          *   (= (bvudiv (bvmul s t) s) t)                ; eq, synthesized
          *   (=> (bvsle t z) (bvslt (bvudiv min s) t)))  ; slt
-         * where z = 0 with getSize(z) = w
+         * where
+         * z = 0 with getSize(z) = w
          * and min is the minimum signed value with getSize(min) = w  */
         Node mul = nm->mkNode(BITVECTOR_MULT, s, t);
         Node div1 = nm->mkNode(BITVECTOR_UDIV_TOTAL, mul, s);
@@ -1047,7 +1083,8 @@ static Node getScBvUdiv(bool pol,
          * (and
          *   (=> (bvsge s z) (bvsgt s t))
          *   (=> (bvslt s z) (bvsgt (bvudiv s (_ bv2 w)) t)))
-         * where z = 0 with getSize(z) = w  */
+         * where
+         * z = 0 with getSize(z) = w  */
         Node div = nm->mkNode(BITVECTOR_UDIV_TOTAL,
             s, bv::utils::mkConst(w, 2));
         Node i1 = nm->mkNode(IMPLIES,
@@ -1063,7 +1100,8 @@ static Node getScBvUdiv(bool pol,
          * (not (and (bvslt t (bvnot #x0)) (bvslt t s)))
          * <->
          * (or (bvsge t ones) (bvsge t s))
-         * where ones = ~0 with getSize(ones) = w  */
+         * where
+         * ones = ~0 with getSize(ones) = w  */
         Node ones = bv::utils::mkOnes(w);
         Node sge1 = nm->mkNode(BITVECTOR_SGE, t, ones);
         Node sge2 = nm->mkNode(BITVECTOR_SGE, t, s);
@@ -1092,6 +1130,8 @@ static Node getScBvAndOr(bool pol,
           || litk == BITVECTOR_UGT || litk == BITVECTOR_SGT);
 
   NodeManager* nm = NodeManager::currentNM();
+  unsigned w = bv::utils::getSize(s);
+  Assert (w == bv::utils::getSize(t));
   Node scl;
 
   if (litk == EQUAL)
@@ -1101,20 +1141,19 @@ static Node getScBvAndOr(bool pol,
       /* x & s = t
        * x | s = t
        * with side condition:
-       * t & s = t
-       * t | s = t */
+       * (= (bvand t s) t)
+       * (= (bvor t s) t)  */
       scl = nm->mkNode(EQUAL, t, nm->mkNode(k, t, s));
     }
     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  */
+         * (or (distinct s z) (distinct t z))
+         * where
+         * z = 0 with getSize(z) = w  */
         Node z = bv::utils::mkZero(w);
         scl = nm->mkNode(OR, s.eqNode(z).notNode(), t.eqNode(z).notNode());
       }
@@ -1122,7 +1161,9 @@ static Node getScBvAndOr(bool pol,
       {
         /* x | s = t
          * with side condition:
-         * s != ~0 || t != ~0  */
+         * (or (distinct s ones) (distinct t ones))
+         * where
+         * ones = ~0 with getSize(ones) = w  */
         Node n = bv::utils::mkOnes(w);
         scl = nm->mkNode(OR, s.eqNode(n).notNode(), t.eqNode(n).notNode());
       }
@@ -1136,36 +1177,77 @@ static Node getScBvAndOr(bool pol,
       {
         /* x & s < t
          * with side condition (synthesized):
-         * t != 0 */
-        Node z = bv::utils::mkZero(bv::utils::getSize(t));
+         * (distinct t z)
+         * where
+         * z = 0 with getSize(z) = 0  */
+        Node z = bv::utils::mkZero(w);
         scl = t.eqNode(z).notNode();
       }
       else
       {
         /* x | s < t
          * with side condition (synthesized):
-         * (bvult s t) */
+         * (bvult s t)  */
         scl = nm->mkNode(BITVECTOR_ULT, s, t);
       }
     }
-    else  /* litk == BITVECTOR_SLT  */
+    else
     {
       if (k == BITVECTOR_AND)
       {
         /* x & s >= t
          * with side condition (synthesized):
-         * (not (bvult s t)) */
+         * (bvuge s t)  */
         scl = nm->mkNode(BITVECTOR_UGE, s, t);
       }
       else
       {
         /* x | s >= t
          * with side condition (synthesized):
-         * true (no side condition) */
+         * true (no side condition)  */
         scl = nm->mkConst<bool>(true);
       }
     }
   }
+  else if (litk == BITVECTOR_UGT)
+  {
+    if (pol)
+    {
+      if (k == BITVECTOR_AND)
+      {
+        /* x & s > t
+         * with side condition (synthesized):
+         * (bvult t s)  */
+        scl = nm->mkNode(BITVECTOR_ULT, t, s);
+      }
+      else
+      {
+        /* x | s > t
+         * with side condition (synthesized):
+         * (bvult t ones)
+         * where
+         * ones = ~0 with getSize(ones) = w  */
+        scl = nm->mkNode(BITVECTOR_ULT, t, bv::utils::mkOnes(w));
+      }
+    }
+    else
+    {
+      if (k == BITVECTOR_AND)
+      {
+        /* x & s <= t
+         * with side condition (synthesized):
+         * true (no side condition)  */
+        scl = nm->mkConst<bool>(true);
+      }
+      else
+      {
+        /* x | s <= t
+         * with side condition (synthesized):
+         * (bvuge t s)  */
+        scl = nm->mkNode(BITVECTOR_UGE, t, s);
+      }
+    }
+  }
   else if (litk == BITVECTOR_SLT)
   {
     if (pol)
@@ -1174,7 +1256,7 @@ static Node getScBvAndOr(bool pol,
       {
         /* x & s < t
          * with side condition (synthesized):
-         * (bvslt (bvand (bvnot (bvneg t)) s) t) */
+         * (bvslt (bvand (bvnot (bvneg t)) s) t)  */
         Node nnt = nm->mkNode(BITVECTOR_NOT, nm->mkNode(BITVECTOR_NEG, t));
         scl = nm->mkNode(BITVECTOR_SLT, nm->mkNode(BITVECTOR_AND, nnt, s), t);
       }
@@ -1182,7 +1264,7 @@ static Node getScBvAndOr(bool pol,
       {
         /* x | s < t
          * with side condition (synthesized):
-         * (bvslt (bvor (bvnot (bvsub s t)) s) t) */
+         * (bvslt (bvor (bvnot (bvsub s t)) s) t)  */
         Node st = nm->mkNode(BITVECTOR_NOT, nm->mkNode(BITVECTOR_SUB, s, t));
         scl = nm->mkNode(BITVECTOR_SLT, nm->mkNode(BITVECTOR_OR, st, s), t);
       }
@@ -1195,8 +1277,7 @@ static Node getScBvAndOr(bool pol,
          * with side condition (case = combined with synthesized bvsgt):
          * (or
          *  (= (bvand s t) t)
-         *  (bvslt t (bvand (bvsub t s) s))
-         * ) */
+         *  (bvslt t (bvand (bvsub t s) s)))  */
         Node sc_sgt = nm->mkNode(
             BITVECTOR_SLT,
             t,
@@ -1208,14 +1289,53 @@ static Node getScBvAndOr(bool pol,
       {
         /* x | s >= t
          * with side condition (synthesized):
-         * (not (bvslt s (bvand s t))) */
+         * (bvsge s (bvand s t))  */
         scl = nm->mkNode(BITVECTOR_SGE, s, nm->mkNode(BITVECTOR_AND, s, t));
       }
     }
   }
   else
   {
-    return Node::null();
+    Assert(litk == BITVECTOR_SGT);
+    if (pol)
+    {
+      /* x & s > t
+       * x | s > t
+       * with side condition (synthesized):
+       * (bvslt t (bvand s max))
+       * (bvslt t (bvor s max))
+       * where
+       * max is the signed maximum value with getSize(max) = w  */
+      BitVector bv_ones = bv::utils::mkBitVectorOnes(w - 1);
+      BitVector bv_max_val = BitVector(1).concat(bv_ones);
+      Node max = bv::utils::mkConst(bv_max_val);
+      scl = nm->mkNode(BITVECTOR_SLT, t, nm->mkNode(k, s, max));
+    }
+    else
+    {
+      if (k == BITVECTOR_AND)
+      {
+        /* x & s <= t
+         * with side condition (synthesized):
+         * (bvuge s (bvand t min))
+         * where
+         * min is the signed minimum value with getSize(min) = w  */
+        BitVector bv_min_val = BitVector(w).setBit(w - 1);
+        Node min = bv::utils::mkConst(bv_min_val);
+        scl = nm->mkNode(BITVECTOR_UGE, s, nm->mkNode(BITVECTOR_AND, t, min));
+      }
+      else
+      {
+        /* x | s <= t
+         * with side condition (synthesized):
+         * (bvsge t (bvor s min))
+         * where
+         * min is the signed minimum value with getSize(min) = w  */
+        BitVector bv_min_val = BitVector(w).setBit(w - 1);
+        Node min = bv::utils::mkConst(bv_min_val);
+        scl = nm->mkNode(BITVECTOR_SGE, t, nm->mkNode(BITVECTOR_OR, s, min));
+      }
+    }
   }
   Node scr = nm->mkNode(litk, nm->mkNode(k, x, s), t);
   Node sc = nm->mkNode(IMPLIES, scl, pol ? scr : scr.notNode());
@@ -1253,9 +1373,12 @@ static Node getScBvLshr(bool pol,
          * 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)
+         * (or
+         *  (= s z)
+         *  (and
+         *   (bvult s w)
+         *   (= ((_ extract 2*w-1 w) (bvshl (concat z t) (concat z s))) z))
+         *  (and (bvuge s w) (= t z)))
          * with w = getSize(t) = getSize(s)
          * and z = 0 with getSize(z) = w  */
         Node z_o_t = nm->mkNode(BITVECTOR_CONCAT, z, t);
@@ -1275,10 +1398,10 @@ static Node getScBvLshr(bool pol,
       {
         /* x >> s != t
          * with side condition:
-         * t != 0 || s < w
-         * with
-         * w = getSize(s) = getSize(t)
-         */
+         * (or (distinct t z) (bvult s w))
+         * where
+         * z = 0 with getSize(z) = w
+         * and w = getSize(s) = getSize(t)  */
         scl = nm->mkNode(OR,
             t.eqNode(z).notNode(),
             nm->mkNode(BITVECTOR_ULT, s, ww));
@@ -1290,14 +1413,16 @@ static Node getScBvLshr(bool 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
+         * (or
+         *  (= t z)
+         *  (= s t)
+         *  (and
+         *   (= ((_ extract w-1-i 0) t) ((_ extract w-1 i) s))
+         *   (= ((_ extract w-1 w-i) t) z_i)))
+         * for 0 < i < w
          * where
          * w = getSize(s) = getSize(t)
-         */
+         * and z_i = 0 with getSize(z_i) = i  */
         NodeBuilder<> nb(nm, OR);
         nb << nm->mkNode(EQUAL, t, s);
         for (unsigned i = 1; i < w; ++i)
@@ -1317,7 +1442,9 @@ static Node getScBvLshr(bool pol,
       {
         /* s >> x != t
          * with side condition:
-         * s != 0 || t != 0  */
+         * (or (distinct s z) (distinct t z))
+         * where
+         * z = 0 with getSize(z) = w  */
         scl = nm->mkNode(OR, s.eqNode(z).notNode(), t.eqNode(z).notNode());
       }
     }
@@ -1330,32 +1457,36 @@ static Node getScBvLshr(bool pol,
       {
         /* x >> s < t
          * with side condition (synthesized):
-         * (not (= z t)) */
+         * (distinct t z)
+         * where
+         * z = 0 with getSize(z) = w  */
         scl = t.eqNode(z).notNode();
       }
       else
       {
         /* x >> s >= t
          * with side condition (synthesized):
-         * (= (bvlshr (bvshl t s) s) t) */
+         * (= (bvlshr (bvshl t s) s) t)  */
         Node ts = nm->mkNode(BITVECTOR_SHL, t, s);
         scl = nm->mkNode(BITVECTOR_LSHR, ts, s).eqNode(t);
       }
     }
-    else  /* litk == BITVECTOR_SLT  */
+    else
     {
       if (pol)
       {
         /* s >> x < t
          * with side condition (synthesized):
-         * (not (= z t)) */
+         * (distinct t z)
+         * where
+         * z = 0 with getSize(z) = w  */
         scl = t.eqNode(z).notNode();
       }
       else
       {
         /* s >> x >= t
          * with side condition (synthesized):
-         * (bvuge s t) */
+         * (bvuge s t)  */
         scl = nm->mkNode(BITVECTOR_UGE, s, t);
       }
     }
@@ -1368,7 +1499,7 @@ static Node getScBvLshr(bool pol,
       {
         /* x >> s > t
          * with side condition (synthesized):
-         * (bvult t (bvlshr (bvnot s) s)) */
+         * (bvult t (bvlshr (bvnot s) s))  */
         Node lshr = nm->mkNode(BITVECTOR_LSHR, nm->mkNode(BITVECTOR_NOT, s), s);
         scl = nm->mkNode(BITVECTOR_ULT, t, lshr);
       }
@@ -1376,7 +1507,7 @@ static Node getScBvLshr(bool pol,
       {
         /* x >> s <= t
          * with side condition:
-         * true (no side condition) */
+         * true (no side condition)  */
         scl = nm->mkConst<bool>(true);
       }
     }
@@ -1386,15 +1517,14 @@ static Node getScBvLshr(bool pol,
       {
         /* s >> x > t
          * with side condition (synthesized):
-         * (bvult t s)
-         */
+         * (bvult t s)  */
         scl = nm->mkNode(BITVECTOR_ULT, t, s);
       }
       else
       {
         /* s >> x <= t
          * with side condition:
-         * true (no side condition) */
+         * true (no side condition)  */
         scl = nm->mkConst<bool>(true);
       }
     }
@@ -1407,7 +1537,7 @@ static Node getScBvLshr(bool pol,
       {
         /* x >> s < t
          * with side condition (synthesized):
-         * (bvslt (bvlshr (bvnot (bvneg t)) s) t) */
+         * (bvslt (bvlshr (bvnot (bvneg t)) s) t)  */
         Node nnt = nm->mkNode(BITVECTOR_NOT, nm->mkNode(BITVECTOR_NEG, t));
         Node lshr = nm->mkNode(BITVECTOR_LSHR, nnt, s);
         scl = nm->mkNode(BITVECTOR_SLT, lshr, t);
@@ -1417,7 +1547,9 @@ static Node getScBvLshr(bool pol,
         /* x >> s >= t
          * with side condition:
          * (=> (not (= s z)) (bvsge (bvlshr ones s) t))
-         * where ones = ~0 with getSize(ones) = w  */
+         * where
+         * z = 0 with getSize(z) = w
+         * and ones = ~0 with getSize(ones) = w  */
         Node ones = bv::utils::mkOnes(w);
         Node lshr = nm->mkNode(BITVECTOR_LSHR, ones, s);
         Node nz = s.eqNode(z).notNode();
@@ -1430,7 +1562,9 @@ static Node getScBvLshr(bool pol,
       {
         /* s >> x < t
          * with side condition (synthesized):
-         * (or (bvslt s t) (bvslt z t)) */
+         * (or (bvslt s t) (bvslt z t))
+         * where
+         * z = 0 with getSize(z) = w  */
         Node st = nm->mkNode(BITVECTOR_SLT, s, t);
         Node zt = nm->mkNode(BITVECTOR_SLT, z, t);
         scl = st.orNode(zt);
@@ -1440,9 +1574,10 @@ static Node getScBvLshr(bool pol,
         /* s >> x >= t
          * with side condition:
          * (and
-         *  (=> (bvslt s z) (bvsge (bvlshr s one) t))
-         *  (=> (bvsge s z) (bvsge s t))
-         * ) */
+         *  (=> (bvslt s z) (bvsge (bvlshr s (_ bv1 w)) t))
+         *  (=> (bvsge s z) (bvsge s t)))
+         * where
+         * z = 0 with getSize(z) = w  */
         Node one = bv::utils::mkConst(w, 1);
         Node sz = nm->mkNode(BITVECTOR_SLT, s, z);
         Node lshr = nm->mkNode(BITVECTOR_LSHR, s, one);
@@ -1475,7 +1610,7 @@ static Node getScBvLshr(bool pol,
       {
         /* x >> s <= t
          * with side condition (synthesized):
-         * (bvsge t (bvlshr t s)) */
+         * (bvsge t (bvlshr t s))  */
         scl = nm->mkNode(BITVECTOR_SGE, t, nm->mkNode(BITVECTOR_LSHR, t, s));
       }
     }
@@ -1486,8 +1621,10 @@ static Node getScBvLshr(bool pol,
         /* s >> x > t
          * with side condition:
          * (and
-         *  (=> (bvslt s z) (bvsgt (bvlshr s one)) t))
-         *  (=> (bvsge s z) (bvsgt s t))) */
+         *  (=> (bvslt s z) (bvsgt (bvlshr s one) t))
+         *  (=> (bvsge s z) (bvsgt s t)))
+         * where
+         * z = 0 and getSize(z) = w  */
         Node one = bv::utils::mkOne(w);
         Node sz = nm->mkNode(BITVECTOR_SLT, s, z);
         Node lshr = nm->mkNode(BITVECTOR_LSHR, s, one);
@@ -1544,16 +1681,19 @@ static Node getScBvAshr(bool 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  */
-
+         * (or
+         *  (= s z)
+         *  (and
+         *   (bvult s w)
+         *   (or
+         *    (= ((_ extract 2*w-1 w-1) (bvshl (concat z t) (concat z s))) z)
+         *    (= ((_ extract 2*w-1 w-1)
+         *        (bvshl (concat ones t) (concat z s))) ones)))
+         *  (and (bvuge s w) (or (= t z) (= t ones))))
+         * where
+         * z = 0 with getSize(z) = w
+         * and ones = ~0 with getSize(ones) = w
+         * and w = getSize(t) = getSize(s)  */
         Node zz = bv::utils::mkZero(w+1);
         Node nn = bv::utils::mkOnes(w+1);
         Node ww = bv::utils::mkConst(w, w);
@@ -1580,30 +1720,35 @@ static Node getScBvAshr(bool pol,
       else
       {
         /* x >> s != t
-         * true (no side condition) */
+         * true (no side condition)  */
         scl = nm->mkConst<bool>(true);
       }
     }
-    else  /* litk == BITVECTOR_SLT  */
+    else
     {
       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)))
+         * (or
+         *  (and (= ((_ extract w-1 w-1) s) (_ bv0 1)) (= t z))
+         *  (and (= ((_ extract w-1 w-1) s) (_ bv0 1)) (= t ones))
+         *  (= s t)
+         *  (and
+         *   (= ((_ extract w-1-i 0) t) ((_ extract w-1 i) s))
+         *   (or
+         *    (and
+         *     (= ((_ extract w-1 w-1) s) (_ bv0 1))
+         *     (= ((_ extract w-1 w-i) t) (_ bv0 i)))
+         *    (and
+         *     (= ((_ extract w-1 w-1) s) (_ bv1 1))
+         *     (= ((_ extract w-1 w-i) t) ones_i)))))
          * for 0 < i < w
          * where
-         * w = getSize(s) = getSize(t)
-         */
+         * z = 0 and getSize(z) = w
+         * and ones = ~0 and getSize(ones) = w
+         * and ones_i = ~0 and getSize(ones_i) = i
+         * and 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(
@@ -1634,8 +1779,10 @@ static Node getScBvAshr(bool pol,
          * with side condition:
          * (and
          *  (or (not (= t z)) (not (= s z)))
-         *  (or (not (= t (bvnot z)) (not (= s (bvnot z))))))
-         */
+         *  (or (not (= t ones)) (not (= s ones))))
+         * where
+         * z = 0 with getSize(z) = w
+         * and ones = ~0 with getSize(ones) = w  */
         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()));
@@ -1650,14 +1797,16 @@ static Node getScBvAshr(bool pol,
       {
         /* x >> s < t
          * with side condition (synthesized):
-         * (not (= t z)) */
+         * (distinct t z)
+         * where
+         * z = 0 with getSize(z) = w  */
         scl = t.eqNode(z).notNode();
       }
       else
       {
         /* x >> s >= t
          * with side condition (synthesized):
-         * true (no side condition) */
+         * true (no side condition)  */
         scl = nm->mkConst<bool>(true);
       }
     }
@@ -1667,7 +1816,9 @@ static Node getScBvAshr(bool pol,
       {
         /* s >> x < t
          * with side condition (synthesized):
-         * (and (not (and (not (bvult s t)) (bvslt s z))) (not (= t z))) */
+         * (and (not (and (bvuge s t) (bvslt s z))) (not (= t z)))
+         * where
+         * z = 0 with getSize(z) = w  */
         Node st = nm->mkNode(BITVECTOR_UGE, s, t);
         Node sz = nm->mkNode(BITVECTOR_SLT, s, z);
         Node tz = t.eqNode(z).notNode();
@@ -1675,9 +1826,9 @@ static Node getScBvAshr(bool pol,
       }
       else
       {
-        /* s >> x < t
+        /* s >> x >= t
          * with side condition (synthesized):
-         * (not (and (bvult s (bvnot s)) (bvult s t))) */
+         * (not (and (bvult s (bvnot s)) (bvult s t)))  */
         Node ss = nm->mkNode(BITVECTOR_ULT, s, nm->mkNode(BITVECTOR_NOT, s));
         Node st = nm->mkNode(BITVECTOR_ULT, s, t);
         scl = ss.andNode(st).notNode();
@@ -1692,16 +1843,16 @@ static Node getScBvAshr(bool pol,
       {
         /* x >> s > t
          * with side condition (synthesized):
-         * (bvult t (bvnot #x0))
-         */
+         * (bvult t ones)
+         * where
+         * ones = ~0 with getSize(ones) = w  */
         scl = nm->mkNode(BITVECTOR_ULT, t, bv::utils::mkOnes(w));
       }
       else
       {
         /* x >> s <= t
          * with side condition (synthesized):
-         * true (no side condition)
-         */
+         * true (no side condition)  */
         scl = nm->mkConst<bool>(true);
       }
     }
@@ -1711,8 +1862,7 @@ static Node getScBvAshr(bool pol,
       {
         /* s >> x > t
          * with side condition (synthesized):
-         * (or (bvslt s (bvlshr s (bvnot t))) (bvult t s))
-         */
+         * (or (bvslt s (bvlshr s (bvnot t))) (bvult t s))  */
         Node lshr = nm->mkNode(BITVECTOR_LSHR, s, nm->mkNode(BITVECTOR_NOT, t));
         Node ts = nm->mkNode(BITVECTOR_ULT, t, s);
         Node slt = nm->mkNode(BITVECTOR_SLT, s, lshr);
@@ -1754,7 +1904,7 @@ static Node getScBvAshr(bool pol,
          * with side condition:
          * (bvsge (bvlshr max s) t)
          * where
-         * max is the signed maximum value with getSize(max) = w */
+         * max is the signed maximum value with getSize(max) = w  */
         BitVector bv_ones = bv::utils::mkBitVectorOnes(w - 1);
         BitVector bv_max_val = BitVector(1).concat(bv_ones);
         Node max = bv::utils::mkConst(bv_max_val);
@@ -1767,7 +1917,9 @@ static Node getScBvAshr(bool pol,
       {
         /* s >> x < t
          * with side condition (synthesized):
-         * (or (bvslt s t) (bvslt z t)) */
+         * (or (bvslt s t) (bvslt z t))
+         * where
+         * z = 0 and getSize(z) = w  */
         Node st = nm->mkNode(BITVECTOR_SLT, s, t);
         Node zt = nm->mkNode(BITVECTOR_SLT, z, t);
         scl = st.orNode(zt);
@@ -1776,7 +1928,7 @@ static Node getScBvAshr(bool pol,
       {
         /* s >> x >= t
          * with side condition (synthesized):
-         * (not (and (bvult t (bvnot t)) (bvslt s t))) */
+         * (not (and (bvult t (bvnot t)) (bvslt s t)))  */
         Node tt = nm->mkNode(BITVECTOR_ULT, t, nm->mkNode(BITVECTOR_NOT, t));
         Node st = nm->mkNode(BITVECTOR_SLT, s, t);
         scl = tt.andNode(st).notNode();
@@ -1807,7 +1959,7 @@ static Node getScBvAshr(bool pol,
          * with side condition (synthesized):
          * (bvsge t (bvnot (bvlshr max s)))
          * where
-         * max is the signed maximum value with getSize(max) = w */
+         * max is the signed maximum value with getSize(max) = w  */
         scl = nm->mkNode(BITVECTOR_SGE, t, nm->mkNode(BITVECTOR_NOT, lshr));
       }
     }
@@ -1830,9 +1982,9 @@ static Node getScBvAshr(bool pol,
       {
         /* s >> x <= t
          * with side condition (synthesized):
-         * (not (and (bvslt t z) (bvslt t s)))
          * (or (bvsge t z) (bvsge t s))
-         */
+         * where
+         * z = 0 and getSize(z) = w  */
         Node tz = nm->mkNode(BITVECTOR_SGE, t, z);
         Node ts = nm->mkNode(BITVECTOR_SGE, t, s);
         scl = tz.orNode(ts);
@@ -1898,15 +2050,15 @@ static Node getScBvShl(bool pol,
          * 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)
+         * (or
+         *  (= s z)
+         *  (and
+         *   (bvult s w)
+         *   (= ((_ extract w-1 0) (bvlshr (concat t z) (concat z s))) z))
+         *  (and (bvuge s w) (= t z)))
          *
          * where
-         * w = getSize(s) = getSize(t) = getSize (z) && z = 0
-         */
+         * w = getSize(s) = getSize(t) = getSize(z) and z = 0  */
         Node shr = nm->mkNode(BITVECTOR_LSHR,
             bv::utils::mkConcat(t, z),
             bv::utils::mkConcat(z, s));
@@ -1924,10 +2076,10 @@ static Node getScBvShl(bool pol,
       {
         /* x << s != t
          * with side condition:
-         * t != 0 || s < w
+         * (or (distinct t z) (bvult s w))
          * with
          * w = getSize(s) = getSize(t)
-         */
+         * and z = 0 with getSize(z) = w  */
         scl = nm->mkNode(OR,
             t.eqNode(z).notNode(),
             nm->mkNode(BITVECTOR_ULT, s, ww));
@@ -1939,14 +2091,17 @@ static Node getScBvShl(bool 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
+         * (or
+         *  (= t z)
+         *  (= s z)
+         *  (and
+         *   (= ((_ extract w-1 i) t) ((_ extract w-1-i 0)))
+         *   (= ((_ extract i-1 0) t) z_i)))
+         * for 0 < i < w
          * where
          * w = getSize(s) = getSize(t)
-         */
+         * and z = 0 with getSize(z) = w
+         * and z_i = 0 with getSize(z_i) = i  */
         NodeBuilder<> nb(nm, OR);
         nb << nm->mkNode(EQUAL, t, s);
         for (unsigned i = 1; i < w; ++i)
@@ -1964,7 +2119,9 @@ static Node getScBvShl(bool pol,
       {
         /* s << x != t
          * with side condition:
-         * s != 0 || t != 0  */
+         * (or (distinct s z) (distinct t z))
+         * where
+         * z = 0 with getSize(z) = w  */
         scl = nm->mkNode(OR, s.eqNode(z).notNode(), t.eqNode(z).notNode());
       }
     }
@@ -1977,14 +2134,14 @@ static Node getScBvShl(bool pol,
       {
         /* x << s < t
          * with side condition (synthesized):
-         * (not (= t z)) */
+         * (not (= t z))  */
         scl = t.eqNode(z).notNode();
       }
       else
       {
         /* x << s >= t
          * with side condition (synthesized):
-         * (bvuge (bvshl ones s) t) */
+         * (bvuge (bvshl ones s) t)  */
         Node shl = nm->mkNode(BITVECTOR_SHL, bv::utils::mkOnes(w), s);
         scl = nm->mkNode(BITVECTOR_UGE, shl, t);
       }
@@ -1995,7 +2152,7 @@ static Node getScBvShl(bool pol,
       {
         /* s << x < t
          * with side condition (synthesized):
-         * (not (= t z)) */
+         * (not (= t z))  */
         scl = t.eqNode(z).notNode();
       }
       else
@@ -2003,7 +2160,7 @@ static Node getScBvShl(bool pol,
         /* s << x >= t
          * with side condition:
          * (or (bvuge (bvshl s i) t) ...)
-         * for i in 0..w-1 */
+         * for i in 0..w-1  */
         scl = naiveShlSc1(BITVECTOR_UGE, s, t);
       }
     }
@@ -2016,7 +2173,9 @@ static Node getScBvShl(bool pol,
       {
         /* x << s > t
          * with side condition (synthesized):
-         * (bvult t (bvshl ones s)) */
+         * (bvult t (bvshl ones s))
+         * where
+         * ones = ~0 with getSize(ones) = w  */
         Node shl = nm->mkNode(BITVECTOR_SHL, bv::utils::mkOnes(w), s);
         scl = nm->mkNode(BITVECTOR_ULT, t, shl);
       }
@@ -2024,7 +2183,7 @@ static Node getScBvShl(bool pol,
       {
         /* x << s <= t
          * with side condition:
-         * true (no side condition) */
+         * true (no side condition)  */
         scl = nm->mkConst<bool>(true);
       }
     }
@@ -2035,14 +2194,14 @@ static Node getScBvShl(bool pol,
         /* s << x > t
          * with side condition:
          * (or (bvugt (bvshl s i) t) ...)
-         * for i in 0..w-1 */
+         * for i in 0..w-1  */
         scl = naiveShlSc1(BITVECTOR_UGT, s, t);
       }
       else
       {
         /* s << x <= t
          * with side condition:
-         * true (no side condition) */
+         * true (no side condition)  */
         scl = nm->mkConst<bool>(true);
       }
     }
@@ -2055,9 +2214,9 @@ static Node getScBvShl(bool pol,
       {
         /* x << s < t
          * with side condition (synthesized):
-         * (bvslt (bvshl (bvlshr min_val s) s) t)
+         * (bvslt (bvshl (bvlshr min s) s) t)
          * where
-         * min_val is the signed minimum value */
+         * min is the signed minimum value with getSize(min) = w  */
         BitVector bv_min_val = BitVector(w).setBit(w - 1);
         Node min = bv::utils::mkConst(bv_min_val);
         Node lshr = nm->mkNode(BITVECTOR_LSHR, min, s);
@@ -2068,9 +2227,9 @@ static Node getScBvShl(bool pol,
       {
         /* x << s >= t
          * with side condition (synthesized):
-         * (bvsge (bvand (bvshl max_val s) max_val) t)
+         * (bvsge (bvand (bvshl max s) max) t)
          * where
-         * max_val is the signed maximum value */
+         * max is the signed maximum value with getSize(max) = w  */
         BitVector bv_ones = bv::utils::mkBitVectorOnes(w - 1);
         BitVector bv_max_val = BitVector(1).concat(bv_ones);
         Node max = bv::utils::mkConst(bv_max_val);
@@ -2084,9 +2243,9 @@ static Node getScBvShl(bool pol,
       {
         /* s << x < t
          * with side condition (synthesized):
-         * (bvult (bvshl min_val s) (bvadd t min_val))
+         * (bvult (bvshl min s) (bvadd t min))
          * where
-         * min_val is the signed minimum value */
+         * min is the signed minimum value with getSize(min) = w  */
         BitVector bv_min_val = BitVector(w).setBit(w - 1);
         Node min = bv::utils::mkConst(bv_min_val);
         Node shl = nm->mkNode(BITVECTOR_SHL, min, s);
@@ -2098,7 +2257,7 @@ static Node getScBvShl(bool pol,
         /* s << x >= t
          * with side condition:
          * (or (bvsge (bvshl s i) t) ...)
-         * for i in 0..w-1 */
+         * for i in 0..w-1  */
         scl = naiveShlSc1(BITVECTOR_SGE, s, t);
       }
     }
@@ -2112,9 +2271,9 @@ static Node getScBvShl(bool pol,
       {
         /* x << s > t
          * with side condition (synthesized):
-         * (bvslt t (bvand (bvshl max_val s) max_val))
+         * (bvslt t (bvand (bvshl max s) max))
          * where
-         * max_val is the signed maximum value */
+         * max is the signed maximum value with getSize(max) = w  */
         BitVector bv_ones = bv::utils::mkBitVectorOnes(w - 1);
         BitVector bv_max_val = BitVector(1).concat(bv_ones);
         Node max = bv::utils::mkConst(bv_max_val);
@@ -2125,9 +2284,9 @@ static Node getScBvShl(bool pol,
       {
         /* x << s <= t
          * with side condition (synthesized):
-         * (bvult (bvlshr t (bvlshr t s)) min_val)
+         * (bvult (bvlshr t (bvlshr t s)) min)
          * where
-         * min_val is the signed minimum value */
+         * min is the signed minimum value with getSize(min) = w  */
         BitVector bv_min_val = BitVector(w).setBit(w - 1);
         Node min = bv::utils::mkConst(bv_min_val);
         Node ts = nm->mkNode(BITVECTOR_LSHR, t, s);
@@ -2141,16 +2300,16 @@ static Node getScBvShl(bool pol,
         /* s << x > t
          * with side condition:
          * (or (bvsgt (bvshl s i) t) ...)
-         * for i in 0..w-1 */
+         * for i in 0..w-1  */
         scl = naiveShlSc1(BITVECTOR_SGT, s, t);
       }
       else
       {
         /* s << x <= t
          * with side condition (synthesized):
-         * (bvult (bvlshr t s) min_val)
+         * (bvult (bvlshr t s) min)
          * where
-         * min_val is the signed minimum value */
+         * min is the signed minimum value with getSize(min) = w  */
         BitVector bv_min_val = BitVector(w).setBit(w - 1);
         Node min = bv::utils::mkConst(bv_min_val);
         scl = nm->mkNode(BITVECTOR_ULT, nm->mkNode(BITVECTOR_LSHR, t, s), min);
@@ -2233,8 +2392,7 @@ Node BvInverter::solveBvLit(Node sv,
       /* x = t[upper:lower]
        * where
        * upper = getSize(t) - 1 - sum(getSize(sv_t[i])) for i < index
-       * lower = getSize(sv_t[i]) for i > index
-       */
+       * lower = getSize(sv_t[i]) for i > index  */
       unsigned upper, lower;
       upper = bv::utils::getSize(t) - 1;
       lower = 0;
@@ -2318,22 +2476,7 @@ Node BvInverter::solveBvLit(Node sv,
                                << " for bit-vector term " << sv_t << std::endl;
             return Node::null();
         }
-        Assert (litk != EQUAL || !sc.isNull());
-        /* No specific handling for litk and operator k, generate generic
-         * side condition. */
-        if (sc.isNull())
-        {
-          solve_tn = sv_t.getType();
-          if (litk == BITVECTOR_ULT || litk == BITVECTOR_UGT)
-          {
-            sc = getScBvUltUgt(pol, litk, getSolveVariable(solve_tn), t);
-          }
-          else
-          {
-            Assert (litk == BITVECTOR_SLT || litk == BITVECTOR_SGT);
-            sc = getScBvSltSgt(pol, litk, getSolveVariable(solve_tn), t);
-          }
-        }
+        Assert(!sc.isNull());
         /* 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.,