diff --git a/crates/primitives/src/algebra/field/emulated.rs b/crates/primitives/src/algebra/field/emulated.rs
index 48e73da9..7c945a1d 100644
--- a/crates/primitives/src/algebra/field/emulated.rs
+++ b/crates/primitives/src/algebra/field/emulated.rs
@@ -672,7 +672,10 @@ impl<Base: SonobeField, Target: SonobeField, const LHS_ALIGNED: bool>
             let y = compose(other.limbs.value().unwrap_or_default());
             Ok((
                 (x - y).div_floor(&m),
-                Bounds(self.lbound().div_floor(&m), self.ubound().div_floor(&m)),
+                Bounds(
+                    (self.lbound() - other.ubound()).div_floor(&m),
+                    (self.ubound() - other.lbound()).div_floor(&m),
+                ),
             ))
         })?;
 
@@ -768,20 +771,24 @@ impl<Base: SonobeField, Target: SonobeField> TwoStageFieldVar for LimbedVar<Base
 // Only implement `EqGadget` for aligned variables.
 impl<F: SonobeField, Cfg> EqGadget<F> for LimbedVar<F, Cfg, true> {
     fn is_eq(&self, other: &Self) -> Result<Boolean<F>, SynthesisError> {
-        let mut result = Boolean::TRUE;
         if self.limbs.len() != other.limbs.len() {
             return Err(SynthesisError::Unsatisfiable);
         }
         if self.bounds.len() != other.bounds.len() {
             return Err(SynthesisError::Unsatisfiable);
         }
+        let mut bits = vec![];
         for i in 0..self.limbs.len() {
             if self.bounds[i] != other.bounds[i] {
                 return Err(SynthesisError::Unsatisfiable);
             }
-            result &= self.limbs[i].is_eq(&other.limbs[i])?;
+            bits.push(self.limbs[i].is_eq(&other.limbs[i])?);
+        }
+        if bits.is_empty() {
+            Ok(Boolean::TRUE)
+        } else {
+            Boolean::kary_and(&bits)
         }
-        Ok(result)
     }
 
     fn enforce_equal(&self, other: &Self) -> Result<(), SynthesisError> {
@@ -800,22 +807,6 @@ impl<F: SonobeField, Cfg> EqGadget<F> for LimbedVar<F, Cfg, true> {
         Ok(())
     }
 
-    fn enforce_not_equal(&self, other: &Self) -> Result<(), SynthesisError> {
-        if self.limbs.len() != other.limbs.len() {
-            return Err(SynthesisError::Unsatisfiable);
-        }
-        if self.bounds.len() != other.bounds.len() {
-            return Err(SynthesisError::Unsatisfiable);
-        }
-        for i in 0..self.limbs.len() {
-            if self.bounds[i] != other.bounds[i] {
-                return Err(SynthesisError::Unsatisfiable);
-            }
-            self.limbs[i].enforce_not_equal(&other.limbs[i])?;
-        }
-        Ok(())
-    }
-
     fn conditional_enforce_equal(
         &self,
         other: &Self,
@@ -825,7 +816,7 @@ impl<F: SonobeField, Cfg> EqGadget<F> for LimbedVar<F, Cfg, true> {
             if should_enforce.value()? {
                 return self.enforce_equal(other);
             } else {
-                return self.enforce_not_equal(other);
+                return Ok(()); // No constraint when should_enforce is false
             }
         }
         self.is_eq(other)?
@@ -1114,8 +1105,8 @@ impl<F: SonobeField, G: SonobeField, Cfg> AllocVar<G, F> for LimbedVar<F, Cfg, t
             || {
                 f().map(|v| {
                     (
-                        BigInt::from_biguint(Sign::Plus, (*v.borrow()).into()),
-                        Bounds(Zero::zero(), G::MODULUS.into().into()),
+                        v.borrow().into_bigint().into().into(),
+                        Bounds(Zero::zero(), (-G::one()).into_bigint().into().into()),
                     )
                 })
             },