From d05aee802bf93d23193739e8280d2ad5ce7e7469 Mon Sep 17 00:00:00 2001 From: Haniel Barbosa Date: Fri, 25 Sep 2020 12:24:06 -0300 Subject: Cleaning and documenting cnf stream (#5134) Moreover changes assertClause to return a bool, which is gonna be used by the proof cnf stream. --- src/theory/bv/bitblast/eager_bitblaster.cpp | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'src/theory/bv/bitblast/eager_bitblaster.cpp') 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() {} -- cgit v1.2.3