From 4ffd8f60ea0e509b679d59e47aa1b7cdf882b825 Mon Sep 17 00:00:00 2001
From: Reuven Peleg <reuvenp@mobileye.com>
Date: Wed, 12 Feb 2025 08:44:06 +0200
Subject: [PATCH 1/2] Do not elimintae variables with unsatistiable bounds

Add a Python unit test testing that.
---
 maraboupy/test/test_core.py | 13 +++++++++++++
 src/engine/Preprocessor.cpp |  5 +++++
 2 files changed, 18 insertions(+)

diff --git a/maraboupy/test/test_core.py b/maraboupy/test/test_core.py
index bc90e13582..d136f8b13a 100644
--- a/maraboupy/test/test_core.py
+++ b/maraboupy/test/test_core.py
@@ -59,6 +59,19 @@ def test_solve_round_and_clip_unsat():
     assert(exitCode == "unsat")
 
 
+def test_unsolvable_elimination():
+    """ Test that unsatisfiable variables are not eliminated """
+    ipq = MarabouCore.InputQuery()
+    ipq.setNumberOfVariables(1)
+
+    ipq.setLowerBound(0, 1.0)
+    ipq.setUpperBound(0, -1.0)
+
+    exitCode, variables, stats = MarabouCore.solve(ipq, OPT)
+    print(variables)
+    assert(exitCode == "unsat")
+
+
 def test_solve_round_and_clip_sat():
     """
     -1 <= x0 <= 0
diff --git a/src/engine/Preprocessor.cpp b/src/engine/Preprocessor.cpp
index f8354575e2..d55214a739 100644
--- a/src/engine/Preprocessor.cpp
+++ b/src/engine/Preprocessor.cpp
@@ -680,6 +680,11 @@ void Preprocessor::collectFixedValues()
         {
             _fixedVariables[i] = getLowerBound( i );
         }
+        else if ( getLowerBound( i ) > getUpperBound( i ) )
+        {
+            // Insatifisfiable variable, don't eliminate
+            continue;
+        }
         else if ( !usedVariables.exists( i ) )
         {
             // If possible, choose a value that matches the debugging

From 15362484b4c8192d6ad7644d5fda0b76ecc28bf2 Mon Sep 17 00:00:00 2001
From: Reuven Peleg <reuvenp@mobileye.com>
Date: Sun, 16 Feb 2025 08:40:51 +0200
Subject: [PATCH 2/2] Immediately throw InfeasibleQueryException in case of
 conflicting bounds

---
 src/engine/Preprocessor.cpp | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/engine/Preprocessor.cpp b/src/engine/Preprocessor.cpp
index d55214a739..bec26afb05 100644
--- a/src/engine/Preprocessor.cpp
+++ b/src/engine/Preprocessor.cpp
@@ -680,10 +680,10 @@ void Preprocessor::collectFixedValues()
         {
             _fixedVariables[i] = getLowerBound( i );
         }
-        else if ( getLowerBound( i ) > getUpperBound( i ) )
+        else if ( FloatUtils::gt( getLowerBound( i ), getUpperBound( i ) ) )
         {
-            // Insatifisfiable variable, don't eliminate
-            continue;
+            // Infeasible condition over the variable
+            throw InfeasibleQueryException();
         }
         else if ( !usedVariables.exists( i ) )
         {