diff --git a/regression/cbmc/argv2/main.i b/regression/cbmc/argv2/main.i
new file mode 100644
index 00000000000..56e9954c4ae
--- /dev/null
+++ b/regression/cbmc/argv2/main.i
@@ -0,0 +1,6 @@
+int main(int argc, char *argv[])
+{
+  __CPROVER_assert(
+    sizeof(char *) > sizeof(int) || argc < 0x7FFFFFFF,
+    "argc cannot reach INT_MAX on 32-bit systems");
+}
diff --git a/regression/cbmc/argv2/test.desc b/regression/cbmc/argv2/test.desc
new file mode 100644
index 00000000000..e41bbe1df7a
--- /dev/null
+++ b/regression/cbmc/argv2/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.i
+--32
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
diff --git a/regression/cbmc/multiple-goto-traces/test.desc b/regression/cbmc/multiple-goto-traces/test.desc
index f5009b36556..96a326299a7 100644
--- a/regression/cbmc/multiple-goto-traces/test.desc
+++ b/regression/cbmc/multiple-goto-traces/test.desc
@@ -5,7 +5,7 @@ activate-multi-line-match
 ^EXIT=10$
 ^SIGNAL=0$
 VERIFICATION FAILED
-Trace for main\.assertion\.1:(\n.*){22}  assertion 4 \!= argc(\n.*){5}Trace for main\.assertion\.3:(\n.*){36}  assertion argc != 4(\n.*){5}Trace for main\.assertion\.4:(\n.*){50}  assertion argc \+ 1 != 5
+Trace for main\.assertion\.1:((\n.*){19}|(\n.*){22})  assertion 4 \!= argc(\n.*){5}Trace for main\.assertion\.3:((\n.*){33}|(\n.*){36})  assertion argc != 4(\n.*){5}Trace for main\.assertion\.4:((\n.*){47}|(\n.*){50})  assertion argc \+ 1 != 5
 \*\* 3 of 4 failed
 --
 ^warning: ignoring
diff --git a/src/ansi-c/ansi_c_entry_point.cpp b/src/ansi-c/ansi_c_entry_point.cpp
index dcdbe610f2b..cd86dd1e71f 100644
--- a/src/ansi-c/ansi_c_entry_point.cpp
+++ b/src/ansi-c/ansi_c_entry_point.cpp
@@ -313,12 +313,10 @@ bool generate_ansi_c_start_function(
         init_code.add(code_assumet(std::move(ge)));
       }
 
+      if(config.ansi_c.max_argc.has_value())
       {
-        // assume argc is at most MAX/8-1
-        mp_integer upper_bound=
-          power(2, config.ansi_c.int_width-4);
-
-        exprt bound_expr=from_integer(upper_bound, argc_symbol.type);
+        exprt bound_expr =
+          from_integer(*config.ansi_c.max_argc, argc_symbol.type);
 
         binary_relation_exprt le(
           argc_symbol.symbol_expr(), ID_le, std::move(bound_expr));
diff --git a/src/util/config.cpp b/src/util/config.cpp
index 017c04c4a21..c39d528f129 100644
--- a/src/util/config.cpp
+++ b/src/util/config.cpp
@@ -1146,6 +1146,29 @@ bool configt::set(const cmdlinet &cmdline)
   if(cmdline.isset("cpp11"))
     cpp.set_cpp11();
 
+  // set the upper bound for argc
+  if(os == "windows")
+  {
+    // On Windows, CreateProcess accepts no more than 32767 characters, so make
+    // that a hard limit.
+    ansi_c.max_argc = mp_integer{32767};
+  }
+  else
+  {
+    // For other systems assume argc is no larger than the what would make argv
+    // consume all available memory space:
+    // 2^pointer_width / (pointer_width / char_width) is the maximum number of
+    // argv elements sysconf(ARG_MAX) is likely much lower than this, but we
+    // don't know that value for the verification target platform.
+    const auto pointer_bits_2log =
+      address_bits(ansi_c.pointer_width / ansi_c.char_width);
+    if(ansi_c.pointer_width - pointer_bits_2log <= ansi_c.int_width)
+    {
+      ansi_c.max_argc = power(2, config.ansi_c.int_width - pointer_bits_2log);
+    }
+    // otherwise we leave argc unconstrained
+  }
+
   return false;
 }
 
diff --git a/src/util/config.h b/src/util/config.h
index 471814e58f3..99549013784 100644
--- a/src/util/config.h
+++ b/src/util/config.h
@@ -258,6 +258,11 @@ class configt
     malloc_failure_modet malloc_failure_mode = malloc_failure_mode_none;
 
     static const std::size_t default_object_bits = 8;
+
+    /// Maximum value of argc, which is operating-systems dependent: Windows
+    /// limits the number of characters accepte by CreateProcess, and Unix
+    /// systems have sysconf(ARG_MAX).
+    optionalt<mp_integer> max_argc;
   } ansi_c;
 
   struct cppt