Proof production bugfix (#887)

Author: omriisack

src/engine/PrecisionRestorer.cpp

@@ -134,16 +134,22 @@ void PrecisionRestorer::restorePrecision( IEngine &engine,
         }
     }
 
-    if ( engine.shouldProduceProofs() )
-        engine.setBoundExplainerContent( &boundExplainerBackup );
-
     for ( unsigned i = 0; i < targetN; ++i )
     {
+        if ( engine.shouldProduceProofs() )
+        {
+            engine.updateGroundUpperBound( i, groundUpperBoundsBackup[i] );
+            engine.updateGroundLowerBound( i, groundLowerBoundsBackup[i] );
+        }
+
         tableau.tightenUpperBoundNaively( i, upperBoundsBackup[i] );
         tableau.tightenLowerBoundNaively( i, lowerBoundsBackup[i] );
     }
 
-    engine.propagateBoundManagerTightenings();
+    if ( engine.shouldProduceProofs() )
+        engine.setBoundExplainerContent( &boundExplainerBackup );
+
+    tableau.updateVariablesToComplyWithBounds();
 
     // Restore constraint status
     for ( const auto &pair : targetEngineState._plConstraintToState )

src/engine/ReluConstraint.cpp

@@ -271,11 +271,11 @@ void ReluConstraint::notifyUpperBound( unsigned variable, double newBound )
                         _boundManager->tightenUpperBound( _b, bound, *_tighteningRow );
                     else
                     {
-                        if ( FloatUtils::isZero( bound ) )
+                        if ( !FloatUtils::isPositive( bound ) )
                             _boundManager->addLemmaExplanationAndTightenBound(
                                 _b, 0, Tightening::UB, { variable }, Tightening::UB, getType() );
                         // Bound cannot be negative if ReLU is inactive
-                        else if ( FloatUtils::isNegative( bound ) )
+                        if ( FloatUtils::isNegative( bound ) )
                             throw InfeasibleQueryException();
                     }
                 }
@@ -326,11 +326,11 @@ void ReluConstraint::notifyUpperBound( unsigned variable, double newBound )
                         _boundManager->tightenLowerBound( _b, -bound, *_tighteningRow );
                     else
                     {
-                        if ( FloatUtils::isZero( bound ) )
+                        if ( !FloatUtils::isPositive( bound ) )
                             _boundManager->addLemmaExplanationAndTightenBound(
                                 _b, 0, Tightening::LB, { variable }, Tightening::UB, getType() );
                         // Bound cannot be negative if ReLU is active
-                        else if ( FloatUtils::isNegative( bound ) )
+                        if ( FloatUtils::isNegative( bound ) )
                             throw InfeasibleQueryException();
                     }
                 }