diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2019-10-30 15:27:10 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-10-30 15:27:10 -0700 |
commit | 43ab3f4cd1aa5549cb1aa3c20a2d589614bcb8fc (patch) | |
tree | cf7b5d7f73a4d4ddc34492334a7d0eb90b57b77b /src/proof/lrat | |
parent | 8dda9531995953c3cec094339002f2ee7cadae08 (diff) |
Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)
Diffstat (limited to 'src/proof/lrat')
-rw-r--r-- | src/proof/lrat/lrat_proof.cpp | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/src/proof/lrat/lrat_proof.cpp b/src/proof/lrat/lrat_proof.cpp index 1685ad1c3..4a19f07be 100644 --- a/src/proof/lrat/lrat_proof.cpp +++ b/src/proof/lrat/lrat_proof.cpp @@ -24,7 +24,7 @@ #include <sstream> #include <unordered_map> -#include "base/cvc4_assert.h" +#include "base/check.h" #include "base/output.h" #include "proof/dimacs.h" #include "proof/lfsc_proof_printer.h" @@ -151,9 +151,9 @@ LratProof LratProof::fromDratProof( drat2er::drat_trim::CheckAndConvertToLRAT( formulaFilename, dratFilename, lratFilename, drat2er::options::QUIET); #else - Unimplemented( - "LRAT proof production requires drat2er.\n" - "Run contrib/get-drat2er, reconfigure with --drat2er, and rebuild"); + Unimplemented() + << "LRAT proof production requires drat2er.\n" + << "Run contrib/get-drat2er, reconfigure with --drat2er, and rebuild"; #endif } @@ -221,7 +221,8 @@ LratProof::LratProof(std::istream& textualProof) SatLiteral lit; firstS >> lit; Trace("pf::lrat") << "First lit: " << lit << std::endl; - Assert(!firstS.fail(), "Couldn't parse first literal from addition line"); + Assert(!firstS.fail()) + << "Couldn't parse first literal from addition line"; SatClause clause; for (; lit != 0; textualProof >> lit) |