Fix DSL proof reconstruction for THEORY_REWRITE (cvc5#10773)

ajreynol · May 16, 2024 · 756c6d2 · 756c6d2
1 parent 9a35285
commit 756c6d2
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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