Do not elimintae variables with unsatistiable bounds

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

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