diff --git a/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml b/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml
index 6e7d68d2..f15cf481 100644
--- a/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml
+++ b/CodeHawk/CHB/bchlib/bCHFunctionInfo.ml
@@ -850,6 +850,7 @@ object (self)
            ?(size=4)
            ?(offset=NoOffset)
            (base: numerical_t): variable_t traceresult =
+    let base = base#modulo (mkNumerical BCHDoubleword.e32) in
     match numerical_to_doubleword base with
     | Error e -> Error ("finfo.mk_global_variable" :: e)
     | Ok addr ->
@@ -1276,6 +1277,9 @@ object (self)
   method get_memvar_offset (v:variable_t): memory_offset_t traceresult =
     varmgr#get_memvar_offset v
 
+  method has_variable_index_offset (v: variable_t): bool =
+    varmgr#has_variable_index_offset v
+
   method get_memval_offset (v:variable_t): memory_offset_t traceresult =
     varmgr#get_memval_offset v
 
diff --git a/CodeHawk/CHB/bchlib/bCHLibTypes.mli b/CodeHawk/CHB/bchlib/bCHLibTypes.mli
index 3605873e..c9698e62 100644
--- a/CodeHawk/CHB/bchlib/bCHLibTypes.mli
+++ b/CodeHawk/CHB/bchlib/bCHLibTypes.mli
@@ -3888,6 +3888,8 @@ object
       not a memory variable. *)
   method get_memvar_offset: variable_t -> memory_offset_t traceresult
 
+  method has_variable_index_offset: variable_t -> bool
+
   (** [get_memval_reference var] returns the base memory reference of
       memory-variable value [var].
 
@@ -4429,6 +4431,8 @@ class type function_environment_int =
         Returns [Error] if [index] is not a valid index of a memory reference. *)
     method is_unknown_reference: int -> bool traceresult
 
+    method has_variable_index_offset: variable_t -> bool
+
 
     (** {2 Memory address variables} *)
 
diff --git a/CodeHawk/CHB/bchlib/bCHLocationInvariant.ml b/CodeHawk/CHB/bchlib/bCHLocationInvariant.ml
index 44e954a9..2bf469ff 100644
--- a/CodeHawk/CHB/bchlib/bCHLocationInvariant.ml
+++ b/CodeHawk/CHB/bchlib/bCHLocationInvariant.ml
@@ -804,7 +804,7 @@ object (self)
                  STR "Variable does not have an initial value: ";
 		 var#toPretty]))
 
-  method get_init_disequalities =
+  method get_init_disequalities: variable_t list =
     let result = ref [] in
     let add v = result := v :: !result in
     let _ = H.iter (fun _ facts ->
@@ -813,7 +813,7 @@ object (self)
 	facts) table in
     !result
 
-  method get_init_equalities =
+  method get_init_equalities: variable_t list =
     let result = ref [] in
     let add v = result := v :: !result in
     let _ = H.iter (fun _ facts ->
diff --git a/CodeHawk/CHB/bchlib/bCHVariable.ml b/CodeHawk/CHB/bchlib/bCHVariable.ml
index c43fc692..c5e891f2 100644
--- a/CodeHawk/CHB/bchlib/bCHVariable.ml
+++ b/CodeHawk/CHB/bchlib/bCHVariable.ml
@@ -573,6 +573,11 @@ object (self)
       (fun av -> av#get_memory_offset)
       (self#get_variable v)
 
+  method has_variable_index_offset (v: variable_t): bool =
+    match self#get_memvar_offset v with
+    | Ok (IndexOffset (v, _, _)) -> self#is_register_variable v
+    | _ -> false
+
   method get_memval_offset (v: variable_t): memory_offset_t traceresult =
     tbind
       ~msg:"varmgr:get_memval_offset"
diff --git a/CodeHawk/CHB/bchlib/bCHVersion.ml b/CodeHawk/CHB/bchlib/bCHVersion.ml
index 1e1e39b1..0f71599b 100644
--- a/CodeHawk/CHB/bchlib/bCHVersion.ml
+++ b/CodeHawk/CHB/bchlib/bCHVersion.ml
@@ -95,8 +95,8 @@ end
 
 
 let version = new version_info_t 
-  ~version:"0.6.0_20241103"
-  ~date:"2024-11-03"
+  ~version:"0.6.0_20241111"
+  ~date:"2024-11-11"
   ~licensee: None
   ~maxfilesize: None
   ()
diff --git a/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml b/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml
index bf093576..4ec4ef47 100644
--- a/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml
+++ b/CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml
@@ -1828,6 +1828,52 @@ object (self)
            xd#index_xpr result;
            xd#index_xpr rresult])
 
+      | SignedMultiplyWordB (c, rd, rn, rm) ->
+         let vrd = rd#to_variable floc in
+         let xrn = rn#to_expr floc in
+         let xrm = rm#to_expr floc in
+         let xe16 = int_constant_expr BCHDoubleword.e16 in
+         let result = XOp (XMult, [xrn; XOp (XMod, [xrm; xe16])]) in
+         let xxrn = rewrite_expr xrn in
+         let xxrm = rewrite_expr xrm in
+         let rresult = rewrite_expr ?restrict:(Some 4) result in
+         let rdefs = [get_rdef xrn; get_rdef xrm] @ (get_all_rdefs rresult) in
+         let uses = [get_def_use vrd] in
+         let useshigh = [get_def_use_high vrd] in
+         let (tagstring, args) =
+           mk_instrx_data
+             ~vars:[vrd]
+             ~xprs:[xrn; xrm; result; rresult; xxrn; xxrm]
+             ~rdefs
+             ~uses
+             ~useshigh
+             () in
+         let (tags, args) = add_optional_instr_condition tagstring args c in
+         (tags, args)
+
+      | SignedMultiplyWordT (c, rd, rn, rm) ->
+         let vrd = rd#to_variable floc in
+         let xrn = rn#to_expr floc in
+         let xrm = rm#to_expr floc in
+         let xe16 = int_constant_expr BCHDoubleword.e16 in
+         let result = XOp (XMult, [xrn; XOp (XShiftrt, [xrm; xe16])]) in
+         let xxrn = rewrite_expr xrn in
+         let xxrm = rewrite_expr xrm in
+         let rresult = rewrite_expr ?restrict:(Some 4) result in
+         let rdefs = [get_rdef xrn; get_rdef xrm] @ (get_all_rdefs rresult) in
+         let uses = [get_def_use vrd] in
+         let useshigh = [get_def_use_high vrd] in
+         let (tagstring, args) =
+           mk_instrx_data
+             ~vars:[vrd]
+             ~xprs:[xrn; xrm; result; rresult; xxrn; xxrm]
+             ~rdefs
+             ~uses
+             ~useshigh
+             () in
+         let (tags, args) = add_optional_instr_condition tagstring args c in
+         (tags, args)
+
       | StoreMultipleDecrementBefore (wback, c, base, rl, _) ->
          let basereg = base#get_register in
          let regcount = rl#get_register_count in
diff --git a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml
index 45647924..8887c822 100644
--- a/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml
+++ b/CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml
@@ -591,14 +591,33 @@ let translate_arm_instruction
              rvar :: rsvar :: acc
           | _ -> acc) [] ops in
 
-  let get_use_high_vars (xprs: xpr_t list): variable_t list =
+  let get_use_high_vars ?(is_pop=false) (xprs: xpr_t list): variable_t list =
     let inv = floc#inv in
     List.fold_left (fun acc x ->
         let xw = inv#rewrite_expr x in
         let xs = simplify_xpr xw in
+        let disvars = inv#get_init_disequalities 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 =
-          List.filter (fun v -> not (floc#f#env#is_function_initial_value v))
-            (floc#env#variables_in_expr xs) in
+          if List.exists is_disvar xprvars && not is_pop then
+            let _ =
+              chlog#add
+                "get_use_high_vars:basic"
+                (LBLOCK [
+                     floc#l#toPretty;
+                     STR "  ";
+                     x2p xs;
+                     STR " ==> ";
+                     x2p x;
+                     pretty_print_list
+                       (floc#env#variables_in_expr x)
+                       (fun v -> v#toPretty)
+                       " [" "; " "]"]) in
+            floc#env#variables_in_expr x
+          else
+            List.filter (fun v -> not (floc#f#env#is_function_initial_value v))
+              xprvars in
         vars @ acc) [] xprs in
 
   let get_addr_use_high_vars (xprs: xpr_t list): variable_t list =
@@ -1618,7 +1637,9 @@ let translate_arm_instruction
      let usevars = get_register_vars [rn; rm] in
      let memvar = mem#to_variable floc in
      let (usevars, usehigh) =
-       if memvar#isTmp || floc#f#env#is_unknown_memory_variable memvar then
+       if memvar#isTmp
+          || floc#f#env#is_unknown_memory_variable memvar
+          || floc#f#env#has_variable_index_offset memvar then
          (* elevate address variables to high-use *)
          let xrn = rn#to_expr floc in
          let xrm = rm#to_expr floc in
@@ -2144,7 +2165,7 @@ let translate_arm_instruction
              let stackvar = stackop#to_variable floc in
              let stackrhs = stackop#to_expr floc in
              let (regvar, cmds1) = floc#get_ssa_assign_commands reg stackrhs in
-             let usehigh = get_use_high_vars [stackrhs] in
+             let usehigh = get_use_high_vars ~is_pop:true [stackrhs] in
              let defcmds1 =
                floc#get_vardef_commands
                  ~defs:[regvar; splhs]
@@ -2589,6 +2610,44 @@ let translate_arm_instruction
       | ACCAlways -> default cmds
       | _ -> make_conditional_commands c cmds)
 
+  | SignedMultiplyWordB (c, rd, rn, rm) ->
+     let floc = get_floc loc in
+     let rdreg = rd#to_register in
+     let (vrd, cmds) = floc#get_ssa_abstract_commands rdreg () in
+     let xrn = rn#to_expr floc in
+     let xrm = rm#to_expr floc in
+     let usevars = get_register_vars [rn; rm] in
+     let usehigh = get_use_high_vars [xrn; xrm] in
+     let defcmds =
+       floc#get_vardef_commands
+         ~defs:[vrd]
+         ~use:usevars
+         ~usehigh:usehigh
+         ctxtiaddr in
+     let cmds = defcmds @ cmds in
+     (match c with
+      | ACCAlways -> default cmds
+      | _ -> make_conditional_commands c cmds)
+
+  | SignedMultiplyWordT (c, rd, rn, rm) ->
+     let floc = get_floc loc in
+     let rdreg = rd#to_register in
+     let (vrd, cmds) = floc#get_ssa_abstract_commands rdreg () in
+     let xrn = rn#to_expr floc in
+     let xrm = rm#to_expr floc in
+     let usevars = get_register_vars [rn; rm] in
+     let usehigh = get_use_high_vars [xrn; xrm] in
+     let defcmds =
+       floc#get_vardef_commands
+         ~defs:[vrd]
+         ~use:usevars
+         ~usehigh:usehigh
+         ctxtiaddr in
+     let cmds = defcmds @ cmds in
+     (match c with
+      | ACCAlways -> default cmds
+      | _ -> make_conditional_commands c cmds)
+
   (* ---------------------------------------- StoreMultipleIncrementAfter --
    * Stores multiple registers to consecutive memoy locations using an address
    * from a base register. The consecutive memory locations start at this
diff --git a/CodeHawk/CHT/CHB_tests/bchlibarm32_tests/txbchlibarm32/bCHARMConditionalExprTest.ml b/CodeHawk/CHT/CHB_tests/bchlibarm32_tests/txbchlibarm32/bCHARMConditionalExprTest.ml
index 73da5140..7d48a36e 100644
--- a/CodeHawk/CHT/CHB_tests/bchlibarm32_tests/txbchlibarm32/bCHARMConditionalExprTest.ml
+++ b/CodeHawk/CHT/CHB_tests/bchlibarm32_tests/txbchlibarm32/bCHARMConditionalExprTest.ml
@@ -183,9 +183,12 @@ let compare_negative_tests () =
   end
 
 
+(* move-bne-x should ideally produce: R5 != -1 *)
 let move_tests () =
   let tests = [
-      ("move-bne", "0x100b0", "0x100b4", "0500b0e1bcffff1a", 3, "(R5 != 0)")
+      ("move-bne", "0x100b0", "0x100b4", "0500b0e1bcffff1a", 3, "(R5 != 0)");
+      ("move-bne-x", "0x100b0", "0x100bc", "0050a0e30500b0e1015045e2bcffff1a", 8,
+       "(R5_val_0x100b4_amp_0x100bc != 0)")
     ] in
   begin
     TS.new_testsuite (testname ^ "_subtract_tests") lastupdated;