Respect the solve polarity for conditions that don't mention the var

src/Solve.cpp

@@ -1064,10 +1064,12 @@ class SolveForInterval : public IRVisitor {
         // and the rule for && will intersect the LHS with everything,
         // leaving the LHS as the final result.
         if (Expr cond = le; !expr_uses_var(cond, var)) {
+            // Respect the polarity we're solving for: under a negation we want
+            // the region where the condition is false.
             if (can_prove(cond)) {
-                result = Interval::everything();
+                result = target ? Interval::everything() : Interval::nothing();
             } else if (can_prove(!cond)) {
-                result = Interval::nothing();
+                result = target ? Interval::nothing() : Interval::everything();
             } else {
                 fail();
             }
@@ -1168,9 +1170,9 @@ class SolveForInterval : public IRVisitor {
         // See the analogous check in visit(const LE *).
         if (Expr cond = ge; !expr_uses_var(ge, var)) {
             if (can_prove(cond)) {
-                result = Interval::everything();
+                result = target ? Interval::everything() : Interval::nothing();
             } else if (can_prove(!cond)) {
-                result = Interval::nothing();
+                result = target ? Interval::nothing() : Interval::everything();
             } else {
                 fail();
             }

test/correctness/solve.cpp

@@ -634,6 +634,29 @@ void test_solve_far_side_min_max() {
                          Interval::neg_inf(), 11);
 }
 
+void test_solve_no_var_polarity() {
+    // A condition that doesn't mention the variable being solved for still has
+    // to respect the polarity we're solving for. Under a negation we want the
+    // region where the condition is false, so a provably-true subcondition
+    // contributes nothing rather than everything.
+    //
+    // All of these are tautologies, since a remainder mod 2 is always 0 or 1,
+    // so every value of x satisfies them.
+    Expr y = Variable::make(Int(32), "y");
+
+    // Only the outer interval is checked. An inner interval may always be
+    // conservatively empty, but an outer one that's empty claims the condition
+    // is nowhere true, which here would be wrong.
+    check_outer_interval(((y % 2) == 0) || ((y % 2) == 1),
+                         Interval::neg_inf(), Interval::pos_inf());
+
+    // The De Morgan dual of the above. The Not flips the polarity, and the
+    // comparisons underneath it are provable, so this used to come back as an
+    // empty interval.
+    check_outer_interval(!(((y % 2) != 1) && ((y % 2) != 0)),
+                         Interval::neg_inf(), Interval::pos_inf());
+}
+
 }  // namespace
 
 int main(int argc, char **argv) {
@@ -668,6 +691,7 @@ int main(int argc, char **argv) {
     test_float_select_condition_not_simplified();
     test_outer_interval_max_min();
     test_solve_far_side_min_max();
+    test_solve_no_var_polarity();
     std::printf("Success!\n");
     return 0;
 }