remove contradiction threshold

Author: OmriIsacHUJI

src/configuration/GlobalConfiguration.cpp

@@ -114,7 +114,6 @@ const unsigned GlobalConfiguration::DNC_DEPTH_THRESHOLD = 5;
 
 const double GlobalConfiguration::MINIMAL_COEFFICIENT_FOR_TIGHTENING = 0.01;
 const double GlobalConfiguration::LEMMA_CERTIFICATION_TOLERANCE = 0.00000001;
-const double GlobalConfiguration::CONTRADICTION_THRESHOLD = 0.000002;
 const bool GlobalConfiguration::WRITE_JSON_PROOF = false;
 const bool GlobalConfiguration::WRITE_ALETHE_PROOF = true;
 

src/configuration/GlobalConfiguration.h

@@ -251,10 +251,6 @@ class GlobalConfiguration
      */
     static const double LEMMA_CERTIFICATION_TOLERANCE;
 
-    /* A (negative) threshold to determine if a contradction is not to be considered
-     */
-    static const double CONTRADICTION_THRESHOLD;
-
     /* Denote whether proofs should be written as a JSON file
      */
     static const bool WRITE_JSON_PROOF;

src/engine/Engine.cpp

@@ -3499,7 +3499,7 @@ bool Engine::certifyInfeasibility( unsigned var ) const
         _groundBoundManager.getAllGroundBounds( Tightening::UB ).data(),
         _groundBoundManager.getAllGroundBounds( Tightening::LB ).data(),
         _tableau->getN() );
-    return FloatUtils::isNegative( derivedBound, GlobalConfiguration::CONTRADICTION_THRESHOLD );
+    return FloatUtils::isNegative( derivedBound );
 }
 
 double Engine::explainBound( unsigned var, bool isUpper ) const