diff options
Diffstat (limited to 'src/proof/sat_proof_implementation.h')
| -rw-r--r-- | src/proof/sat_proof_implementation.h | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h index 68050d93c..82e7cb7b2 100644 --- a/src/proof/sat_proof_implementation.h +++ b/src/proof/sat_proof_implementation.h @@ -565,6 +565,9 @@ ClauseId TSatProof<Solver>::registerUnitClause(typename Solver::TLit lit, if (kind == INPUT) { Assert(d_inputClauses.find(newId) == d_inputClauses.end()); + Debug("pf::sat") << "TSatProof::registerUnitClause: registering a new " + "input (UNIT CLAUSE): " + << lit << std::endl; d_inputClauses.insert(newId); } if (kind == THEORY_LEMMA) { |