diff options
Diffstat (limited to 'src/proof/proof_manager.cpp')
| -rw-r--r-- | src/proof/proof_manager.cpp | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index d8ab811bc..f2205e2ed 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -332,6 +332,9 @@ void ProofManager::traceUnsatCore() { d_satProof->collectClausesUsed(used_inputs, used_lemmas); + // At this point, there should be no assertions without a clause id + Assert(d_cnfProof->isAssertionStackEmpty()); + IdToSatClause::const_iterator it = used_inputs.begin(); for(; it != used_inputs.end(); ++it) { Node node = d_cnfProof->getAssertionForClause(it->first); |