Cleaning and documenting cnf stream (#5134)

Moreover changes assertClause to return a bool, which is gonna be used by the proof cnf stream.

1 files changed, 7 insertions, 7 deletions

diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp
index c48e20224..046ad4b1b 100644
--- a/src/theory/bv/bitblast/eager_bitblaster.cpp
+++ b/src/theory/bv/bitblast/eager_bitblaster.cpp
@@ -69,13 +69,13 @@ EagerBitblaster::EagerBitblaster(BVSolverLazy* theory_bv, context::Context* c)
   }
   d_satSolver.reset(solver);
   ResourceManager* rm = smt::currentResourceManager();
-  d_cnfStream.reset(new prop::TseitinCnfStream(d_satSolver.get(),
-                                               d_bitblastingRegistrar.get(),
-                                               d_nullContext.get(),
-                                               nullptr,
-                                               rm,
-                                               false,
-                                               "EagerBitblaster"));
+  d_cnfStream.reset(new prop::CnfStream(d_satSolver.get(),
+                                        d_bitblastingRegistrar.get(),
+                                        d_nullContext.get(),
+                                        nullptr,
+                                        rm,
+                                        false,
+                                        "EagerBitblaster"));
 }
 
 EagerBitblaster::~EagerBitblaster() {}