diff --git a/src/math/polysat/forbidden_intervals.cpp b/src/math/polysat/forbidden_intervals.cpp
index 9586b820d..63b97ed5b 100644
--- a/src/math/polysat/forbidden_intervals.cpp
+++ b/src/math/polysat/forbidden_intervals.cpp
@@ -55,14 +55,7 @@ namespace polysat {
 
         _backtrack.released = true;
 
-
-        // a*v <= 0, a odd
-        if (ok1 && ok2 && match_zero(c, a1, b1, e1, a2, b2, e2, fi))
-            return true;
-
         // v > q
-        // 2^k*a*v + b > 0
-        // TODO: is !ok2 required?
         if (ok1 && !ok2 && match_non_zero(c, a1, b1, e1, fi))
             return true;
 
@@ -77,6 +70,14 @@ namespace polysat {
         SASSERT(b1.is_val());
         SASSERT(b2.is_val());
 
+        // a*v <= 0, a odd
+        if (match_zero(c, a1, b1, e1, a2, b2, e2, fi))
+            return true;
+
+        // a*v + b > 0, a odd
+        if (match_non_zero_linear(c, a1, b1, e1, a2, b2, e2, fi))
+            return true;
+
         if (match_linear1(c, a1, b1, e1, a2, b2, e2, fi))
             return true;
         if (match_linear2(c, a1, b1, e1, a2, b2, e2, fi))
@@ -271,6 +272,10 @@ namespace polysat {
     /**
      * a*v <= 0, a odd
      * forbidden interval for v is [1,0[
+     *
+     * TODO: extend to
+     * 2^k*a*v <= 0, a odd
+     * (using periodic intervals?)
      */
     bool forbidden_intervals::match_zero(
         signed_constraint const& c,
@@ -294,6 +299,42 @@ namespace polysat {
         return false;
     }
 
+    /**
+     * a*v + b > 0, a odd
+     *
+     * TODO: extend to
+     * 2^k*a*v + b > 0, a odd
+     * (using periodic intervals?)
+     */
+    bool forbidden_intervals::match_non_zero_linear(
+        signed_constraint const& c,
+        rational const & a1, pdd const& b1, pdd const& e1,
+        rational const & a2, pdd const& b2, pdd const& e2,
+        fi_record& fi) {
+        if (c.is_negative() && a1.is_odd() && a2.is_zero() && b2.is_zero()) {
+            // a*v + b > 0
+            // <=> a*v + b != 0
+            // <=> v + a^-1 * b != 0
+            // <=> v != - a^-1 * b
+            auto& m = e1.manager();
+            rational const& mod_value = m.two_to_N();
+            rational a1_inv;
+            VERIFY(a1.mult_inverse(m.power_of_2(), a1_inv));
+            rational lo_val(mod(-b1.val() * a1_inv, mod_value));
+            auto lo = -e1 * a1_inv;
+            rational hi_val(mod(lo_val + 1, mod_value));
+            auto hi = lo + 1;
+            fi.coeff = 1;
+            fi.interval = eval_interval::proper(lo, lo_val, hi, hi_val);
+            if (b1 != e1)
+                fi.side_cond.push_back(s.eq(b1, e1));
+            if (b2 != e2)
+                fi.side_cond.push_back(s.eq(b2, e2));
+            return true;
+        }
+        return false;
+    }
+
     /** 
      * v > q
      * forbidden interval for v is [0,1[
diff --git a/src/math/polysat/forbidden_intervals.h b/src/math/polysat/forbidden_intervals.h
index 4b8dc2d3e..2d88216d3 100644
--- a/src/math/polysat/forbidden_intervals.h
+++ b/src/math/polysat/forbidden_intervals.h
@@ -57,6 +57,11 @@ namespace polysat {
             rational const & a2, pdd const& b2, pdd const& e2,
             fi_record& fi);
 
+        bool match_non_zero_linear(signed_constraint const& c,
+            rational const & a1, pdd const& b1, pdd const& e1,
+            rational const & a2, pdd const& b2, pdd const& e2,
+            fi_record& fi);
+
         bool match_non_zero(signed_constraint const& c,
             rational const & a1, pdd const& b1, pdd const& e1,
             fi_record& fi);