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..bec26afb05 100644
--- a/src/engine/Preprocessor.cpp
+++ b/src/engine/Preprocessor.cpp
@@ -680,6 +680,11 @@ void Preprocessor::collectFixedValues()
         {
             _fixedVariables[i] = getLowerBound( i );
         }
+        else if ( FloatUtils::gt( getLowerBound( i ), getUpperBound( i ) ) )
+        {
+            // Infeasible condition over the variable
+            throw InfeasibleQueryException();
+        }
         else if ( !usedVariables.exists( i ) )
         {
             // If possible, choose a value that matches the debugging