diff --git a/doc/man/cbmc.1 b/doc/man/cbmc.1
index d356eabf5ba..15fffbcf2c3 100644
--- a/doc/man/cbmc.1
+++ b/doc/man/cbmc.1
@@ -105,9 +105,6 @@ disable signed arithmetic over\- and underflow checks
 \fB\-\-no\-malloc\-may\-fail\fR
 do not allow malloc calls to fail by default
 .TP
-\fB\-\-no\-malloc\-fail\-null\fR
-do not set malloc failure mode to return null pointer
-.TP
 \fB\-\-no\-unwinding\-assertions\fR (\fBcbmc\fR\-only)
 do not generate unwinding assertions (cannot be
 used with \fB\-\-cover\fR)
diff --git a/doc/man/goto-analyzer.1 b/doc/man/goto-analyzer.1
index ea41841da47..a42eb3cc461 100644
--- a/doc/man/goto-analyzer.1
+++ b/doc/man/goto-analyzer.1
@@ -637,9 +637,6 @@ disable signed arithmetic over\- and underflow checks
 \fB\-\-no\-malloc\-may\-fail\fR
 do not allow malloc calls to fail by default
 .TP
-\fB\-\-no\-malloc\-fail\-null\fR
-do not set malloc failure mode to return null pointer
-.TP
 \fB\-\-no\-unwinding\-assertions\fR (\fBcbmc\fR\-only)
 do not generate unwinding assertions (cannot be
 used with \fB\-\-cover\fR)
diff --git a/doc/man/goto-instrument.1 b/doc/man/goto-instrument.1
index 6ecdb5efc37..88428b58c7c 100644
--- a/doc/man/goto-instrument.1
+++ b/doc/man/goto-instrument.1
@@ -697,6 +697,9 @@ set malloc failure mode to assert\-then\-assume
 \fB\-\-malloc\-fail\-null\fR
 set malloc failure mode to return null
 .TP
+\fB\-\-no\-malloc\-may\-fail\fR
+do not allow malloc calls to fail by default
+.TP
 \fB\-\-string\-abstraction\fR
 track C string lengths and zero\-termination
 .TP
diff --git a/regression/contracts-dfcc/chain.sh b/regression/contracts-dfcc/chain.sh
index 97f9afb5ab1..8b931718943 100755
--- a/regression/contracts-dfcc/chain.sh
+++ b/regression/contracts-dfcc/chain.sh
@@ -43,6 +43,10 @@ else
   $goto_cc -o "${name}${dfcc_suffix}.gb" "${name}.c"
 fi
 
+if [[ "${args_inst}" != *"malloc"* ]]; then
+  args_inst="--no-malloc-may-fail $args_inst"
+fi
+
 rm -f "${name}${dfcc_suffix}-mod.gb"
 $goto_instrument ${args_inst} "${name}${dfcc_suffix}.gb" "${name}${dfcc_suffix}-mod.gb"
 if [ ! -e "${name}${dfcc_suffix}-mod.gb" ] ; then
diff --git a/regression/goto-instrument/chain.sh b/regression/goto-instrument/chain.sh
index ed4fdbedc9d..96ebce32760 100755
--- a/regression/goto-instrument/chain.sh
+++ b/regression/goto-instrument/chain.sh
@@ -21,7 +21,7 @@ else
 fi
 
 rm -f "${target}-mod.gb"
-$goto_instrument ${args} "${target}.gb" "${target}-mod.gb"
+$goto_instrument --no-malloc-may-fail ${args} "${target}.gb" "${target}-mod.gb"
 if [ ! -e "${target}-mod.gb" ] ; then
   cp "${target}.gb" "${target}-mod.gb"
 elif echo $args | grep -q -- "--dump-c-type-header" ; then
@@ -39,5 +39,5 @@ elif echo $args | grep -q -- "--dump-c" ; then
 
   rm "${target}-mod.c"
 fi
-$goto_instrument --show-goto-functions "${target}-mod.gb"
+$goto_instrument --no-malloc-may-fail --show-goto-functions "${target}-mod.gb"
 $cbmc --no-standard-checks "${target}-mod.gb"
diff --git a/regression/goto-synthesizer/chain.sh b/regression/goto-synthesizer/chain.sh
index ed7c7fa498d..d6379cac470 100755
--- a/regression/goto-synthesizer/chain.sh
+++ b/regression/goto-synthesizer/chain.sh
@@ -37,7 +37,7 @@ fi
 rm -f "${name}-mod.gb"
 rm -f "${name}-mod-2.gb"
 echo "Running goto-instrument: "
-$goto_instrument ${args_inst} "${name}.gb" "${name}-mod.gb"
+$goto_instrument --no-malloc-may-fail ${args_inst} "${name}.gb" "${name}-mod.gb"
 if [ ! -e "${name}-mod.gb" ] ; then
   cp "$name.gb" "${name}-mod.gb"
 elif echo $args_inst | grep -q -- "--dump-c" ; then
@@ -53,9 +53,9 @@ elif echo $args_inst | grep -q -- "--dump-c" ; then
 fi
 echo "Running goto-synthesizer: "
 if echo $args_synthesizer | grep -q -- "--dump-loop-contracts" ; then
-  $goto_synthesizer ${args_synthesizer} "${name}-mod.gb"
+  $goto_synthesizer ${args_synthesizer} --no-malloc-may-fail "${name}-mod.gb"
 else
-  $goto_synthesizer ${args_synthesizer} "${name}-mod.gb" "${name}-mod-2.gb"
+  $goto_synthesizer ${args_synthesizer} --no-malloc-may-fail "${name}-mod.gb" "${name}-mod-2.gb"
   echo "Running CBMC: "
   $cbmc --no-standard-checks ${args_cbmc} "${name}-mod-2.gb"
 fi
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index d0bef5fa8a1..19f450e13c9 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -126,10 +126,28 @@ void cbmc_parse_optionst::set_default_analysis_flags(
   {
     options.set_option("unwinding-assertions", enabled);
   }
+
+  if(enabled)
+  {
+    config.ansi_c.malloc_may_fail = true;
+    config.ansi_c.malloc_failure_mode =
+      configt::ansi_ct::malloc_failure_modet::malloc_failure_mode_return_null;
+  }
+  else
+  {
+    config.ansi_c.malloc_may_fail = false;
+    config.ansi_c.malloc_failure_mode =
+      configt::ansi_ct::malloc_failure_modet::malloc_failure_mode_none;
+  }
 }
 
 void cbmc_parse_optionst::get_command_line_options(optionst &options)
 {
+  // Enable flags that in combination provide analysis with no surprises
+  // (expected checks and no unsoundness by missing checks).
+  cbmc_parse_optionst::set_default_analysis_flags(
+    options, !cmdline.isset("no-standard-checks"));
+
   if(config.set(cmdline))
   {
     usage_error();
@@ -366,11 +384,6 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     "self-loops-to-assumptions",
     !cmdline.isset("no-self-loops-to-assumptions"));
 
-  // Enable flags that in combination provide analysis with no surprises
-  // (expected checks and no unsoundness by missing checks).
-  cbmc_parse_optionst::set_default_analysis_flags(
-    options, !cmdline.isset("no-standard-checks"));
-
   // all (other) checks supported by goto_check
   PARSE_OPTIONS_GOTO_CHECK(cmdline, options);
 
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp
index 868d23e71f0..5fe19e6bd55 100644
--- a/src/goto-analyzer/goto_analyzer_parse_options.cpp
+++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp
@@ -68,6 +68,19 @@ void goto_analyzer_parse_optionst::set_default_analysis_flags(
   options.set_option("signed-overflow-check", enabled);
   options.set_option("undefined-shift-check", enabled);
 
+  if(enabled)
+  {
+    config.ansi_c.malloc_may_fail = true;
+    config.ansi_c.malloc_failure_mode =
+      configt::ansi_ct::malloc_failure_modet::malloc_failure_mode_return_null;
+  }
+  else
+  {
+    config.ansi_c.malloc_may_fail = false;
+    config.ansi_c.malloc_failure_mode =
+      configt::ansi_ct::malloc_failure_modet::malloc_failure_mode_none;
+  }
+
   // This is in-line with the options we set for CBMC in cbmc_parse_optionst
   // with the exception of unwinding-assertions, which don't make sense in
   // the context of abstract interpretation.
@@ -75,6 +88,9 @@ void goto_analyzer_parse_optionst::set_default_analysis_flags(
 
 void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
 {
+  goto_analyzer_parse_optionst::set_default_analysis_flags(
+    options, !cmdline.isset("no-standard-checks"));
+
   if(config.set(cmdline))
   {
     usage_error();
@@ -84,9 +100,6 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("function"))
     options.set_option("function", cmdline.get_value("function"));
 
-  goto_analyzer_parse_optionst::set_default_analysis_flags(
-    options, !cmdline.isset("no-standard-checks"));
-
   // all (other) checks supported by goto_check
   PARSE_OPTIONS_GOTO_CHECK(cmdline, options);
 
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h
index 0e55007c81c..a78643b12d7 100644
--- a/src/goto-analyzer/goto_analyzer_parse_options.h
+++ b/src/goto-analyzer/goto_analyzer_parse_options.h
@@ -89,6 +89,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H
 #define CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H
 
+#include <util/config.h>
 #include <util/parse_options.h>
 #include <util/timestamper.h>
 #include <util/ui_message.h>
@@ -152,6 +153,7 @@ class optionst;
   OPT_SHOW_GOTO_FUNCTIONS \
   OPT_SHOW_PROPERTIES \
   OPT_GOTO_CHECK \
+  OPT_CONFIG_LIBRARY \
   "(show-symbol-table)(show-parse-tree)" \
   "(property):" \
   "(verbosity):(version)" \
diff --git a/src/util/config.cpp b/src/util/config.cpp
index a390435b264..892ae6995a0 100644
--- a/src/util/config.cpp
+++ b/src/util/config.cpp
@@ -1126,7 +1126,15 @@ bool configt::set(const cmdlinet &cmdline)
   if(cmdline.isset("malloc-fail-assert"))
     ansi_c.malloc_failure_mode = ansi_c.malloc_failure_mode_assert_then_assume;
 
-  ansi_c.malloc_may_fail = cmdline.isset("malloc-may-fail");
+  if(cmdline.isset("malloc-may-fail"))
+  {
+    ansi_c.malloc_may_fail = true;
+  }
+  if(cmdline.isset("no-malloc-may-fail"))
+  {
+    ansi_c.malloc_may_fail = false;
+    ansi_c.malloc_failure_mode = ansi_ct::malloc_failure_mode_none;
+  }
 
   if(cmdline.isset("c89"))
     ansi_c.set_c89();
diff --git a/src/util/config.h b/src/util/config.h
index 0bfedadc627..253eedeeadb 100644
--- a/src/util/config.h
+++ b/src/util/config.h
@@ -71,10 +71,12 @@ class symbol_table_baset;
 
 #define OPT_CONFIG_LIBRARY                                                     \
   "(malloc-fail-assert)(malloc-fail-null)(malloc-may-fail)"                    \
+  "(no-malloc-may-fail)"                                                       \
   "(string-abstraction)"
 
 #define HELP_CONFIG_LIBRARY                                                    \
   " {y--malloc-may-fail} \t allow malloc calls to return a null pointer\n"     \
+  " {y--no-malloc-may-fail} \t disable potential malloc failure\n"             \
   " {y--malloc-fail-assert} \t "                                               \
   "set malloc failure mode to assert-then-assume\n"                            \
   " {y--malloc-fail-null} \t set malloc failure mode to return null\n"         \
@@ -271,7 +273,7 @@ class configt
     libt lib;
 
     bool string_abstraction;
-    bool malloc_may_fail = false;
+    bool malloc_may_fail = true;
 
     enum malloc_failure_modet
     {
@@ -280,7 +282,7 @@ class configt
       malloc_failure_mode_assert_then_assume = 2
     };
 
-    malloc_failure_modet malloc_failure_mode = malloc_failure_mode_none;
+    malloc_failure_modet malloc_failure_mode = malloc_failure_mode_return_null;
 
     static const std::size_t default_object_bits = 8;