Remove partial UDIV/UREM operators. (#6069)

This commit removes the partial UDIV/UREM operator handling. BITVECTOR_UDIV and BITVECTOR_UREM are now total.

2 files changed, 67 insertions, 81 deletions

diff --git a/test/unit/preprocessing/pass_bv_gauss_white.cpp b/test/unit/preprocessing/pass_bv_gauss_white.cpp
index 5e2e80e4a..9ae4a7eac 100644
--- a/test/unit/preprocessing/pass_bv_gauss_white.cpp
+++ b/test/unit/preprocessing/pass_bv_gauss_white.cpp
@@ -960,7 +960,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_unique2)
       d_x);
   Node y_mul_one = d_nodeManager->mkNode(
       kind::BITVECTOR_MULT,
-      d_nodeManager->mkNode(kind::BITVECTOR_UREM_TOTAL, d_one, d_five),
+      d_nodeManager->mkNode(kind::BITVECTOR_UREM, d_one, d_five),
       d_y);
   Node z_mul_one =
       d_nodeManager->mkNode(kind::BITVECTOR_MULT, bv::utils::mkOne(32), d_z);
@@ -989,7 +989,7 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_unique2)
   Node x_mul_four = d_nodeManager->mkNode(
       kind::BITVECTOR_MULT,
       d_nodeManager->mkNode(
-          kind::BITVECTOR_UDIV_TOTAL,
+          kind::BITVECTOR_UDIV,
           d_nodeManager->mkNode(
               kind::BITVECTOR_PLUS,
               d_nodeManager->mkNode(kind::BITVECTOR_MULT,
@@ -2193,11 +2193,11 @@ TEST_F(TestPPWhiteBVGauss, elim_rewrite_for_urem_not_invalid1)
    * ------------------------------------------------------------------- */
 
   Node n1 = d_nodeManager->mkNode(
-      kind::BITVECTOR_UDIV_TOTAL,
+      kind::BITVECTOR_UDIV,
       d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_three, d_x),
       d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_two, d_y));
   Node n2 = d_nodeManager->mkNode(
-      kind::BITVECTOR_UREM_TOTAL,
+      kind::BITVECTOR_UREM,
       d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_two, d_x),
       d_nodeManager->mkNode(kind::BITVECTOR_MULT, d_five, d_y));
 
@@ -2699,39 +2699,29 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw1)
   Node concat2x = bv::utils::mkConcat(bv::utils::mkZero(16), zext48x);
   ASSERT_EQ(BVGauss::getMinBwExpr(concat2x), 16);
 
-  Node udiv1p =
-      d_nodeManager->mkNode(kind::BITVECTOR_UDIV_TOTAL, zext48p, zext48p);
+  Node udiv1p = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, zext48p, zext48p);
   ASSERT_EQ(BVGauss::getMinBwExpr(udiv1p), 1);
-  Node udiv1x =
-      d_nodeManager->mkNode(kind::BITVECTOR_UDIV_TOTAL, zext48x, zext48x);
+  Node udiv1x = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, zext48x, zext48x);
   ASSERT_EQ(BVGauss::getMinBwExpr(udiv1x), 48);
 
-  Node udiv2p =
-      d_nodeManager->mkNode(kind::BITVECTOR_UDIV_TOTAL, zext48p, zext48p8);
+  Node udiv2p = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, zext48p, zext48p8);
   ASSERT_EQ(BVGauss::getMinBwExpr(udiv2p), 1);
-  Node udiv2x =
-      d_nodeManager->mkNode(kind::BITVECTOR_UDIV_TOTAL, zext48x, zext48x8);
+  Node udiv2x = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, zext48x, zext48x8);
   ASSERT_EQ(BVGauss::getMinBwExpr(udiv2x), 48);
 
-  Node urem1p =
-      d_nodeManager->mkNode(kind::BITVECTOR_UREM_TOTAL, zext48p, zext48p);
+  Node urem1p = d_nodeManager->mkNode(kind::BITVECTOR_UREM, zext48p, zext48p);
   ASSERT_EQ(BVGauss::getMinBwExpr(urem1p), 1);
-  Node urem1x =
-      d_nodeManager->mkNode(kind::BITVECTOR_UREM_TOTAL, zext48x, zext48x);
+  Node urem1x = d_nodeManager->mkNode(kind::BITVECTOR_UREM, zext48x, zext48x);
   ASSERT_EQ(BVGauss::getMinBwExpr(urem1x), 1);
 
-  Node urem2p =
-      d_nodeManager->mkNode(kind::BITVECTOR_UREM_TOTAL, zext48p, zext48p8);
+  Node urem2p = d_nodeManager->mkNode(kind::BITVECTOR_UREM, zext48p, zext48p8);
   ASSERT_EQ(BVGauss::getMinBwExpr(urem2p), 1);
-  Node urem2x =
-      d_nodeManager->mkNode(kind::BITVECTOR_UREM_TOTAL, zext48x, zext48x8);
+  Node urem2x = d_nodeManager->mkNode(kind::BITVECTOR_UREM, zext48x, zext48x8);
   ASSERT_EQ(BVGauss::getMinBwExpr(urem2x), 16);
 
-  Node urem3p =
-      d_nodeManager->mkNode(kind::BITVECTOR_UREM_TOTAL, zext48p8, zext48p);
+  Node urem3p = d_nodeManager->mkNode(kind::BITVECTOR_UREM, zext48p8, zext48p);
   ASSERT_EQ(BVGauss::getMinBwExpr(urem3p), 1);
-  Node urem3x =
-      d_nodeManager->mkNode(kind::BITVECTOR_UREM_TOTAL, zext48x8, zext48x);
+  Node urem3x = d_nodeManager->mkNode(kind::BITVECTOR_UREM, zext48x8, zext48x);
   ASSERT_EQ(BVGauss::getMinBwExpr(urem3x), 8);
 
   Node add1p = d_nodeManager->mkNode(kind::BITVECTOR_PLUS, extp, extp);
@@ -2806,11 +2796,11 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw3a)
   Node z = d_nodeManager->mkVar("z", d_nodeManager->mkBitVectorType(16));
   Node zextop5 =
       d_nodeManager->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(5));
-  Node udiv1 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV_TOTAL, x, y);
+  Node udiv1 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, x, y);
   Node zext1 = d_nodeManager->mkNode(zextop5, udiv1);
   Node ext1 = bv::utils::mkExtract(zext1, 4, 0);
   Node ext2 = bv::utils::mkExtract(z, 4, 0);
-  Node udiv2 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV_TOTAL, ext1, ext2);
+  Node udiv2 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, ext1, ext2);
   Node zext2 = bv::utils::mkConcat(bv::utils::mkZero(5), udiv2);
   ASSERT_EQ(BVGauss::getMinBwExpr(zext2), 5);
 }
@@ -2822,11 +2812,11 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw3b)
    *             ((_ extract 4 0) z)))  */
   Node zextop5 =
       d_nodeManager->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(5));
-  Node udiv1 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV_TOTAL, d_x, d_y);
+  Node udiv1 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, d_x, d_y);
   Node zext1 = d_nodeManager->mkNode(zextop5, udiv1);
   Node ext1 = bv::utils::mkExtract(zext1, 4, 0);
   Node ext2 = bv::utils::mkExtract(d_z, 4, 0);
-  Node udiv2 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV_TOTAL, ext1, ext2);
+  Node udiv2 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, ext1, ext2);
   Node zext2 = bv::utils::mkConcat(bv::utils::mkZero(5), udiv2);
   ASSERT_EQ(BVGauss::getMinBwExpr(zext2), 5);
 }
@@ -2848,19 +2838,17 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw4a)
   Node zextop7 =
       d_nodeManager->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(7));
 
-  Node udiv1 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV_TOTAL, x, y);
+  Node udiv1 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, x, y);
   Node zext1 = d_nodeManager->mkNode(zextop5, udiv1);
 
   Node ext1_1 = bv::utils::mkExtract(zext1, 4, 0);
   Node ext2_1 = bv::utils::mkExtract(z, 4, 0);
-  Node udiv2_1 =
-      d_nodeManager->mkNode(kind::BITVECTOR_UDIV_TOTAL, ext1_1, ext2_1);
+  Node udiv2_1 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, ext1_1, ext2_1);
   Node zext2_1 = bv::utils::mkConcat(bv::utils::mkZero(5), udiv2_1);
 
   Node ext1_2 = bv::utils::mkExtract(zext1, 2, 0);
   Node ext2_2 = bv::utils::mkExtract(z, 2, 0);
-  Node udiv2_2 =
-      d_nodeManager->mkNode(kind::BITVECTOR_UDIV_TOTAL, ext1_2, ext2_2);
+  Node udiv2_2 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, ext1_2, ext2_2);
   Node zext2_2 = d_nodeManager->mkNode(zextop7, udiv2_2);
 
   Node plus = d_nodeManager->mkNode(kind::BITVECTOR_PLUS, zext2_1, zext2_2);
@@ -2882,19 +2870,17 @@ TEST_F(TestPPWhiteBVGauss, get_min_bw4b)
   Node zextop7 =
       d_nodeManager->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(7));
 
-  Node udiv1 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV_TOTAL, d_x, d_y);
+  Node udiv1 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, d_x, d_y);
   Node zext1 = d_nodeManager->mkNode(zextop5, udiv1);
 
   Node ext1_1 = bv::utils::mkExtract(zext1, 4, 0);
   Node ext2_1 = bv::utils::mkExtract(d_z, 4, 0);
-  Node udiv2_1 =
-      d_nodeManager->mkNode(kind::BITVECTOR_UDIV_TOTAL, ext1_1, ext2_1);
+  Node udiv2_1 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, ext1_1, ext2_1);
   Node zext2_1 = bv::utils::mkConcat(bv::utils::mkZero(5), udiv2_1);
 
   Node ext1_2 = bv::utils::mkExtract(zext1, 2, 0);
   Node ext2_2 = bv::utils::mkExtract(d_z, 2, 0);
-  Node udiv2_2 =
-      d_nodeManager->mkNode(kind::BITVECTOR_UDIV_TOTAL, ext1_2, ext2_2);
+  Node udiv2_2 = d_nodeManager->mkNode(kind::BITVECTOR_UDIV, ext1_2, ext2_2);
   Node zext2_2 = d_nodeManager->mkNode(zextop7, udiv2_2);
 
   Node plus = d_nodeManager->mkNode(kind::BITVECTOR_PLUS, zext2_1, zext2_2);
diff --git a/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp b/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp
index b5996a684..fd740167f 100644
--- a/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp
+++ b/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp
@@ -99,15 +99,15 @@ class TestTheoryWhiteQuantifiersBvInverter : public TestSmtNoFinishInit
                unsigned idx,
                Node (*getsc)(bool, Kind, Kind, unsigned, Node, Node, Node))
   {
-    ASSERT_TRUE(k == BITVECTOR_MULT || k == BITVECTOR_UREM_TOTAL
-                || k == BITVECTOR_UDIV_TOTAL || k == BITVECTOR_AND
+    ASSERT_TRUE(k == BITVECTOR_MULT || k == BITVECTOR_UREM
+                || k == BITVECTOR_UDIV || k == BITVECTOR_AND
                 || k == BITVECTOR_OR || k == BITVECTOR_LSHR
                 || k == BITVECTOR_ASHR || k == BITVECTOR_SHL);
 
     Node sc = getsc(pol, litk, k, idx, d_sk, d_s, d_t);
     ASSERT_FALSE(sc.isNull());
     Kind ksc = sc.getKind();
-    ASSERT_TRUE((k == BITVECTOR_UDIV_TOTAL && idx == 1 && pol == false)
+    ASSERT_TRUE((k == BITVECTOR_UDIV && idx == 1 && pol == false)
                 || (k == BITVECTOR_ASHR && idx == 0 && pol == false)
                 || ksc == IMPLIES);
     Node scl = ksc == IMPLIES ? sc[0] : bv::utils::mkTrue();
@@ -301,44 +301,44 @@ TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_mult_eq_false1)
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_eq_true0)
 {
-  runTest(true, EQUAL, BITVECTOR_UREM_TOTAL, 0, getICBvUrem);
+  runTest(true, EQUAL, BITVECTOR_UREM, 0, getICBvUrem);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_eq_true1)
 {
-  runTest(true, EQUAL, BITVECTOR_UREM_TOTAL, 1, getICBvUrem);
+  runTest(true, EQUAL, BITVECTOR_UREM, 1, getICBvUrem);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_eq_false0)
 {
-  runTest(false, EQUAL, BITVECTOR_UREM_TOTAL, 0, getICBvUrem);
+  runTest(false, EQUAL, BITVECTOR_UREM, 0, getICBvUrem);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_eq_false1)
 {
-  runTest(false, EQUAL, BITVECTOR_UREM_TOTAL, 1, getICBvUrem);
+  runTest(false, EQUAL, BITVECTOR_UREM, 1, getICBvUrem);
 }
 
 /* Udiv */
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_eq_true0)
 {
-  runTest(true, EQUAL, BITVECTOR_UDIV_TOTAL, 0, getICBvUdiv);
+  runTest(true, EQUAL, BITVECTOR_UDIV, 0, getICBvUdiv);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_eq_true1)
 {
-  runTest(true, EQUAL, BITVECTOR_UDIV_TOTAL, 1, getICBvUdiv);
+  runTest(true, EQUAL, BITVECTOR_UDIV, 1, getICBvUdiv);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_eq_false0)
 {
-  runTest(false, EQUAL, BITVECTOR_UDIV_TOTAL, 0, getICBvUdiv);
+  runTest(false, EQUAL, BITVECTOR_UDIV, 0, getICBvUdiv);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_eq_false1)
 {
-  runTest(false, EQUAL, BITVECTOR_UDIV_TOTAL, 1, getICBvUdiv);
+  runTest(false, EQUAL, BITVECTOR_UDIV, 1, getICBvUdiv);
 }
 
 /* And */
@@ -877,164 +877,164 @@ TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_mult_sgt_false1)
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_ult_true0)
 {
-  runTest(true, BITVECTOR_ULT, BITVECTOR_UREM_TOTAL, 0, getICBvUrem);
+  runTest(true, BITVECTOR_ULT, BITVECTOR_UREM, 0, getICBvUrem);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_ult_true1)
 {
-  runTest(true, BITVECTOR_ULT, BITVECTOR_UREM_TOTAL, 1, getICBvUrem);
+  runTest(true, BITVECTOR_ULT, BITVECTOR_UREM, 1, getICBvUrem);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_ult_false0)
 {
-  runTest(false, BITVECTOR_ULT, BITVECTOR_UREM_TOTAL, 0, getICBvUrem);
+  runTest(false, BITVECTOR_ULT, BITVECTOR_UREM, 0, getICBvUrem);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_ult_false1)
 {
-  runTest(false, BITVECTOR_ULT, BITVECTOR_UREM_TOTAL, 1, getICBvUrem);
+  runTest(false, BITVECTOR_ULT, BITVECTOR_UREM, 1, getICBvUrem);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_ugt_true0)
 {
-  runTest(true, BITVECTOR_UGT, BITVECTOR_UREM_TOTAL, 0, getICBvUrem);
+  runTest(true, BITVECTOR_UGT, BITVECTOR_UREM, 0, getICBvUrem);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_ugt_true1)
 {
-  runTest(true, BITVECTOR_UGT, BITVECTOR_UREM_TOTAL, 1, getICBvUrem);
+  runTest(true, BITVECTOR_UGT, BITVECTOR_UREM, 1, getICBvUrem);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_ugt_false0)
 {
-  runTest(false, BITVECTOR_UGT, BITVECTOR_UREM_TOTAL, 0, getICBvUrem);
+  runTest(false, BITVECTOR_UGT, BITVECTOR_UREM, 0, getICBvUrem);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_ugt_false1)
 {
-  runTest(false, BITVECTOR_UGT, BITVECTOR_UREM_TOTAL, 1, getICBvUrem);
+  runTest(false, BITVECTOR_UGT, BITVECTOR_UREM, 1, getICBvUrem);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_slt_true0)
 {
-  runTest(true, BITVECTOR_SLT, BITVECTOR_UREM_TOTAL, 0, getICBvUrem);
+  runTest(true, BITVECTOR_SLT, BITVECTOR_UREM, 0, getICBvUrem);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_slt_true1)
 {
-  runTest(true, BITVECTOR_SLT, BITVECTOR_UREM_TOTAL, 1, getICBvUrem);
+  runTest(true, BITVECTOR_SLT, BITVECTOR_UREM, 1, getICBvUrem);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_slt_false0)
 {
-  runTest(false, BITVECTOR_SLT, BITVECTOR_UREM_TOTAL, 0, getICBvUrem);
+  runTest(false, BITVECTOR_SLT, BITVECTOR_UREM, 0, getICBvUrem);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_slt_false1)
 {
-  runTest(false, BITVECTOR_SLT, BITVECTOR_UREM_TOTAL, 1, getICBvUrem);
+  runTest(false, BITVECTOR_SLT, BITVECTOR_UREM, 1, getICBvUrem);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_sgt_true0)
 {
-  runTest(true, BITVECTOR_SGT, BITVECTOR_UREM_TOTAL, 0, getICBvUrem);
+  runTest(true, BITVECTOR_SGT, BITVECTOR_UREM, 0, getICBvUrem);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_sgt_true1)
 {
-  runTest(true, BITVECTOR_SGT, BITVECTOR_UREM_TOTAL, 1, getICBvUrem);
+  runTest(true, BITVECTOR_SGT, BITVECTOR_UREM, 1, getICBvUrem);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_sgt_false0)
 {
-  runTest(false, BITVECTOR_SGT, BITVECTOR_UREM_TOTAL, 0, getICBvUrem);
+  runTest(false, BITVECTOR_SGT, BITVECTOR_UREM, 0, getICBvUrem);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_urem_sgt_false1)
 {
-  runTest(false, BITVECTOR_SGT, BITVECTOR_UREM_TOTAL, 1, getICBvUrem);
+  runTest(false, BITVECTOR_SGT, BITVECTOR_UREM, 1, getICBvUrem);
 }
 
 /* Udiv */
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_ult_true0)
 {
-  runTest(true, BITVECTOR_ULT, BITVECTOR_UDIV_TOTAL, 0, getICBvUdiv);
+  runTest(true, BITVECTOR_ULT, BITVECTOR_UDIV, 0, getICBvUdiv);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_ult_true1)
 {
-  runTest(true, BITVECTOR_ULT, BITVECTOR_UDIV_TOTAL, 1, getICBvUdiv);
+  runTest(true, BITVECTOR_ULT, BITVECTOR_UDIV, 1, getICBvUdiv);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_ult_false0)
 {
-  runTest(false, BITVECTOR_ULT, BITVECTOR_UDIV_TOTAL, 0, getICBvUdiv);
+  runTest(false, BITVECTOR_ULT, BITVECTOR_UDIV, 0, getICBvUdiv);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_ult_false1)
 {
-  runTest(false, BITVECTOR_ULT, BITVECTOR_UDIV_TOTAL, 1, getICBvUdiv);
+  runTest(false, BITVECTOR_ULT, BITVECTOR_UDIV, 1, getICBvUdiv);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_ugt_true0)
 {
-  runTest(true, BITVECTOR_UGT, BITVECTOR_UDIV_TOTAL, 0, getICBvUdiv);
+  runTest(true, BITVECTOR_UGT, BITVECTOR_UDIV, 0, getICBvUdiv);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_ugt_true1)
 {
-  runTest(true, BITVECTOR_UGT, BITVECTOR_UDIV_TOTAL, 1, getICBvUdiv);
+  runTest(true, BITVECTOR_UGT, BITVECTOR_UDIV, 1, getICBvUdiv);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_ugt_false0)
 {
-  runTest(false, BITVECTOR_UGT, BITVECTOR_UDIV_TOTAL, 0, getICBvUdiv);
+  runTest(false, BITVECTOR_UGT, BITVECTOR_UDIV, 0, getICBvUdiv);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_ugt_false1)
 {
-  runTest(false, BITVECTOR_UGT, BITVECTOR_UDIV_TOTAL, 1, getICBvUdiv);
+  runTest(false, BITVECTOR_UGT, BITVECTOR_UDIV, 1, getICBvUdiv);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_slt_true0)
 {
-  runTest(true, BITVECTOR_SLT, BITVECTOR_UDIV_TOTAL, 0, getICBvUdiv);
+  runTest(true, BITVECTOR_SLT, BITVECTOR_UDIV, 0, getICBvUdiv);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_slt_true1)
 {
-  runTest(true, BITVECTOR_SLT, BITVECTOR_UDIV_TOTAL, 1, getICBvUdiv);
+  runTest(true, BITVECTOR_SLT, BITVECTOR_UDIV, 1, getICBvUdiv);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_slt_false0)
 {
-  runTest(false, BITVECTOR_SLT, BITVECTOR_UDIV_TOTAL, 0, getICBvUdiv);
+  runTest(false, BITVECTOR_SLT, BITVECTOR_UDIV, 0, getICBvUdiv);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_slt_false1)
 {
-  runTest(false, BITVECTOR_SLT, BITVECTOR_UDIV_TOTAL, 1, getICBvUdiv);
+  runTest(false, BITVECTOR_SLT, BITVECTOR_UDIV, 1, getICBvUdiv);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_sgt_true0)
 {
-  runTest(true, BITVECTOR_SGT, BITVECTOR_UDIV_TOTAL, 0, getICBvUdiv);
+  runTest(true, BITVECTOR_SGT, BITVECTOR_UDIV, 0, getICBvUdiv);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_sgt_true1)
 {
-  runTest(true, BITVECTOR_SGT, BITVECTOR_UDIV_TOTAL, 1, getICBvUdiv);
+  runTest(true, BITVECTOR_SGT, BITVECTOR_UDIV, 1, getICBvUdiv);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_sgt_false0)
 {
-  runTest(false, BITVECTOR_SGT, BITVECTOR_UDIV_TOTAL, 0, getICBvUdiv);
+  runTest(false, BITVECTOR_SGT, BITVECTOR_UDIV, 0, getICBvUdiv);
 }
 
 TEST_F(TestTheoryWhiteQuantifiersBvInverter, getIC_bv_udiv_sgt_false1)
 {
-  runTest(false, BITVECTOR_SGT, BITVECTOR_UDIV_TOTAL, 1, getICBvUdiv);
+  runTest(false, BITVECTOR_SGT, BITVECTOR_UDIV, 1, getICBvUdiv);
 }
 
 /* And */