diff --git a/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml b/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml
index f15cf481..8f893058 100644
--- a/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml
+++ b/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml
@@ -1545,6 +1545,8 @@ object (self)
 
   method is_register_variable = varmgr#is_register_variable
 
+  method is_stackpointer_variable = varmgr#is_stackpointer_variable
+
   method is_initial_register_value = varmgr#is_initial_register_value
 
   method is_initial_mips_argument_value = varmgr#is_initial_mips_argument_value
diff --git a/CodeHawk/CHB/bchlib/bCHLibTypes.mli b/CodeHawk/CHB/bchlib/bCHLibTypes.mli
index c9698e62..a8975447 100644
--- a/CodeHawk/CHB/bchlib/bCHLibTypes.mli
+++ b/CodeHawk/CHB/bchlib/bCHLibTypes.mli
@@ -3564,6 +3564,7 @@ object ('a)
 
   method is_auxiliary_variable: bool
   method is_register_variable: bool
+  method is_stackpointer_variable: bool
   method is_mips_argument_variable: bool
   method is_arm_argument_variable: bool
   method is_arm_extension_register_variable: bool
@@ -3949,6 +3950,10 @@ object
   (** Returns [true] if [var] is a register variable (of any architecture). *)
   method is_register_variable: variable_t -> bool
 
+  (** Returns [true] if [var] is a register used as a stackpointer (in the
+      current architecture). *)
+  method is_stackpointer_variable: variable_t -> bool
+
   (** Returns the register associated with [var].
 
       Returns [Error] if [var] is not a register variable or [var] cannot be
@@ -4452,6 +4457,10 @@ class type function_environment_int =
     (** Returns [true] if [var] is a register variable (of any architecture). *)
     method is_register_variable: variable_t -> bool
 
+    (** Returns [true] if [var] is a register variable that used by the current
+        architecture as a stackpointer. *)
+    method is_stackpointer_variable: variable_t -> bool
+
     (** Returns the register associated with [var].
 
         Returns [Error] if [var] is not a register variable or [var] cannot be
diff --git a/CodeHawk/CHB/bchlib/bCHVariable.ml b/CodeHawk/CHB/bchlib/bCHVariable.ml
index c5e891f2..b474b7a6 100644
--- a/CodeHawk/CHB/bchlib/bCHVariable.ml
+++ b/CodeHawk/CHB/bchlib/bCHVariable.ml
@@ -420,6 +420,11 @@ object (self:'a)
   method is_register_variable =
     match denotation with RegisterVariable _ -> true | _ -> false
 
+  method is_stackpointer_variable =
+    match denotation with
+    | RegisterVariable r -> BCHCPURegisters.is_stackpointer_register r
+    | _ -> false
+
   method is_mips_argument_variable =
     match denotation with
     | RegisterVariable reg ->
@@ -927,6 +932,10 @@ object (self)
     tfold_default
       (fun av -> av#is_register_variable) false (self#get_variable v)
 
+  method is_stackpointer_variable (v: variable_t) =
+    tfold_default
+      (fun av -> av#is_stackpointer_variable) false (self#get_variable v)
+
   method is_mips_argument_variable (v:variable_t) =
     tfold_default
       (fun av -> av#is_mips_argument_variable) false (self#get_variable v)
diff --git a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml
index 8887c822..083a13cd 100644
--- a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml
+++ b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml
@@ -597,6 +597,9 @@ let translate_arm_instruction
         let xw = inv#rewrite_expr x in
         let xs = simplify_xpr xw in
         let disvars = inv#get_init_disequalities in
+        let disvars =
+          List.filter
+            (fun v -> not (floc#f#env#is_initial_stackpointer_value v)) disvars in
         let is_disvar v = List.exists (fun vv -> v#equal vv) disvars in
         let xprvars = floc#env#variables_in_expr xs in
         let vars =