diff --git a/src/cprover/bv_pointers_wide.cpp b/src/cprover/bv_pointers_wide.cpp
index 8cb9e7b46a3..dc4ba7bcd28 100644
--- a/src/cprover/bv_pointers_wide.cpp
+++ b/src/cprover/bv_pointers_wide.cpp
@@ -629,9 +629,30 @@ bvt bv_pointers_widet::convert_bitvector(const exprt &expr)
           difference, element_size_bv, bv_utilst::representationt::SIGNED);
       }
 
-      prop.l_set_to_true(prop.limplies(
-        prop.land(same_object_lit, prop.land(lhs_in_bounds, rhs_in_bounds)),
-        bv_utils.equal(difference, bv)));
+      if(prop.cnf_handled_well())
+      {
+        for(std::size_t i = 0; i < width; ++i)
+        {
+          prop.lcnf(
+            {!same_object_lit,
+             !lhs_in_bounds,
+             !rhs_in_bounds,
+             !difference[i],
+             bv[i]});
+          prop.lcnf(
+            {!same_object_lit,
+             !lhs_in_bounds,
+             !rhs_in_bounds,
+             difference[i],
+             !bv[i]});
+        }
+      }
+      else
+      {
+        prop.l_set_to_true(prop.limplies(
+          prop.land(same_object_lit, prop.land(lhs_in_bounds, rhs_in_bounds)),
+          bv_utils.equal(difference, bv)));
+      }
     }
 
     return bv;
@@ -892,7 +913,10 @@ void bv_pointers_widet::do_postponed(const postponedt &postponed)
       if(!is_dynamic)
         l2 = !l2;
 
-      prop.l_set_to_true(prop.limplies(l1, l2));
+      if(prop.cnf_handled_well())
+        prop.lcnf({!l1, l2});
+      else
+        prop.l_set_to_true(prop.limplies(l1, l2));
     }
   }
   else if(
@@ -933,7 +957,10 @@ void bv_pointers_widet::do_postponed(const postponedt &postponed)
       literalt l1 = bv_utils.equal(bv, saved_bv);
       literalt l2 = bv_utils.equal(postponed.bv, size_bv);
 
-      prop.l_set_to_true(prop.limplies(l1, l2));
+      if(prop.cnf_handled_well())
+        prop.lcnf({!l1, l2});
+      else
+        prop.l_set_to_true(prop.limplies(l1, l2));
     }
   }
   else
diff --git a/src/solvers/flattening/boolbv_bv_rel.cpp b/src/solvers/flattening/boolbv_bv_rel.cpp
index 35febd35421..4f01cfef153 100644
--- a/src/solvers/flattening/boolbv_bv_rel.cpp
+++ b/src/solvers/flattening/boolbv_bv_rel.cpp
@@ -73,10 +73,20 @@ literalt boolbvt::convert_bv_rel(const binary_relation_exprt &expr)
         {
           literalt equal_lit = equality(lhs, rhs);
 
-          if(or_equal)
-            prop.l_set_to_true(prop.limplies(equal_lit, literal));
+          if(prop.cnf_handled_well())
+          {
+            if(or_equal)
+              prop.lcnf(!equal_lit, literal);
+            else
+              prop.lcnf(!equal_lit, !literal);
+          }
           else
-            prop.l_set_to_true(prop.limplies(equal_lit, !literal));
+          {
+            if(or_equal)
+              prop.l_set_to_true(prop.limplies(equal_lit, literal));
+            else
+              prop.l_set_to_true(prop.limplies(equal_lit, !literal));
+          }
         }
       }
 
diff --git a/src/solvers/flattening/boolbv_byte_extract.cpp b/src/solvers/flattening/boolbv_byte_extract.cpp
index 01cb688063f..7f451c01597 100644
--- a/src/solvers/flattening/boolbv_byte_extract.cpp
+++ b/src/solvers/flattening/boolbv_byte_extract.cpp
@@ -142,9 +142,32 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
           else
             equal_bv[j]=const_literal(true);
 
-        prop.l_set_to_true(prop.limplies(
-          convert(equal_exprt(expr.offset(), from_integer(i, constant_type))),
-          prop.land(equal_bv)));
+        if(prop.cnf_handled_well())
+        {
+          literalt index_eq =
+            convert(equal_exprt(expr.offset(), from_integer(i, constant_type)));
+
+          for(std::size_t j = 0; j < width; j++)
+          {
+            if(offset + j >= op_bv.size())
+              break;
+
+            prop.lcnf({!index_eq, !bv[j], op_bv[offset + j]});
+            prop.lcnf({!index_eq, bv[j], !op_bv[offset + j]});
+          }
+        }
+        else
+        {
+          for(std::size_t j = 0; j < width; j++)
+            if(offset + j < op_bv.size())
+              equal_bv[j] = prop.lequal(bv[j], op_bv[offset + j]);
+            else
+              equal_bv[j] = const_literal(true);
+
+          prop.l_set_to_true(prop.limplies(
+            convert(equal_exprt(expr.offset(), from_integer(i, constant_type))),
+            prop.land(equal_bv)));
+        }
       }
     }
     else
diff --git a/src/solvers/flattening/boolbv_case.cpp b/src/solvers/flattening/boolbv_case.cpp
index 54eb819fd38..f12a902149c 100644
--- a/src/solvers/flattening/boolbv_case.cpp
+++ b/src/solvers/flattening/boolbv_case.cpp
@@ -68,8 +68,10 @@ bvt boolbvt::convert_case(const exprt &expr)
       {
         literalt value_literal=bv_utils.equal(bv, op);
 
-        prop.l_set_to_true(
-          prop.limplies(compare_literal, value_literal));
+        if(prop.cnf_handled_well())
+          prop.lcnf({!compare_literal, value_literal});
+        else
+          prop.l_set_to_true(prop.limplies(compare_literal, value_literal));
       }
 
       what=COMPARE;
diff --git a/src/solvers/flattening/boolbv_cond.cpp b/src/solvers/flattening/boolbv_cond.cpp
index 28f52d57228..13e6095b1ab 100644
--- a/src/solvers/flattening/boolbv_cond.cpp
+++ b/src/solvers/flattening/boolbv_cond.cpp
@@ -45,9 +45,19 @@ bvt boolbvt::convert_cond(const cond_exprt &expr)
       {
         const bvt &op = convert_bv(operand, bv.size());
 
-        literalt value_literal=bv_utils.equal(bv, op);
-
-        prop.l_set_to_true(prop.limplies(cond_literal, value_literal));
+        if(prop.cnf_handled_well())
+        {
+          for(std::size_t i = 0; i < bv.size(); ++i)
+          {
+            prop.lcnf({!cond_literal, !bv[i], op[i]});
+            prop.lcnf({!cond_literal, bv[i], !op[i]});
+          }
+        }
+        else
+        {
+          literalt value_literal = bv_utils.equal(bv, op);
+          prop.l_set_to_true(prop.limplies(cond_literal, value_literal));
+        }
       }
 
       condition=!condition;
diff --git a/src/solvers/flattening/boolbv_extractbit.cpp b/src/solvers/flattening/boolbv_extractbit.cpp
index 29dcb5c62cc..8e6a8d712ed 100644
--- a/src/solvers/flattening/boolbv_extractbit.cpp
+++ b/src/solvers/flattening/boolbv_extractbit.cpp
@@ -65,8 +65,17 @@ literalt boolbvt::convert_extractbit(const extractbit_exprt &expr)
       for(std::size_t i = 0; i < src_bv.size(); i++)
       {
         equal_exprt equality(index_casted, from_integer(i, index_type));
-        literalt equal = prop.lequal(literal, src_bv[i]);
-        prop.l_set_to_true(prop.limplies(convert(equality), equal));
+        if(prop.cnf_handled_well())
+        {
+          literalt index_eq = convert(equality);
+          prop.lcnf({!index_eq, !literal, src_bv[i]});
+          prop.lcnf({!index_eq, literal, !src_bv[i]});
+        }
+        else
+        {
+          literalt equal = prop.lequal(literal, src_bv[i]);
+          prop.l_set_to_true(prop.limplies(convert(equality), equal));
+        }
       }
 
       return literal;
diff --git a/src/solvers/flattening/boolbv_index.cpp b/src/solvers/flattening/boolbv_index.cpp
index 2e400a57345..dbe63743ea7 100644
--- a/src/solvers/flattening/boolbv_index.cpp
+++ b/src/solvers/flattening/boolbv_index.cpp
@@ -186,9 +186,18 @@ bvt boolbvt::convert_index(const index_exprt &expr)
           "past the array's end");
 
         // Cache comparisons and equalities
-        prop.l_set_to_true(convert(implies_exprt(
-          equal_exprt(index, from_integer(i, index.type())),
-          equal_exprt(result, *it++))));
+        if(prop.cnf_handled_well())
+        {
+          prop.lcnf(
+            {!convert(equal_exprt(index, from_integer(i, index.type()))),
+             convert(equal_exprt(result, *it++))});
+        }
+        else
+        {
+          prop.l_set_to_true(convert(implies_exprt(
+            equal_exprt(index, from_integer(i, index.type())),
+            equal_exprt(result, *it++))));
+        }
       }
 
       return bv;
@@ -229,13 +238,33 @@ bvt boolbvt::convert_index(const index_exprt &expr)
       {
         mp_integer offset=i*width;
 
-        for(std::size_t j=0; j<width; j++)
-          equal_bv[j] = prop.lequal(
-            bv[j], array_bv[numeric_cast_v<std::size_t>(offset + j)]);
+        if(prop.cnf_handled_well())
+        {
+          literalt index_eq =
+            convert(equal_exprt(index, from_integer(i, index.type())));
+
+          for(std::size_t j = 0; j < width; j++)
+          {
+            prop.lcnf(
+              {!index_eq,
+               !bv[j],
+               array_bv[numeric_cast_v<std::size_t>(offset + j)]});
+            prop.lcnf(
+              {!index_eq,
+               bv[j],
+               !array_bv[numeric_cast_v<std::size_t>(offset + j)]});
+          }
+        }
+        else
+        {
+          for(std::size_t j = 0; j < width; j++)
+            equal_bv[j] = prop.lequal(
+              bv[j], array_bv[numeric_cast_v<std::size_t>(offset + j)]);
 
-        prop.l_set_to_true(prop.limplies(
-          convert(equal_exprt(index, from_integer(i, index.type()))),
-          prop.land(equal_bv)));
+          prop.l_set_to_true(prop.limplies(
+            convert(equal_exprt(index, from_integer(i, index.type()))),
+            prop.land(equal_bv)));
+        }
       }
     }
     else
diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp
index a022801df4b..74e77dba2ff 100644
--- a/src/solvers/flattening/bv_pointers.cpp
+++ b/src/solvers/flattening/bv_pointers.cpp
@@ -697,8 +697,20 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
           prop.lor(in_bounds, prop.land(lhs_in_bounds, rhs_in_bounds));
       }
 
-      prop.l_set_to_true(prop.limplies(
-        prop.land(same_object_lit, in_bounds), bv_utils.equal(difference, bv)));
+      if(prop.cnf_handled_well())
+      {
+        for(std::size_t i = 0; i < width; ++i)
+        {
+          prop.lcnf({!same_object_lit, !in_bounds, !difference[i], bv[i]});
+          prop.lcnf({!same_object_lit, !in_bounds, difference[i], !bv[i]});
+        }
+      }
+      else
+      {
+        prop.l_set_to_true(prop.limplies(
+          prop.land(same_object_lit, in_bounds),
+          bv_utils.equal(difference, bv)));
+      }
     }
 
     return bv;
@@ -1071,10 +1083,18 @@ void bv_pointerst::finish_eager_conversion()
       replace_expr(replacements, is_not_dyn);
 
       PRECONDITION(postponed.bv.size() == 1);
-      prop.l_set_to_true(
-        prop.limplies(convert_bv(is_dyn)[0], postponed.bv.front()));
-      prop.l_set_to_true(
-        prop.limplies(convert_bv(is_not_dyn)[0], !postponed.bv.front()));
+      if(prop.cnf_handled_well())
+      {
+        prop.lcnf({!convert_bv(is_dyn)[0], postponed.bv.front()});
+        prop.lcnf({!convert_bv(is_not_dyn)[0], !postponed.bv.front()});
+      }
+      else
+      {
+        prop.l_set_to_true(
+          prop.limplies(convert_bv(is_dyn)[0], postponed.bv.front()));
+        prop.l_set_to_true(
+          prop.limplies(convert_bv(is_not_dyn)[0], !postponed.bv.front()));
+      }
     }
     else if(
       const auto postponed_object_size =
@@ -1121,7 +1141,10 @@ void bv_pointerst::finish_eager_conversion()
 #ifndef COMPACT_OBJECT_SIZE_EQ
         literalt l2 = bv_utils.equal(postponed.bv, size_bv);
 
-        prop.l_set_to_true(prop.limplies(l1, l2));
+        if(prop.cnf_handled_well())
+          prop.lcnf({!l1, l2});
+        else
+          prop.l_set_to_true(prop.limplies(l1, l2));
 #else
         for(std::size_t i = 0; i < postponed.bv.size(); ++i)
         {
diff --git a/src/solvers/flattening/bv_utils.cpp b/src/solvers/flattening/bv_utils.cpp
index 31dd12fea20..1a804f345ae 100644
--- a/src/solvers/flattening/bv_utils.cpp
+++ b/src/solvers/flattening/bv_utils.cpp
@@ -492,8 +492,16 @@ bvt bv_utilst::adder_no_overflow(
     // we ignore the carry-out
     bvt sum = adder(op0, tmp_op, const_literal(subtract)).first;
 
-    prop.l_set_to_false(
-      prop.land(sign_the_same, prop.lxor(sign_bit(sum), old_sign)));
+    if(prop.cnf_handled_well())
+    {
+      prop.lcnf({!sign_the_same, !sign_bit(sum), old_sign});
+      prop.lcnf({!sign_the_same, sign_bit(sum), !old_sign});
+    }
+    else
+    {
+      prop.l_set_to_false(
+        prop.land(sign_the_same, prop.lxor(sign_bit(sum), old_sign)));
+    }
 
     return sum;
   }
@@ -596,7 +604,19 @@ bvt bv_utilst::negate(const bvt &bv)
 
 bvt bv_utilst::negate_no_overflow(const bvt &bv)
 {
-  prop.l_set_to_false(overflow_negate(bv));
+  if(prop.cnf_handled_well())
+  {
+    // inlined negation of overflow_negate
+    bvt should_be_zeros(bv);
+    should_be_zeros.pop_back();
+    should_be_zeros.push_back(!sign_bit(bv));
+    prop.lcnf(should_be_zeros);
+  }
+  else
+  {
+    prop.l_set_to_false(overflow_negate(bv));
+  }
+
   return negate(bv);
 }
 
@@ -994,7 +1014,12 @@ bvt bv_utilst::unsigned_multiplier_no_overflow(
       product = adder_no_overflow(product, tmpop);
 
       for(std::size_t idx=op1.size()-sum; idx<op1.size(); idx++)
-        prop.l_set_to_false(prop.land(op1[idx], op0[sum]));
+      {
+        if(prop.cnf_handled_well())
+          prop.lcnf({!op1[idx], !op0[sum]});
+        else
+          prop.l_set_to_false(prop.land(op1[idx], op0[sum]));
+      }
     }
 
   return product;
@@ -1039,7 +1064,10 @@ bvt bv_utilst::absolute_value(const bvt &bv)
 
 bvt bv_utilst::cond_negate_no_overflow(const bvt &bv, literalt cond)
 {
-  prop.l_set_to_true(prop.limplies(cond, !overflow_negate(bv)));
+  if(prop.cnf_handled_well())
+    prop.lcnf({!cond, !overflow_negate(bv)});
+  else
+    prop.l_set_to_true(prop.limplies(cond, !overflow_negate(bv)));
 
   return cond_negate(bv, cond);
 }
@@ -1214,21 +1242,45 @@ void bv_utilst::unsigned_divider(
 
   bvt sum = adder_no_overflow(product, rem);
 
-  literalt is_equal=equal(sum, op0);
-
-  prop.l_set_to_true(prop.limplies(is_not_zero, is_equal));
+  if(prop.cnf_handled_well())
+  {
+    for(std::size_t i = 0; i < width; ++i)
+    {
+      prop.lcnf({!is_not_zero, !sum[i], op0[i]});
+      prop.lcnf({!is_not_zero, sum[i], !op0[i]});
+    }
+  }
+  else
+  {
+    literalt is_equal = equal(sum, op0);
+    prop.l_set_to_true(prop.limplies(is_not_zero, is_equal));
+  }
 
   // op1!=0 => rem < op1
 
-  prop.l_set_to_true(
-    prop.limplies(
+  if(prop.cnf_handled_well())
+  {
+    prop.lcnf(
+      {!is_not_zero, lt_or_le(false, rem, op1, representationt::UNSIGNED)});
+  }
+  else
+  {
+    prop.l_set_to_true(prop.limplies(
       is_not_zero, lt_or_le(false, rem, op1, representationt::UNSIGNED)));
+  }
 
   // op1!=0 => res <= op0
 
-  prop.l_set_to_true(
-    prop.limplies(
+  if(prop.cnf_handled_well())
+  {
+    prop.lcnf(
+      {!is_not_zero, lt_or_le(true, res, op0, representationt::UNSIGNED)});
+  }
+  else
+  {
+    prop.l_set_to_true(prop.limplies(
       is_not_zero, lt_or_le(true, res, op0, representationt::UNSIGNED)));
+  }
 }
 
 
diff --git a/src/solvers/prop/prop_conv_solver.cpp b/src/solvers/prop/prop_conv_solver.cpp
index 597f95c7067..08ede8b99f0 100644
--- a/src/solvers/prop/prop_conv_solver.cpp
+++ b/src/solvers/prop/prop_conv_solver.cpp
@@ -251,7 +251,10 @@ literalt prop_conv_solvert::convert_bool(const exprt &expr)
     for(unsigned i = 1; i < op_bv.size(); i++)
       b.push_back(prop.lequal(op_bv[0], op_bv[i]));
 
-    prop.l_set_to_true(prop.lor(b));
+    if(prop.cnf_handled_well())
+      prop.lcnf(b);
+    else
+      prop.l_set_to_true(prop.lor(b));
 
     return op_bv[0];
   }
diff --git a/src/solvers/refinement/refine_arithmetic.cpp b/src/solvers/refinement/refine_arithmetic.cpp
index d8241c7b0b8..5a53d5de30d 100644
--- a/src/solvers/refinement/refine_arithmetic.cpp
+++ b/src/solvers/refinement/refine_arithmetic.cpp
@@ -82,16 +82,31 @@ bvt bv_refinementt::convert_mult(const mult_exprt &expr)
     literalt op0_zero=bv_utils.is_zero(a.op0_bv);
     literalt op1_zero=bv_utils.is_zero(a.op1_bv);
     literalt res_zero=bv_utils.is_zero(a.result_bv);
-    prop.l_set_to_true(
-      prop.limplies(prop.lor(op0_zero, op1_zero), res_zero));
+    if(prop.cnf_handled_well())
+    {
+      prop.lcnf({!op0_zero, res_zero});
+      prop.lcnf({!op1_zero, res_zero});
+    }
+    else
+    {
+      prop.l_set_to_true(prop.limplies(prop.lor(op0_zero, op1_zero), res_zero));
+    }
 
     // x*1==x and 1*x==x
     literalt op0_one=bv_utils.is_one(a.op0_bv);
     literalt op1_one=bv_utils.is_one(a.op1_bv);
     literalt res_op0=bv_utils.equal(a.op0_bv, a.result_bv);
     literalt res_op1=bv_utils.equal(a.op1_bv, a.result_bv);
-    prop.l_set_to_true(prop.limplies(op0_one, res_op1));
-    prop.l_set_to_true(prop.limplies(op1_one, res_op0));
+    if(prop.cnf_handled_well())
+    {
+      prop.lcnf({!op0_one, res_op1});
+      prop.lcnf({!op1_one, res_op0});
+    }
+    else
+    {
+      prop.l_set_to_true(prop.limplies(op0_one, res_op1));
+      prop.l_set_to_true(prop.limplies(op1_one, res_op0));
+    }
   }
 
   return bv;
@@ -238,11 +253,16 @@ void bv_refinementt::check_SAT(approximationt &a)
       literalt result_equal=
         bv_utils.equal(a.result_bv, float_utils.build_constant(result));
 
-      literalt op0_and_op1_equal=
-        prop.land(op0_equal, op1_equal);
+      if(prop.cnf_handled_well())
+      {
+        prop.lcnf({!op0_equal, !op1_equal, result_equal});
+      }
+      else
+      {
+        literalt op0_and_op1_equal = prop.land(op0_equal, op1_equal);
 
-      prop.l_set_to_true(
-        prop.limplies(op0_and_op1_equal, result_equal));
+        prop.l_set_to_true(prop.limplies(op0_and_op1_equal, result_equal));
+      }
     }
     else
     {