From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Thu, 18 Nov 2021 17:28:50 +0000 (-0300)
Subject: [proofs] Fix trace in SatProofManager  (#7664)
X-Git-Tag: cvc5-1.0.0~799
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ae09936f4d732b460f493f32c9192223be867e1f;p=cvc5.git

[proofs] Fix trace in SatProofManager  (#7664)
---

diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp
index 0b3f28c61..e12b2cae9 100644
--- a/src/prop/sat_proof_manager.cpp
+++ b/src/prop/sat_proof_manager.cpp
@@ -356,7 +356,8 @@ void SatProofManager::explainLit(SatLiteral lit,
   if (d_assumptions.contains(litNode))
   {
     Trace("sat-proof")
-        << "SatProofManager::explainLit: input assumption, ABORT\n";
+        << "SatProofManager::explainLit: input assumption, ABORT\n"
+        << pop;
     return;
   }
   // We don't need to explain nodes who already have proofs.