diff --git a/src/common/Statistics.cpp b/src/common/Statistics.cpp
index 667a852eb..b9f7e72e5 100644
--- a/src/common/Statistics.cpp
+++ b/src/common/Statistics.cpp
@@ -42,6 +42,8 @@ Statistics::Statistics()
     _unsignedAttributes[TOTAL_NUMBER_OF_VALID_CASE_SPLITS] = 0;
     _unsignedAttributes[NUM_CERTIFIED_LEAVES] = 0;
     _unsignedAttributes[NUM_DELEGATED_LEAVES] = 0;
+    _unsignedAttributes[NUM_LEMMAS] = 0;
+    _unsignedAttributes[CERTIFIED_UNSAT] = 0;
 
     _longAttributes[NUM_MAIN_LOOP_ITERATIONS] = 0;
     _longAttributes[NUM_SIMPLEX_STEPS] = 0;
@@ -425,6 +427,7 @@ void Statistics::print()
             getUnsignedAttribute( Statistics::NUM_CERTIFIED_LEAVES ) );
     printf( "\tNumber of leaves to delegate: %u\n",
             getUnsignedAttribute( Statistics::NUM_DELEGATED_LEAVES ) );
+    printf( "\tNumber of lemmas: %u\n", getUnsignedAttribute( Statistics::NUM_LEMMAS ) );
 }
 
 unsigned long long Statistics::getTotalTimeInMicro() const
diff --git a/src/common/Statistics.h b/src/common/Statistics.h
index 04c8f4356..4761594b4 100644
--- a/src/common/Statistics.h
+++ b/src/common/Statistics.h
@@ -67,9 +67,13 @@ class Statistics
         // branches of the search tree, that have since been popped)
         TOTAL_NUMBER_OF_VALID_CASE_SPLITS,
 
-        // Total number of delegated and certified leaves in the search tree
+        // Total number of delegated leaves, certified leaves and lemmas in the search tree
         NUM_CERTIFIED_LEAVES,
         NUM_DELEGATED_LEAVES,
+        NUM_LEMMAS,
+
+        // 1 if returned UNSAT and proof was certified by proof checker, 0 otherwise.
+        CERTIFIED_UNSAT,
     };
 
     enum StatisticsLongAttribute {
diff --git a/src/engine/BoundManager.cpp b/src/engine/BoundManager.cpp
index 6b6200cc5..5c8c9d156 100644
--- a/src/engine/BoundManager.cpp
+++ b/src/engine/BoundManager.cpp
@@ -469,7 +469,7 @@ bool BoundManager::addLemmaExplanationAndTightenBound( unsigned var,
                                                                         affectedVarBound,
                                                                         allExplanations,
                                                                         constraintType );
-        _engine->getUNSATCertificateCurrentPointer()->addPLCLemma( PLCExpl );
+        _engine->addPLCLemma( PLCExpl );
         affectedVarBound == Tightening::UB ? _engine->updateGroundUpperBound( var, value )
                                            : _engine->updateGroundLowerBound( var, value );
         resetExplanation( var, affectedVarBound );
diff --git a/src/engine/Engine.cpp b/src/engine/Engine.cpp
index 2a0b7242c..15facd1fe 100644
--- a/src/engine/Engine.cpp
+++ b/src/engine/Engine.cpp
@@ -3733,6 +3733,7 @@ bool Engine::certifyUNSATCertificate()
     if ( certificationSucceeded )
     {
         printf( "Certified\n" );
+        _statistics.incUnsignedAttribute( Statistics::CERTIFIED_UNSAT );
         if ( _statistics.getUnsignedAttribute( Statistics::NUM_DELEGATED_LEAVES ) )
             printf( "Some leaves were delegated and need to be certified separately by an SMT "
                     "solver\n" );
@@ -3867,3 +3868,13 @@ void Engine::extractBounds( IQuery &inputQuery )
         }
     }
 }
+
+void Engine::addPLCLemma( std::shared_ptr<PLCLemma> &explanation )
+{
+    if ( !_produceUNSATProofs )
+        return;
+
+    ASSERT( explanation && _UNSATCertificate && _UNSATCertificateCurrentPointer )
+    _statistics.incUnsignedAttribute( Statistics::NUM_LEMMAS );
+    _UNSATCertificateCurrentPointer->get()->addPLCLemma( explanation );
+}
\ No newline at end of file
diff --git a/src/engine/Engine.h b/src/engine/Engine.h
index 934769c8d..a3ea1c22d 100644
--- a/src/engine/Engine.h
+++ b/src/engine/Engine.h
@@ -300,6 +300,11 @@ class Engine
     */
     void propagateBoundManagerTightenings();
 
+    /*
+      Add lemma to the UNSAT Certificate
+    */
+    void addPLCLemma( std::shared_ptr<PLCLemma> &explanation );
+
 private:
     enum BasisRestorationRequired {
         RESTORATION_NOT_NEEDED = 0,
diff --git a/src/engine/IEngine.h b/src/engine/IEngine.h
index 9b9108b20..ea592bb4e 100644
--- a/src/engine/IEngine.h
+++ b/src/engine/IEngine.h
@@ -19,6 +19,7 @@
 #include "BoundExplainer.h"
 #include "DivideStrategy.h"
 #include "List.h"
+#include "PlcLemma.h"
 #include "SnCDivideStrategy.h"
 #include "TableauStateStorageLevel.h"
 #include "Vector.h"
@@ -31,6 +32,7 @@
 class EngineState;
 class Equation;
 class PiecewiseLinearCaseSplit;
+class PLCLemma;
 class SmtState;
 class String;
 class PiecewiseLinearConstraint;
@@ -184,6 +186,11 @@ class IEngine
       Propagate bound tightenings stored in the BoundManager
     */
     virtual void propagateBoundManagerTightenings() = 0;
+
+    /*
+      Add lemma to the UNSAT Certificate
+    */
+    virtual void addPLCLemma( std::shared_ptr<PLCLemma> &explanation ) = 0;
 };
 
 #endif // __IEngine_h__
diff --git a/src/engine/tests/MockEngine.h b/src/engine/tests/MockEngine.h
index eaeee8b89..4bab58130 100644
--- a/src/engine/tests/MockEngine.h
+++ b/src/engine/tests/MockEngine.h
@@ -286,6 +286,10 @@ class MockEngine : public IEngine
     {
         return true;
     }
+
+    void addPLCLemma( std::shared_ptr<PLCLemma> & /*explanation*/ )
+    {
+    }
 };
 
 #endif // __MockEngine_h__