From 756c6d2ca5919bca2a6fde80a1f8c48a594284ae Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 16 May 2024 16:58:58 -0500
Subject: [PATCH] Fix DSL proof reconstruction for THEORY_REWRITE (#10773)

---
 src/rewriter/rewrite_db_proof_cons.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/rewriter/rewrite_db_proof_cons.cpp b/src/rewriter/rewrite_db_proof_cons.cpp
index 645c3e89d18..d3a3b7f3805 100644
--- a/src/rewriter/rewrite_db_proof_cons.cpp
+++ b/src/rewriter/rewrite_db_proof_cons.cpp
@@ -882,7 +882,7 @@ bool RewriteDbProofCons::ensureProofInternal(CDProof* cdp, const Node& eqi)
             else
             {
               Assert(pcur.d_id == RewriteProofStatus::THEORY_REWRITE);
-              pfac.push_back(cur[0]);
+              pfac.push_back(cur);
             }
           }
           // recurse on premises