From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Thu, 2 Dec 2021 16:43:10 +0000 (-0300)
Subject: [proofs] Fix a trace in SAT proof manager (#7732)
X-Git-Tag: cvc5-1.0.0~736
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9d563b2963835b2a4e6ab19bdf5a5b21d934416e;p=cvc5.git

[proofs] Fix a trace in SAT proof manager (#7732)
---

diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp
index e12b2cae9..fb37b1d01 100644
--- a/src/prop/sat_proof_manager.cpp
+++ b/src/prop/sat_proof_manager.cpp
@@ -450,7 +450,8 @@ void SatProofManager::explainLit(SatLiteral lit,
       Trace("sat-proof") << "SatProofManager::explainLit:   " << children[i];
       if (i > 0)
       {
-        Trace("sat-proof") << " [" << args[i - 1] << "]";
+        Trace("sat-proof") << " [" << args[(2 * i) - 2] << ", "
+                           << args[(2 * i) - 1] << "]";
       }
       Trace("sat-proof") << "\n";
     }