diff --git a/src/th-lra/Sidekick_lra.ml b/src/th-lra/Sidekick_lra.ml
index 4699d9ee..0f9911eb 100644
--- a/src/th-lra/Sidekick_lra.ml
+++ b/src/th-lra/Sidekick_lra.ml
@@ -237,8 +237,12 @@ module Make(A : ARG) : S with module A = A = struct
              | exception Not_found -> ()
              | (pred, a, b) ->
                let pred = if sign then pred else FM.Pred.neg pred in
-               let c = FM_A.Constr.mk ~tag:lit pred a b in
-               FM_A.assert_c fm c;
+               if pred = Neq then (
+                 Log.debugf 50 (fun k->k "skip neq in %a" T.pp t);
+               ) else (
+                 let c = FM_A.Constr.mk ~tag:lit pred a b in
+                 FM_A.assert_c fm c;
+               )
            end)
     end;
     Log.debug 5 "lra: call arith solver";
diff --git a/src/th-lra/fourier_motzkin.ml b/src/th-lra/fourier_motzkin.ml
index 1b4ecc8e..91d894f5 100644
--- a/src/th-lra/fourier_motzkin.ml
+++ b/src/th-lra/fourier_motzkin.ml
@@ -248,7 +248,7 @@ module Make(A : ARG)
   }
 
   let add_sys (sys:system) (c:Constr.t) : system =
-    assert (match c.pred with Eq|Neq|Lt -> true | _ -> false);
+    assert (match c.pred with Eq|Leq|Lt -> true | _ -> false);
     if Constr.is_trivial c then (
       Log.debugf 10 (fun k->k"(@[FM.drop-trivial@ %a@])" Constr.pp c);
       sys