diff options
| author | Guy <katz911@gmail.com> | 2016-06-30 12:39:01 -0700 |
|---|---|---|
| committer | Guy <katz911@gmail.com> | 2016-06-30 12:39:01 -0700 |
| commit | e252f83e7298fdbad1ac8882763e7571e7a83235 (patch) | |
| tree | f0a26d7c1c5f67d5ebc45e1d8423c50dd8d6f554 /src/proof | |
| parent | 42eed1a8f72d4a5b9ac384100b42f7b0c8b46729 (diff) | |
| parent | 9b9e41478d0e1e62fa4bc8ca206a70dff5e8c392 (diff) | |
Merge branch 'master' of https://github.com/CVC4/CVC4
Diffstat (limited to 'src/proof')
| -rw-r--r-- | src/proof/theory_proof.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index eff0a8247..473152647 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -621,7 +621,7 @@ void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas, } } - Assert(found); + AlwaysAssert(found); Debug("pf::tp") << "Replacing theory assertion " << clause_expr[k] << " with " @@ -730,7 +730,7 @@ void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas, } } - Assert(found); + AlwaysAssert(found); Debug("pf::tp") << "Replacing theory assertion " << currentClauseExpr[k] |