From 1bf05d51ce6e4310ce42828102663276152b33f2 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Sun, 28 Nov 2021 16:35:04 -0500
Subject: [PATCH] fix(proof):  emit proper result for RUP steps

---
 src/sat/Solver.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/sat/Solver.ml b/src/sat/Solver.ml
index ce64cacd..226c29b8 100644
--- a/src/sat/Solver.ml
+++ b/src/sat/Solver.ml
@@ -1028,8 +1028,7 @@ module Make(Plugin : PLUGIN)
                         (Atom.debug_a store) atoms);
       let proof =
         let lits =
-          Clause.atoms_a store c
-          |> Iter.of_array
+          Iter.of_array atoms
           |> Iter.map (Atom.lit store)
         in
         Proof.emit_redundant_clause lits