diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2020-09-25 12:24:06 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-25 12:24:06 -0300 |
| commit | d05aee802bf93d23193739e8280d2ad5ce7e7469 (patch) | |
| tree | 49156d00634f9e9db4279eb6bc2adcdee9ec1bfe /test/unit/prop | |
| parent | 96da64b450fc6dd6f5cf701587db38adbe8ba177 (diff) | |
Cleaning and documenting cnf stream (#5134)
Moreover changes assertClause to return a bool, which is gonna be used by the proof cnf stream.
Diffstat (limited to 'test/unit/prop')
| -rw-r--r-- | test/unit/prop/cnf_stream_white.h | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h index d64749d6b..ae79e1517 100644 --- a/test/unit/prop/cnf_stream_white.h +++ b/test/unit/prop/cnf_stream_white.h @@ -146,11 +146,11 @@ class CnfStreamWhite : public CxxTest::TestSuite { d_cnfContext = new context::Context(); d_cnfRegistrar = new theory::TheoryRegistrar(d_theoryEngine); ResourceManager* rm = d_smt->getResourceManager(); - d_cnfStream = new CVC4::prop::TseitinCnfStream(d_satSolver, - d_cnfRegistrar, - d_cnfContext, - &d_smt->getOutputManager(), - rm); + d_cnfStream = new CVC4::prop::CnfStream(d_satSolver, + d_cnfRegistrar, + d_cnfContext, + &d_smt->getOutputManager(), + rm); } void tearDown() override |