diff --git a/infer/src/topl/Topl.ml b/infer/src/topl/Topl.ml
index 57d9b3c52..f8aac67be 100644
--- a/infer/src/topl/Topl.ml
+++ b/infer/src/topl/Topl.ml
@@ -39,14 +39,6 @@ let get_proc_attr proc_name =
   Option.map ~f:Procdesc.get_attributes (get_proc_desc proc_name)
 
 
-let max_args = ref 0
-
-let get_max_args () =
-  let instrument_max_args = !max_args in
-  let automaton_max_args = ToplAutomaton.max_args (Lazy.force automaton) in
-  Int.max instrument_max_args automaton_max_args
-
-
 let get_transitions_count () = ToplAutomaton.tcount (Lazy.force automaton)
 
 (** Checks whether the method name and the number of arguments matches the conditions in a
@@ -103,18 +95,15 @@ let call_execute loc =
   [|ToplUtils.topl_call dummy_ret_id Tvoid loc ToplName.execute []|]
 
 
-(* Side-effect: increases [!max_args] when it sees a call with more arguments. *)
 let instrument_instruction = function
   | Sil.Call ((ret_id, ret_typ), e_fun, arg_ts, loc, _call_flags) as i ->
       let active_transitions = get_active_transitions e_fun arg_ts in
       if not (Array.exists ~f:(fun x -> x) active_transitions) then [|i|]
-      else (
-        max_args := Int.max !max_args (List.length arg_ts) ;
-        tt "found %d arguments@\n" (List.length arg_ts) ;
+      else
         let i1s = set_transitions loc active_transitions in
         let i2s = call_save_args loc ret_id ret_typ arg_ts in
         let i3s = call_execute loc in
-        Array.concat [[|i|]; i1s; i2s; i3s] )
+        Array.concat [[|i|]; i1s; i2s; i3s]
   | i ->
       [|i|]
 
@@ -145,7 +134,7 @@ let add_types tenv =
     let state = (ToplUtils.make_field ToplName.state, Typ.mk (Tint IInt), []) in
     let retval = (ToplUtils.make_field ToplName.retval, ToplUtils.any_type, []) in
     let transitions = List.init (get_transitions_count ()) ~f:transition_field in
-    let saved_args = List.init (get_max_args ()) ~f:saved_arg_field in
+    let saved_args = List.init (ToplAutomaton.max_args (Lazy.force automaton)) ~f:saved_arg_field in
     let registers = List.map ~f:register_field (get_registers ()) in
     List.concat [[retval; state]; transitions; saved_args; registers]
   in
@@ -158,7 +147,7 @@ let instrument tenv procdesc =
     let f _node = instrument_instruction in
     tt "instrument@\n" ;
     let _updated = Procdesc.replace_instrs_by procdesc ~f in
-    tt "add types %d@\n" !max_args ; add_types tenv ; tt "done@\n" )
+    tt "add types@\n" ; add_types tenv ; tt "done@\n" )
 
 
 (** [lookup_static_var var prop] expects [var] to have the form [Exp.Lfield (obj, fieldname)], and
diff --git a/infer/src/topl/ToplMonitor.ml b/infer/src/topl/ToplMonitor.ml
index 40b428875..e00112355 100644
--- a/infer/src/topl/ToplMonitor.ml
+++ b/infer/src/topl/ToplMonitor.ml
@@ -198,14 +198,16 @@ let gen_maybe_call ret_id : node_generator =
 
 let arguments_count proc_name = List.length (Typ.Procname.get_parameters proc_name)
 
-(* NOTE: The order of parameters must correspond to what gets generated by [call_save_args]. *)
-let generate_save_args _automaton proc_name =
-  let n = arguments_count proc_name in
+(* NOTE: The order of parameters must correspond to what gets generated by [Topl.call_save_args]. *)
+let generate_save_args automaton proc_name =
+  if arguments_count proc_name < 1 then
+    L.die InternalError "ToplMonitor: saveArgs() needs at least one argument" ;
+  let n = Int.min (arguments_count proc_name - 1) (ToplAutomaton.max_args automaton) in
   let local_var = ToplUtils.local_var proc_name in
   procedure proc_name
     (sequence
        ( assign (ToplUtils.static_var ToplName.retval) (local_var (ToplName.arg 0))
-       :: List.init (n - 1) ~f:(fun i ->
+       :: List.init n ~f:(fun i ->
               assign
                 (ToplUtils.static_var (ToplName.saved_arg i))
                 (local_var (ToplName.arg (i + 1))) ) ))