1 files changed, 12 insertions, 3 deletions
diff --git a/src/proof/lrat/lrat_proof.cpp b/src/proof/lrat/lrat_proof.cpp
index ea03a9e20..6c2c5e2e8 100644
--- a/src/proof/lrat/lrat_proof.cpp
+++ b/src/proof/lrat/lrat_proof.cpp
@@ -25,6 +25,11 @@
 #include "base/cvc4_assert.h"
 #include "base/output.h"
 
+#if CVC4_USE_DRAT2ER
+#include "drat2er_options.h"
+#include "drat_trim_interface.h"
+#endif
+
 namespace CVC4 {
 namespace proof {
 namespace lrat {
@@ -221,9 +226,13 @@ LratProof LratProof::fromDratProof(
   dratStream << dratBinary;
   dratStream.close();
 
-  // TODO(aozdemir) Add invocation of DRAT trim, once I get CMake to bundle it
-  // into CVC4 correctly.
-  Unimplemented();
+#if CVC4_USE_DRAT2ER
+  drat2er::drat_trim::CheckAndConvertToLRAT(
+      formulaFilename, dratFilename, lratFilename, drat2er::options::QUIET);
+#else
+  Unimplemented("LRAT proof production requires drat2er.\n"
+      "Run contrib/get-drat2er, reconfigure with --drat2er, and rebuild");
+#endif
 
   std::ifstream lratStream(lratFilename);
   LratProof lrat(lratStream);