diff --git a/doc/man/cbmc.1 b/doc/man/cbmc.1
index 8722b40ada9..d356eabf5ba 100644
--- a/doc/man/cbmc.1
+++ b/doc/man/cbmc.1
@@ -8,6 +8,12 @@ cbmc \- Bounded Model Checker for C/C++ and Java programs
 
 .B cbmc [--all-properties] \fIfile.c\fB ...
 
+.B cbmc [--no-standard-checks] \fIfile.c\fB ...
+
+.B cbmc [--no-standard-checks] [--pointer-check] \fIfile.c\fB ...
+
+.B cbmc [--no-bounds-check] \fIfile.c\fB ...
+
 .B goto-cc [-I \fIinclude-path\fB] [-c] \fIfile.c\fB [-o \fIoutfile.o\fB]
 
 .B goto-instrument \fIinfile\fB \fIoutfile\fR
@@ -41,8 +47,79 @@ The usual flow is to (1) translate source into a GOTO binary using
 goto-cc, then (2) perform instrumentation with goto-instrument, and
 finally (3) perform the analysis with cbmc.
 .SH OPTIONS
+.SS "Standard Checks"
+From version \fB6.0\fR onwards, \fBcbmc\fR, \fBgoto-analyzer\fR and some other tools
+apply some checks to the program by default (called the "standard checks"), with the
+aim to provide a better user experience for a non-expert user of the tool. These checks are:
+.TP
+\fB\-\-pointer\-check\fR
+enable pointer checks
+.TP
+\fB\-\-bounds\-check\fR
+enable array bounds checks
+.TP
+\fB\-\-undefined\-shift\-check\fR
+check shift greater than bit\-width
+.TP
+\fB\-\-div\-by\-zero\-check\fR
+enable division by zero checks
+.TP
+\fB\-\-pointer\-primitive\-check\fR
+checks that all pointers in pointer primitives are valid or null
+.TP
+\fB\-\-signed\-overflow\-check\fR
+enable signed arithmetic over\- and underflow checks
+.TP
+\fB\-\-malloc\-may\-fail\fR
+allow malloc calls to return a null pointer
+.TP
+\fB\-\-malloc\-fail\-null\fR
+set malloc failure mode to return null
+.TP
+\fB\-\-unwinding\-assertions\fR (\fBcbmc\fR\-only)
+generate unwinding assertions (cannot be
+used with \fB\-\-cover\fR)
+.PP
+These checks can all be deactivated at once by using the \fB\-\-no\-standard\-checks\fR flag
+like in the header example, or individually, by prepending a \fBno\-\fR before the flag, like
+so:
+.TP
+\fB\-\-no\-pointer\-check\fR
+disable pointer checks
+.TP
+\fB\-\-no\-bounds\-check\fR
+disable array bounds checks
+.TP
+\fB\-\-no\-undefined\-shift\-check\fR
+do not perform check for shift greater than bit\-width
+.TP
+\fB\-\-no\-div\-by\-zero\-check\fR
+disable division by zero checks
+.TP
+\fB\-\-no\-pointer\-primitive\-check\fR
+do not check that all pointers in pointer primitives are valid or null
+.TP
+\fB\-\-no\-signed\-overflow\-check\fR
+disable signed arithmetic over\- and underflow checks
+.TP
+\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)
+.PP
+If an already set flag is re-set, like calling \fB\-\-pointer\-check\fR
+when default checks are already on, the flag is simply ignored.
 .SS "Analysis options:"
 .TP
+\fB\-\-no\-standard\-checks\fR
+disable the standard (default) checks applied to a C/GOTO program
+(see above for more information)
+.TP
 \fB\-\-show\-properties\fR
 show the properties, but don't run analysis
 .TP
diff --git a/doc/man/goto-analyzer.1 b/doc/man/goto-analyzer.1
index bfa40f426f7..ea41841da47 100644
--- a/doc/man/goto-analyzer.1
+++ b/doc/man/goto-analyzer.1
@@ -8,6 +8,12 @@ goto-analyzer \- Data-flow analysis for C programs and goto binaries
 
 .B goto\-analyzer [options] file.c|file.gb
 
+.B goto\-analyzer [--no-standard-checks] \fIfile.c\fB ...
+
+.B goto\-analyzer [--no-standard-checks] [--pointer-check] \fIfile.c\fB ...
+
+.B goto\-analyzer [--no-bounds-check] \fIfile.c\fB ...
+
 .SH DESCRIPTION
 .B goto-analyzer
 is an abstract interpreter which uses the same
@@ -494,6 +500,10 @@ list loaded goto functions
 show the properties, but don't run analysis
 .SS "Program instrumentation options:"
 .TP
+\fB\-\-no\-standard\-checks\fR
+disable the standard (default) checks applied to a C/GOTO program
+(see below for more information)
+.TP
 \fB\-\-property\fR id
 enable selected properties only
 .TP
@@ -569,6 +579,73 @@ set malloc failure mode to return null
 .TP
 \fB\-\-string\-abstraction\fR
 track C string lengths and zero\-termination
+.SS "Standard Checks"
+From version \fB6.0\fR onwards, \fBcbmc\fR, \fBgoto-analyzer\fR and some other tools
+apply some checks to the program by default (called the "standard checks"), with the
+aim to provide a better user experience for a non-expert user of the tool. These checks are:
+.TP
+\fB\-\-pointer\-check\fR
+enable pointer checks
+.TP
+\fB\-\-bounds\-check\fR
+enable array bounds checks
+.TP
+\fB\-\-undefined\-shift\-check\fR
+check shift greater than bit\-width
+.TP
+\fB\-\-div\-by\-zero\-check\fR
+enable division by zero checks
+.TP
+\fB\-\-pointer\-primitive\-check\fR
+checks that all pointers in pointer primitives are valid or null
+.TP
+\fB\-\-signed\-overflow\-check\fR
+enable signed arithmetic over\- and underflow checks
+.TP
+\fB\-\-malloc\-may\-fail\fR
+allow malloc calls to return a null pointer
+.TP
+\fB\-\-malloc\-fail\-null\fR
+set malloc failure mode to return null
+.TP
+\fB\-\-unwinding\-assertions\fR (\fBcbmc\fR\-only)
+generate unwinding assertions (cannot be
+used with \fB\-\-cover\fR)
+.PP
+These checks can all be deactivated at once by using the \fB\-\-no\-standard\-checks\fR flag
+like in the header example, or individually, by prepending a \fBno\-\fR before the flag, like
+so:
+.TP
+\fB\-\-no\-pointer\-check\fR
+disable pointer checks
+.TP
+\fB\-\-no\-bounds\-check\fR
+disable array bounds checks
+.TP
+\fB\-\-no\-undefined\-shift\-check\fR
+do not perform check for shift greater than bit\-width
+.TP
+\fB\-\-no\-div\-by\-zero\-check\fR
+disable division by zero checks
+.TP
+\fB\-\-no\-pointer\-primitive\-check\fR
+do not check that all pointers in pointer primitives are valid or null
+.TP
+\fB\-\-no\-signed\-overflow\-check\fR
+disable signed arithmetic over\- and underflow checks
+.TP
+\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)
+.PP
+If an already set flag is re-set, like calling \fB\-\-pointer\-check\fR
+when default checks are already on, the flag is simply ignored.
 .SS "Other options:"
 .TP
 \fB\-\-validate\-goto\-model\fR
diff --git a/regression/acceleration/accelerate.sh b/regression/acceleration/accelerate.sh
index c8598419ef0..7b1f17cf908 100755
--- a/regression/acceleration/accelerate.sh
+++ b/regression/acceleration/accelerate.sh
@@ -16,7 +16,7 @@ is_windows=$4
 shift 4
 
 cfile=""
-cbmcargs=""
+cbmcargs="--no-standard-checks"
 
 # create the temporary directory relative to the current directory, thus
 # avoiding file names that start with a "/", which confuses goto-cl (Windows)
diff --git a/regression/book-examples/CMakeLists.txt b/regression/book-examples/CMakeLists.txt
index d61cfb85b92..88cf52769ec 100644
--- a/regression/book-examples/CMakeLists.txt
+++ b/regression/book-examples/CMakeLists.txt
@@ -13,19 +13,19 @@ else()
 endif()
 
 add_test_pl_tests(
-    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation" -X smt-backend ${gcc_only} ${exclude_win_broken_tests}
+    "$<TARGET_FILE:cbmc> --no-standard-checks --validate-goto-model --validate-ssa-equation" -X smt-backend ${gcc_only} ${exclude_win_broken_tests}
 )
 
 add_test_pl_profile(
     "book-examples-paths-lifo"
-    "$<TARGET_FILE:cbmc> --paths lifo"
+    "$<TARGET_FILE:cbmc> --no-standard-checks --paths lifo"
     "-C;-X;thorough-paths;-X;smt-backend;-X;paths-lifo-expected-failure;${gcc_only_string}-s;paths-lifo;${exclude_win_broken_tests_string}"
     "CORE"
 )
 
 add_test_pl_profile(
     "book-examples-cprover-smt2"
-    "$<TARGET_FILE:cbmc> --cprover-smt2"
+    "$<TARGET_FILE:cbmc> --no-standard-checks --cprover-smt2"
     "-C;-X;broken-smt-backend;-X;thorough-smt-backend;-X;broken-cprover-smt-backend;-X;thorough-cprover-smt-backend;${gcc_only_string}-s;cprover-smt2;${exclude_win_broken_tests_string}"
     "CORE"
 )
@@ -33,7 +33,7 @@ add_test_pl_profile(
 # If `-X` (exclude flag) is passed, test.pl will exclude the tests matching the label following it.
 add_test_pl_profile(
   "book-examples-new-smt-backend"
-  "$<TARGET_FILE:cbmc> --incremental-smt2-solver 'z3 --smt2 -in'"
+  "$<TARGET_FILE:cbmc> --no-standard-checks --incremental-smt2-solver 'z3 --smt2 -in'"
   "${gcc_only_string}-X;no-new-smt;-s;new-smt-backend"
   "CORE"
 )
diff --git a/regression/book-examples/Makefile b/regression/book-examples/Makefile
index e5777ce8774..969a26ca813 100644
--- a/regression/book-examples/Makefile
+++ b/regression/book-examples/Makefile
@@ -10,27 +10,27 @@ GCC_ONLY =
 endif
 
 test:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" -X smt-backend $(GCC_ONLY)
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --validate-goto-model --validate-ssa-equation" -X smt-backend $(GCC_ONLY)
 
 test-cprover-smt2:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --cprover-smt2" \
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --cprover-smt2" \
 					  -X broken-smt-backend -X thorough-smt-backend \
 					  -X broken-cprover-smt-backend -X thorough-cprover-smt-backend \
 					  -s cprover-smt2 $(GCC_ONLY)
 
 test-z3:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --z3" \
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --z3" \
 					  -X broken-smt-backend -X thorough-smt-backend \
 					  -X broken-z3-smt-backend -X thorough-z3-smt-backend \
 					  -s z3 $(GCC_ONLY)
 
 test-paths-lifo:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --paths lifo" \
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --paths lifo" \
 					  -X thorough-paths -X smt-backend -X paths-lifo-expected-failure \
 					  -s paths-lifo $(GCC_ONLY)
 
 test-new-smt-backend:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'z3 --smt2 -in'" \
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --incremental-smt2-solver 'z3 --smt2 -in'" \
 					  -X no-new-smt \
 					  -s new-smt-backend $(GCC_ONLY)
 
diff --git a/regression/cbmc-concurrency/CMakeLists.txt b/regression/cbmc-concurrency/CMakeLists.txt
index 2071288ffd8..f4a9787031e 100644
--- a/regression/cbmc-concurrency/CMakeLists.txt
+++ b/regression/cbmc-concurrency/CMakeLists.txt
@@ -1,11 +1,11 @@
 if((NOT WIN32) AND (NOT APPLE))
 add_test_pl_tests(
-    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation"
+    "$<TARGET_FILE:cbmc> --no-standard-checks --validate-goto-model --validate-ssa-equation"
 )
 else()
 add_test_pl_profile(
     "cbmc-concurrency"
-    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation"
+    "$<TARGET_FILE:cbmc> --no-standard-checks --validate-goto-model --validate-ssa-equation"
     "-C;-X;pthread"
     "CORE"
 )
diff --git a/regression/cbmc-concurrency/Makefile b/regression/cbmc-concurrency/Makefile
index bd3ca1bdf60..2f8153fc7c3 100644
--- a/regression/cbmc-concurrency/Makefile
+++ b/regression/cbmc-concurrency/Makefile
@@ -10,10 +10,10 @@ ifeq ($(filter-out OSX MSVC,$(BUILD_ENV_)),)
 endif
 
 test:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" $(no_pthread)
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --validate-goto-model --validate-ssa-equation" $(no_pthread)
 
 tests.log: ../test.pl
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" $(no_pthread)
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --validate-goto-model --validate-ssa-equation" $(no_pthread)
 
 clean:
 	find . -name '*.out' -execdir $(RM) '{}' \;
diff --git a/regression/cbmc-cover/CMakeLists.txt b/regression/cbmc-cover/CMakeLists.txt
index 93d5ee716c2..5e2a1847360 100644
--- a/regression/cbmc-cover/CMakeLists.txt
+++ b/regression/cbmc-cover/CMakeLists.txt
@@ -1,3 +1,3 @@
 add_test_pl_tests(
-    "$<TARGET_FILE:cbmc>"
+    "$<TARGET_FILE:cbmc> --no-standard-checks"
 )
diff --git a/regression/cbmc-cover/Makefile b/regression/cbmc-cover/Makefile
index 1a63894412b..82aa192b5ad 100644
--- a/regression/cbmc-cover/Makefile
+++ b/regression/cbmc-cover/Makefile
@@ -1,10 +1,10 @@
 default: tests.log
 
 test:
-	@../test.pl -e -p -c ../../../src/cbmc/cbmc
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks"
 
 tests.log: ../test.pl
-	@../test.pl -e -p -c ../../../src/cbmc/cbmc
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks"
 
 clean:
 	find . -name '*.out' -execdir $(RM) '{}' \;
diff --git a/regression/cbmc-cpp/CMakeLists.txt b/regression/cbmc-cpp/CMakeLists.txt
index 4d141f395e6..72ba751bca3 100644
--- a/regression/cbmc-cpp/CMakeLists.txt
+++ b/regression/cbmc-cpp/CMakeLists.txt
@@ -5,5 +5,5 @@ else()
 endif()
 
 add_test_pl_tests(
-    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation" ${gcc_only}
+    "$<TARGET_FILE:cbmc> --no-standard-checks --validate-goto-model --validate-ssa-equation" ${gcc_only}
 )
diff --git a/regression/cbmc-cpp/Makefile b/regression/cbmc-cpp/Makefile
index b08769d4551..2ad6fbdcac6 100644
--- a/regression/cbmc-cpp/Makefile
+++ b/regression/cbmc-cpp/Makefile
@@ -8,10 +8,10 @@ ifeq ($(BUILD_ENV_),MSVC)
 endif
 
 test:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" $(excluded_tests)
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --validate-goto-model --validate-ssa-equation" $(excluded_tests)
 
 tests.log: ../test.pl
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" $(excluded_tests)
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --validate-goto-model --validate-ssa-equation" $(excluded_tests)
 
 clean:
 	find . -name '*.out' -execdir $(RM) '{}' \;
diff --git a/regression/cbmc-incr-oneloop/CMakeLists.txt b/regression/cbmc-incr-oneloop/CMakeLists.txt
index 33d24bd6b3b..476a5d9f5d8 100644
--- a/regression/cbmc-incr-oneloop/CMakeLists.txt
+++ b/regression/cbmc-incr-oneloop/CMakeLists.txt
@@ -1,3 +1,3 @@
 add_test_pl_tests(
-    "perl ../timeout.pl 8 $<TARGET_FILE:cbmc> --slice-formula"
+    "perl ../timeout.pl 8 $<TARGET_FILE:cbmc> --no-standard-checks --slice-formula"
 )
diff --git a/regression/cbmc-incr-oneloop/Makefile b/regression/cbmc-incr-oneloop/Makefile
index 35d25c57e2c..750ca5aca2a 100644
--- a/regression/cbmc-incr-oneloop/Makefile
+++ b/regression/cbmc-incr-oneloop/Makefile
@@ -2,10 +2,10 @@ default: tests.log
 
 # Note the `perl -e` serves the purpose of providing timeout
 test:
-	@../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 15 ../../../src/cbmc/cbmc --slice-formula"
+	@../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 15 ../../../src/cbmc/cbmc --no-standard-checks --slice-formula"
 
 tests.log: ../test.pl
-	@../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 15 ../../../src/cbmc/cbmc --slice-formula"
+	@../test.pl -c "perl -e 'alarm shift @ARGV; exec @ARGV' 15 ../../../src/cbmc/cbmc --no-standard-checks --slice-formula"
 
 clean:
 	@$(RM) *.log
diff --git a/regression/cbmc-incr-smt2/CMakeLists.txt b/regression/cbmc-incr-smt2/CMakeLists.txt
index 2e8e54e434c..ddce0eab71b 100644
--- a/regression/cbmc-incr-smt2/CMakeLists.txt
+++ b/regression/cbmc-incr-smt2/CMakeLists.txt
@@ -1,13 +1,13 @@
 add_test_pl_profile(
     "cbmc-incr-smt2-z3"
-    "$<TARGET_FILE:cbmc> --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation"
+    "$<TARGET_FILE:cbmc> --no-standard-checks --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation"
     "-C;-s;new-smt-z3"
     "CORE"
 )
 
 add_test_pl_profile(
     "cbmc-incr-smt2-cvc5"
-    "$<TARGET_FILE:cbmc> --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --validate-goto-model --validate-ssa-equation"
+    "$<TARGET_FILE:cbmc> --no-standard-checks --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --validate-goto-model --validate-ssa-equation"
     "-C;-s;new-smt-cvc5"
     "CORE"
 )
diff --git a/regression/cbmc-incr-smt2/Makefile b/regression/cbmc-incr-smt2/Makefile
index 9a5b8bf4195..f766292bc22 100644
--- a/regression/cbmc-incr-smt2/Makefile
+++ b/regression/cbmc-incr-smt2/Makefile
@@ -6,10 +6,10 @@ include ../../src/common
 test: test.z3 test.cvc5
 
 test.z3:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation"
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation"
 
 test.cvc5:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --validate-goto-model --validate-ssa-equation"
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --validate-goto-model --validate-ssa-equation"
 
 tests.log: ../test.pl test
 
diff --git a/regression/cbmc-incr/CMakeLists.txt b/regression/cbmc-incr/CMakeLists.txt
index aad62741a82..636afd1a7b6 100644
--- a/regression/cbmc-incr/CMakeLists.txt
+++ b/regression/cbmc-incr/CMakeLists.txt
@@ -1,3 +1,3 @@
 add_test_pl_tests(
-    "perl ../timeout.pl 30 $<TARGET_FILE:cbmc> --incremental --magic-numbers"
+    "perl ../timeout.pl 30 $<TARGET_FILE:cbmc> --no-standard-checks --incremental --magic-numbers"
 )
diff --git a/regression/cbmc-incr/Makefile b/regression/cbmc-incr/Makefile
index 1de65b50102..5113fb4050b 100644
--- a/regression/cbmc-incr/Makefile
+++ b/regression/cbmc-incr/Makefile
@@ -1,6 +1,6 @@
 default: tests.log
 
-PARAM = --incremental --magic-numbers
+PARAM = --incremental --magic-numbers --no-standard-checks
 # --refine   --slice-formula
 
 test:
diff --git a/regression/cbmc-library/CMakeLists.txt b/regression/cbmc-library/CMakeLists.txt
index f523261d1aa..9e76346fe05 100644
--- a/regression/cbmc-library/CMakeLists.txt
+++ b/regression/cbmc-library/CMakeLists.txt
@@ -1,11 +1,11 @@
 if(NOT WIN32)
 add_test_pl_tests(
-    "$<TARGET_FILE:cbmc>"
+    "$<TARGET_FILE:cbmc> --no-standard-checks"
 )
 else()
 add_test_pl_profile(
     "cbmc-library"
-    "$<TARGET_FILE:cbmc>"
+    "$<TARGET_FILE:cbmc> --no-standard-checks"
     "-C;-X;unix;-X;gcc-only"
     "CORE"
 )
diff --git a/regression/cbmc-library/Makefile b/regression/cbmc-library/Makefile
index e82cb289424..3389cea12c8 100644
--- a/regression/cbmc-library/Makefile
+++ b/regression/cbmc-library/Makefile
@@ -9,10 +9,10 @@ ifeq ($(BUILD_ENV_),MSVC)
 endif
 
 test:
-	@../test.pl -e -p -c ../../../src/cbmc/cbmc $(unix_only) $(gcc_only)
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks" $(unix_only) $(gcc_only)
 
 tests.log: ../test.pl
-	@../test.pl -e -p -c ../../../src/cbmc/cbmc $(unix_only) $(gcc_only)
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks" $(unix_only) $(gcc_only)
 
 clean:
 	find . -name '*.out' -execdir $(RM) '{}' \;
diff --git a/regression/cbmc-primitives/CMakeLists.txt b/regression/cbmc-primitives/CMakeLists.txt
index 331c1cd1fe2..f8cd4322355 100644
--- a/regression/cbmc-primitives/CMakeLists.txt
+++ b/regression/cbmc-primitives/CMakeLists.txt
@@ -2,18 +2,18 @@ find_program(Z3_EXISTS "z3")
 message(${Z3_EXISTS})
 if(Z3_EXISTS)
     add_test_pl_tests(
-        "$<TARGET_FILE:cbmc>"
+        "$<TARGET_FILE:cbmc> --no-standard-checks"
     )
 
     # If `-X` (exclude flag) is passed, test.pl will exclude the tests matching the label following it.
     add_test_pl_profile(
             "cbmc-primitives-new-smt-backend"
-            "$<TARGET_FILE:cbmc> --incremental-smt2-solver 'z3 --smt2 -in'"
+            "$<TARGET_FILE:cbmc> --no-standard-checks --incremental-smt2-solver 'z3 --smt2 -in'"
             "-X;no-new-smt;-s;new-smt-backend"
             "CORE"
     )
 else()
     add_test_pl_tests(
-        "$<TARGET_FILE:cbmc>" -X smt-backend
+        "$<TARGET_FILE:cbmc> --no-standard-checks" -X smt-backend
     )
 endif()
diff --git a/regression/cbmc-primitives/Makefile b/regression/cbmc-primitives/Makefile
index e60c0d87ca5..2c9885222db 100644
--- a/regression/cbmc-primitives/Makefile
+++ b/regression/cbmc-primitives/Makefile
@@ -1,13 +1,13 @@
 default: tests.log
 
 test:
-	@../test.pl -e -p -c ../../../src/cbmc/cbmc
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks"
 
 test.smt2_incr:
-	@../test.pl -e -p -X no-new-smt -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation"
+	@../test.pl -e -p -X no-new-smt -c "../../../src/cbmc/cbmc --no-standard-checks --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation"
 
 tests.log: ../test.pl
-	@../test.pl -e -p -c ../../../src/cbmc/cbmc
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks"
 
 clean:
 	find . -name '*.out' -execdir $(RM) '{}' \;
diff --git a/regression/cbmc-sequentialization/CMakeLists.txt b/regression/cbmc-sequentialization/CMakeLists.txt
index 761fc6bca19..4d532a9d46e 100644
--- a/regression/cbmc-sequentialization/CMakeLists.txt
+++ b/regression/cbmc-sequentialization/CMakeLists.txt
@@ -1,10 +1,10 @@
 if(NOT WIN32)
   add_test_pl_tests(
-          "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation"
+          "$<TARGET_FILE:cbmc> --no-standard-checks --validate-goto-model --validate-ssa-equation"
   )
 else()
   add_test_pl_tests(
-          "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation"
+          "$<TARGET_FILE:cbmc> --no-standard-checks --validate-goto-model --validate-ssa-equation"
           -X requires_posix_only_headers
   )
 endif()
diff --git a/regression/cbmc-sequentialization/Makefile b/regression/cbmc-sequentialization/Makefile
index 672dac210bb..fa2c53859e2 100644
--- a/regression/cbmc-sequentialization/Makefile
+++ b/regression/cbmc-sequentialization/Makefile
@@ -10,7 +10,7 @@ POSIX_ONLY =
 endif
 
 test:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" $(POSIX_ONLY)
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --validate-goto-model --validate-ssa-equation" $(POSIX_ONLY)
 
 tests.log: ../test.pl test
 
diff --git a/regression/cbmc-shadow-memory/CMakeLists.txt b/regression/cbmc-shadow-memory/CMakeLists.txt
index 93d5ee716c2..5e2a1847360 100644
--- a/regression/cbmc-shadow-memory/CMakeLists.txt
+++ b/regression/cbmc-shadow-memory/CMakeLists.txt
@@ -1,3 +1,3 @@
 add_test_pl_tests(
-    "$<TARGET_FILE:cbmc>"
+    "$<TARGET_FILE:cbmc> --no-standard-checks"
 )
diff --git a/regression/cbmc-shadow-memory/Makefile b/regression/cbmc-shadow-memory/Makefile
index d86a43477e6..63237f82e69 100644
--- a/regression/cbmc-shadow-memory/Makefile
+++ b/regression/cbmc-shadow-memory/Makefile
@@ -1,13 +1,13 @@
 default: tests.log
 
 test:
-	@../test.pl -p -c ../../../src/cbmc/cbmc -X smt-backend
+	@../test.pl -p -c "../../../src/cbmc/cbmc --no-standard-checks" -X smt-backend
 
 test-cprover-smt2:
-	@../test.pl -p -c "../../../src/cbmc/cbmc --cprover-smt2"
+	@../test.pl -p -c "../../../src/cbmc/cbmc --no-standard-checks --cprover-smt2"
 
 tests.log: ../test.pl
-	@../test.pl -p -c ../../../src/cbmc/cbmc -X smt-backend
+	@../test.pl -p -c "../../../src/cbmc/cbmc --no-standard-checks" -X smt-backend
 
 show:
 	@for dir in *; do \
diff --git a/regression/cbmc-shadow-memory/strdup1/main.c b/regression/cbmc-shadow-memory/strdup1/main.c
index b937b83bc97..fd23e37436c 100644
--- a/regression/cbmc-shadow-memory/strdup1/main.c
+++ b/regression/cbmc-shadow-memory/strdup1/main.c
@@ -8,6 +8,9 @@ int main()
   __CPROVER_field_decl_global("field1", (unsigned __CPROVER_bitvector[2])0);
 
   char *s = (char *)malloc(3 * sizeof(char));
+  // Terminate string so that `strdup` will not call `strlen`
+  // on a string without a null-terminator.
+  s[2] = '\0';
   assert(__CPROVER_get_field(&s[0], "field1") == 0);
   assert(__CPROVER_get_field(&s[1], "field1") == 0);
 
diff --git a/regression/cbmc-with-incr/CMakeLists.txt b/regression/cbmc-with-incr/CMakeLists.txt
index da7f7e70da7..bf03c7249a2 100644
--- a/regression/cbmc-with-incr/CMakeLists.txt
+++ b/regression/cbmc-with-incr/CMakeLists.txt
@@ -1,3 +1,3 @@
 add_test_pl_tests(
-    "$<TARGET_FILE:cbmc> --incremental"
+    "$<TARGET_FILE:cbmc> --no-standard-checks --incremental"
 )
diff --git a/regression/cbmc-with-incr/Makefile b/regression/cbmc-with-incr/Makefile
index 1b69101ed35..ffb4f3b84d2 100644
--- a/regression/cbmc-with-incr/Makefile
+++ b/regression/cbmc-with-incr/Makefile
@@ -1,10 +1,10 @@
 default: tests.log
 
 test:
-	@../test.pl -c "../../../src/cbmc/cbmc --incremental"
+	@../test.pl -c "../../../src/cbmc/cbmc --no-standard-checks --incremental"
 
 tests.log: ../test.pl
-	@../test.pl -c "../../../src/cbmc/cbmc --incremental"
+	@../test.pl -c "../../../src/cbmc/cbmc --no-standard-checks --incremental"
 
 clean:
 	@$(RM) *.log
diff --git a/regression/cbmc/CMakeLists.txt b/regression/cbmc/CMakeLists.txt
index b0de5320280..96aca8cf05c 100644
--- a/regression/cbmc/CMakeLists.txt
+++ b/regression/cbmc/CMakeLists.txt
@@ -13,19 +13,19 @@ else()
 endif()
 
 add_test_pl_tests(
-    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation" -X smt-backend ${gcc_only} ${exclude_win_broken_tests}
+    "$<TARGET_FILE:cbmc> --no-standard-checks --validate-goto-model --validate-ssa-equation" -X smt-backend ${gcc_only} ${exclude_win_broken_tests}
 )
 
 add_test_pl_profile(
     "cbmc-paths-lifo"
-    "$<TARGET_FILE:cbmc> --paths lifo"
+    "$<TARGET_FILE:cbmc> --no-standard-checks --paths lifo"
     "-C;-X;thorough-paths;-X;smt-backend;-X;paths-lifo-expected-failure;${gcc_only_string}-s;paths-lifo;${exclude_win_broken_tests_string}"
     "CORE"
 )
 
 add_test_pl_profile(
     "cbmc-cprover-smt2"
-    "$<TARGET_FILE:cbmc> --cprover-smt2"
+    "$<TARGET_FILE:cbmc> --no-standard-checks --cprover-smt2"
     "-C;-X;broken-smt-backend;-X;thorough-smt-backend;-X;broken-cprover-smt-backend;-X;thorough-cprover-smt-backend;${gcc_only_string}-s;cprover-smt2;${exclude_win_broken_tests_string}"
     "CORE"
 )
@@ -33,7 +33,7 @@ add_test_pl_profile(
 # If `-X` (exclude flag) is passed, test.pl will exclude the tests matching the label following it.
 add_test_pl_profile(
   "cbmc-new-smt-backend"
-  "$<TARGET_FILE:cbmc> --incremental-smt2-solver 'z3 --smt2 -in'"
+  "$<TARGET_FILE:cbmc> --no-standard-checks --incremental-smt2-solver 'z3 --smt2 -in'"
   "${gcc_only_string}-X;no-new-smt;-s;new-smt-backend"
   "CORE"
 )
diff --git a/regression/cbmc/Makefile b/regression/cbmc/Makefile
index e5777ce8774..969a26ca813 100644
--- a/regression/cbmc/Makefile
+++ b/regression/cbmc/Makefile
@@ -10,27 +10,27 @@ GCC_ONLY =
 endif
 
 test:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" -X smt-backend $(GCC_ONLY)
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --validate-goto-model --validate-ssa-equation" -X smt-backend $(GCC_ONLY)
 
 test-cprover-smt2:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --cprover-smt2" \
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --cprover-smt2" \
 					  -X broken-smt-backend -X thorough-smt-backend \
 					  -X broken-cprover-smt-backend -X thorough-cprover-smt-backend \
 					  -s cprover-smt2 $(GCC_ONLY)
 
 test-z3:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --z3" \
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --z3" \
 					  -X broken-smt-backend -X thorough-smt-backend \
 					  -X broken-z3-smt-backend -X thorough-z3-smt-backend \
 					  -s z3 $(GCC_ONLY)
 
 test-paths-lifo:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --paths lifo" \
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --paths lifo" \
 					  -X thorough-paths -X smt-backend -X paths-lifo-expected-failure \
 					  -s paths-lifo $(GCC_ONLY)
 
 test-new-smt-backend:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'z3 --smt2 -in'" \
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --incremental-smt2-solver 'z3 --smt2 -in'" \
 					  -X no-new-smt \
 					  -s new-smt-backend $(GCC_ONLY)
 
diff --git a/regression/contracts-dfcc/chain.sh b/regression/contracts-dfcc/chain.sh
index 0bd901feaaf..97f9afb5ab1 100755
--- a/regression/contracts-dfcc/chain.sh
+++ b/regression/contracts-dfcc/chain.sh
@@ -59,4 +59,4 @@ elif echo $args_inst | grep -q -- "--dump-c" ; then
   rm "${name}${dfcc_suffix}-mod.c"
 fi
 $goto_instrument --show-goto-functions "${name}${dfcc_suffix}-mod.gb"
-$cbmc "${name}${dfcc_suffix}-mod.gb" ${args_cbmc}
+$cbmc --no-standard-checks "${name}${dfcc_suffix}-mod.gb" ${args_cbmc}
diff --git a/regression/contracts/chain.sh b/regression/contracts/chain.sh
index 615fd4568d6..527167d5984 100755
--- a/regression/contracts/chain.sh
+++ b/regression/contracts/chain.sh
@@ -42,4 +42,4 @@ elif echo $args_inst | grep -q -- "--dump-c" ; then
   rm "${name}-mod.c"
 fi
 $goto_instrument --show-goto-functions "${name}-mod.gb"
-$cbmc "${name}-mod.gb" ${args_cbmc}
+$cbmc --no-standard-checks "${name}-mod.gb" ${args_cbmc}
diff --git a/regression/goto-analyzer-simplify/CMakeLists.txt b/regression/goto-analyzer-simplify/CMakeLists.txt
index d0e80bbd2bf..c77b87019d7 100644
--- a/regression/goto-analyzer-simplify/CMakeLists.txt
+++ b/regression/goto-analyzer-simplify/CMakeLists.txt
@@ -1,3 +1,3 @@
 add_test_pl_tests(
-    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-analyzer>"
+    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-analyzer> --no-standard-checks"
 )
diff --git a/regression/goto-analyzer-simplify/Makefile b/regression/goto-analyzer-simplify/Makefile
index 4f66d4159ea..7852dc3448c 100644
--- a/regression/goto-analyzer-simplify/Makefile
+++ b/regression/goto-analyzer-simplify/Makefile
@@ -1,10 +1,10 @@
 default: tests.log
 
 test:
-	@../test.pl -e -p -c "../chain.sh ../../../src/goto-analyzer/goto-analyzer"
+	@../test.pl -e -p -c "../chain.sh ../../../src/goto-analyzer/goto-analyzer --no-standard-checks"
 
 tests.log: ../test.pl
-	@../test.pl -e -p -c "../chain.sh ../../../src/goto-analyzer/goto-analyzer"
+	@../test.pl -e -p -c "../chain.sh ../../../src/goto-analyzer/goto-analyzer --no-standard-checks"
 
 clean:
 	find . -name '*.out' -execdir $(RM) '{}' \;
diff --git a/regression/goto-analyzer/CMakeLists.txt b/regression/goto-analyzer/CMakeLists.txt
index 73af8689568..16978abe8a8 100644
--- a/regression/goto-analyzer/CMakeLists.txt
+++ b/regression/goto-analyzer/CMakeLists.txt
@@ -1,3 +1,3 @@
 add_test_pl_tests(
-    "$<TARGET_FILE:goto-analyzer>"
+    "$<TARGET_FILE:goto-analyzer> --no-standard-checks"
 )
diff --git a/regression/goto-analyzer/Makefile b/regression/goto-analyzer/Makefile
index 22e68590597..66fd99853f9 100644
--- a/regression/goto-analyzer/Makefile
+++ b/regression/goto-analyzer/Makefile
@@ -1,10 +1,10 @@
 default: tests.log
 
 test:
-	@../test.pl -e -p -c ../../../src/goto-analyzer/goto-analyzer
+	@../test.pl -e -p -c "../../../src/goto-analyzer/goto-analyzer --no-standard-checks"
 
 tests.log: ../test.pl
-	@../test.pl -e -p -c ../../../src/goto-analyzer/goto-analyzer
+	@../test.pl -e -p -c "../../../src/goto-analyzer/goto-analyzer --no-standard-checks"
 
 clean:
 	find . -name '*.out' -execdir $(RM) '{}' \;
diff --git a/regression/goto-cc-cbmc/chain.sh b/regression/goto-cc-cbmc/chain.sh
index 61ec544401e..68e5f19b600 100755
--- a/regression/goto-cc-cbmc/chain.sh
+++ b/regression/goto-cc-cbmc/chain.sh
@@ -17,4 +17,4 @@ else
   "${goto_cc}" "${name}" -o "${base_name}.gb"
 fi
 
-"${cbmc}" "${base_name}.gb" ${options}
+"${cbmc}" --no-standard-checks "${base_name}.gb" ${options}
diff --git a/regression/goto-harness/chain.sh b/regression/goto-harness/chain.sh
index c9f796abfc2..050de057785 100755
--- a/regression/goto-harness/chain.sh
+++ b/regression/goto-harness/chain.sh
@@ -58,12 +58,14 @@ $goto_harness "$input_goto_binary" "$harness_file" --harness-function-name $entr
 $cbmc --show-goto-functions "$harness_file"
 if [[ "${harness_file}" == "harness.gb" ]];then
   $cbmc --function $entry_point "$harness_file" \
+    --no-standard-checks `# deactivate default checks to make tests pass without significant adapting` \
     --pointer-check `# because we want to see out of bounds errors` \
     --unwind 11 `# with the way we set up arrays symex can't figure out loop bounds automatically` \
     --unwinding-assertions `# we want to make sure we don't accidentally pass tests because we didn't unwind enough` \
     # cbmc args end
 else
 $cbmc --function $entry_point "$input_c_file" "$harness_file" \
+  --no-standard-checks `# deactivate default checks to make tests pass without significant adapting` \
   --pointer-check `# because we want to see out of bounds errors` \
   --unwind 11 `# with the way we set up arrays symex can't figure out loop bounds automatically` \
   --unwinding-assertions `# we want to make sure we don't accidentally pass tests because we didn't unwind enough` \
diff --git a/regression/goto-instrument/chain.sh b/regression/goto-instrument/chain.sh
index 2b4381ae918..ed4fdbedc9d 100755
--- a/regression/goto-instrument/chain.sh
+++ b/regression/goto-instrument/chain.sh
@@ -40,4 +40,4 @@ elif echo $args | grep -q -- "--dump-c" ; then
   rm "${target}-mod.c"
 fi
 $goto_instrument --show-goto-functions "${target}-mod.gb"
-$cbmc "${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 52b4b683dbc..ed7c7fa498d 100755
--- a/regression/goto-synthesizer/chain.sh
+++ b/regression/goto-synthesizer/chain.sh
@@ -57,5 +57,5 @@ if echo $args_synthesizer | grep -q -- "--dump-loop-contracts" ; then
 else
   $goto_synthesizer ${args_synthesizer} "${name}-mod.gb" "${name}-mod-2.gb"
   echo "Running CBMC: "
-  $cbmc ${args_cbmc} "${name}-mod-2.gb"
+  $cbmc --no-standard-checks ${args_cbmc} "${name}-mod-2.gb"
 fi
diff --git a/regression/linking-goto-binaries/chain.sh b/regression/linking-goto-binaries/chain.sh
index d74593341a0..d391318efbd 100755
--- a/regression/linking-goto-binaries/chain.sh
+++ b/regression/linking-goto-binaries/chain.sh
@@ -21,4 +21,4 @@ else
   $goto_cc "${main}.gb" "${next}.gb" -o "final.gb"
 fi
 
-$cbmc --validate-goto-model "final.gb"
+$cbmc --no-standard-checks --validate-goto-model "final.gb"
diff --git a/regression/validate-trace-xml-schema/check.py b/regression/validate-trace-xml-schema/check.py
index 1ee1c781abd..fe9601d04d2 100644
--- a/regression/validate-trace-xml-schema/check.py
+++ b/regression/validate-trace-xml-schema/check.py
@@ -133,7 +133,7 @@ def check_test_desc(self, test_desc_path):
                 self.check_trace(test_desc_path, trace_file)
 
     def read_trace_into(self, trace_file, args):
-        subprocess.run([CbmcPath, '--trace', '--xml-ui'] + args,
+        subprocess.run([CbmcPath, '--no-standard-checks', '--trace', '--xml-ui'] + args,
                        stdout=trace_file)
 
     def check_trace(self, test_desc_path, trace_file):
diff --git a/scripts/check_help.sh b/scripts/check_help.sh
index f524c0fb5d7..6dad8f8e5ef 100755
--- a/scripts/check_help.sh
+++ b/scripts/check_help.sh
@@ -83,10 +83,30 @@ for t in  \
         echo "$undoc" | sed 's/^/\\fB/;s/-/\\-/g;s/$/\\fR/' >> man_page_opts
       done
       ;;
+    # We also need ignore the negative default checks for goto-instrument given
+    # that it's not processing them (but still ends up importing them by using
+    # the macro PARSE_OPTIONS_GOTO_CHECK). The rationale for ignoring them is
+    # similar to the goto-diff entry below.
     goto-instrument)
       for undoc in \
         -document-claims-html -document-claims-latex -show-claims \
-        -no-simplify ; do
+        -no-simplify -no-pointer-check -no-bounds-check -no-undefined-shift-check \
+        -no-pointer-primitive-check -no-div-by-zero-check -no-signed-overflow-check ; do
+        echo "$undoc" >> help_string
+        echo "$undoc" | sed 's/^/\\fB/;s/-/\\-/g;s/$/\\fR/' >> man_page_opts
+      done
+      ;;
+    # goto-diff is a bit of a peculiar situation in that it initialises some
+    # of its options using the PARSE_OPTIONS_GOTO_CHECK macro which initialises
+    # the negative checks (being the mirror image of the default checks), which
+    # this tool doesn't make use of - but there's also no good way to remove
+    # given our current architecture. Thus, we just don't document them (and
+    # ignore them if someone falls on them by accident).
+    goto-diff)
+      for undoc in \
+        -no-pointer-check -no-bounds-check -no-undefined-shift-check \
+        -no-pointer-primitive-check -no-div-by-zero-check \
+        -no-signed-overflow-check ; do
         echo "$undoc" >> help_string
         echo "$undoc" | sed 's/^/\\fB/;s/-/\\-/g;s/$/\\fR/' >> man_page_opts
       done
diff --git a/src/ansi-c/goto_check_c.h b/src/ansi-c/goto_check_c.h
index 451bfa15c3c..9fcf818241b 100644
--- a/src/ansi-c/goto_check_c.h
+++ b/src/ansi-c/goto_check_c.h
@@ -47,53 +47,71 @@ void goto_check_c(
   "(retain-trivial-checks)"                                                    \
   "(error-label):"                                                             \
   "(no-assertions)(no-assumptions)"                                            \
-  "(assert-to-assume)"
+  "(assert-to-assume)"                                                         \
+  "(no-bounds-check)(no-pointer-check)(no-signed-overflow-check)"              \
+  "(no-pointer-primitive-check)(no-undefined-shift-check)"                     \
+  "(no-div-by-zero-check)"
 
-#define HELP_GOTO_CHECK                                                        \
-  " {y--bounds-check} \t enable array bounds checks\n"                         \
-  " {y--pointer-check} \t enable pointer checks\n"                             \
+// clang-format off
+#define HELP_GOTO_CHECK \
+  " {y--no-standard-checks} \t disable default checks (more information in manpage)" /* NOLINT(whitespace/line_length) */ \
+  " {y--bounds-check} \t enable array bounds checks (default on)\n"            \
+  " {y--no-bounds-check} \t disable array bounds checks\n"                     \
+  " {y--pointer-check} \t enable pointer checks (default on)\n"                \
+  " {y--no-pointer-check} \t disable pointer checks\n"                         \
   " {y--memory-leak-check} \t enable memory leak checks\n"                     \
   " {y--memory-cleanup-check} \t enable memory cleanup checks\n"               \
-  " {y--div-by-zero-check} \t enable division by zero checks\n"                \
+  " {y--div-by-zero-check} \t enable division by zero checks (default on)\n"   \
+  " {y--no-div-by-zero-check} \t disable division by zero checks\n"            \
   " {y--signed-overflow-check} \t "                                            \
-  "enable signed arithmetic over- and underflow checks\n"                      \
+  "enable signed arithmetic over- and underflow checks (default on)\n"         \
+  " {y--no-signed-overflow-check} \t "                                         \
+  "disable signed arithmetic over- and underflow checks\n"                     \
   " {y--unsigned-overflow-check} \t "                                          \
   "enable arithmetic over- and underflow checks\n"                             \
   " {y--pointer-overflow-check} \t "                                           \
   "enable pointer arithmetic over- and underflow checks\n"                     \
   " {y--conversion-check} \t "                                                 \
   "check whether values can be represented after type cast\n"                  \
-  " {y--undefined-shift-check} \t check shift greater than bit-width\n"        \
+  " {y--undefined-shift-check} \t check shift greater than bit-width "         \
+  "(default on)\n"                                                             \
+  " {y--no-undefined-shift-check} \t disable check for shift greater than "    \
+  "bit-width\n"                                                                \
   " {y--float-overflow-check} \t check floating-point for +/-Inf\n"            \
   " {y--nan-check} \t check floating-point for NaN\n"                          \
   " {y--enum-range-check} \t "                                                 \
   "checks that all enum type expressions have values in the enum range\n"      \
   " {y--pointer-primitive-check} \t "                                          \
-  "checks that all pointers in pointer primitives are valid or null\n"         \
+  "checks that all pointers in pointer primitives are valid or null (default " \
+  "on)\n"                                                                      \
+  " {y--no-pointer-primitive-check} \t "                                       \
+  "disable checks that all pointers in pointer primitives are valid or null\n" \
   " {y--retain-trivial-checks} \t include checks that are trivially true\n"    \
   " {y--error-label} {ulabel} \t check that label {ulabel} is unreachable\n"   \
   " {y--no-built-in-assertions} \t ignore assertions in built-in library\n"    \
   " {y--no-assertions} \t ignore user assertions\n"                            \
   " {y--no-assumptions} \t ignore user assumptions\n"                          \
   " {y--assert-to-assume} \t convert user assertions to assumptions\n"
+// clang-format on
+
+#define PARSE_OPTION_OVERRIDE(cmdline, options, option)                        \
+  if(cmdline.isset(option))                                                    \
+    options.set_option(option, true);                                          \
+  if(cmdline.isset("no-" option))                                              \
+    options.set_option(option, false);                                         \
+  (void)0
 
 // clang-format off
 #define PARSE_OPTIONS_GOTO_CHECK(cmdline, options) \
-  options.set_option("bounds-check", cmdline.isset("bounds-check")); \
-  options.set_option("pointer-check", cmdline.isset("pointer-check")); \
   options.set_option("memory-leak-check", cmdline.isset("memory-leak-check")); \
   options.set_option("memory-cleanup-check", cmdline.isset("memory-cleanup-check")); /* NOLINT(whitespace/line_length) */ \
-  options.set_option("div-by-zero-check", cmdline.isset("div-by-zero-check")); \
   options.set_option("enum-range-check", cmdline.isset("enum-range-check")); \
-  options.set_option("signed-overflow-check", cmdline.isset("signed-overflow-check")); /* NOLINT(whitespace/line_length) */  \
   options.set_option("unsigned-overflow-check", cmdline.isset("unsigned-overflow-check")); /* NOLINT(whitespace/line_length) */  \
   options.set_option("pointer-overflow-check", cmdline.isset("pointer-overflow-check")); /* NOLINT(whitespace/line_length) */  \
   options.set_option("conversion-check", cmdline.isset("conversion-check")); \
-  options.set_option("undefined-shift-check", cmdline.isset("undefined-shift-check")); /* NOLINT(whitespace/line_length) */  \
   options.set_option("float-overflow-check", cmdline.isset("float-overflow-check")); /* NOLINT(whitespace/line_length) */  \
   options.set_option("nan-check", cmdline.isset("nan-check")); \
   options.set_option("built-in-assertions", !cmdline.isset("no-built-in-assertions")); /* NOLINT(whitespace/line_length) */ \
-  options.set_option("pointer-primitive-check", cmdline.isset("pointer-primitive-check")); /* NOLINT(whitespace/line_length) */ \
   options.set_option("retain-trivial-checks", \
                      cmdline.isset("retain-trivial-checks")); \
   options.set_option("assertions", !cmdline.isset("no-assertions")); /* NOLINT(whitespace/line_length) */ \
@@ -101,7 +119,13 @@ void goto_check_c(
   options.set_option("assert-to-assume", cmdline.isset("assert-to-assume")); /* NOLINT(whitespace/line_length) */ \
   options.set_option("retain-trivial", cmdline.isset("retain-trivial")); /* NOLINT(whitespace/line_length) */ \
   if(cmdline.isset("error-label")) \
-    options.set_option("error-label", cmdline.get_values("error-label")); \
+    options.set_option("error-label", cmdline.get_values("error-label"));      \
+  PARSE_OPTION_OVERRIDE(cmdline, options, "bounds-check"); \
+  PARSE_OPTION_OVERRIDE(cmdline, options, "pointer-check"); \
+  PARSE_OPTION_OVERRIDE(cmdline, options, "div-by-zero-check"); \
+  PARSE_OPTION_OVERRIDE(cmdline, options, "signed-overflow-check"); \
+  PARSE_OPTION_OVERRIDE(cmdline, options, "undefined-shift-check"); \
+  PARSE_OPTION_OVERRIDE(cmdline, options, "pointer-primitive-check"); \
   (void)0
 // clang-format on
 
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index e8579a519eb..a26448a9f54 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -106,6 +106,23 @@ void cbmc_parse_optionst::set_default_options(optionst &options)
   options.set_option("depth", UINT32_MAX);
 }
 
+void cbmc_parse_optionst::set_default_analysis_flags(
+  optionst &options,
+  const bool enabled)
+{
+  // Checks enabled by default in v6.0+.
+  options.set_option("bounds-check", enabled);
+  options.set_option("pointer-check", enabled);
+  options.set_option("pointer-primitive-check", enabled);
+  options.set_option("div-by-zero-check", enabled);
+  options.set_option("signed-overflow-check", enabled);
+  options.set_option("undefined-shift-check", enabled);
+
+  // Unwinding assertions required in certain cases for sound verification
+  // results. See https://github.com/diffblue/cbmc/issues/6561 for elaboration.
+  options.set_option("unwinding-assertions", enabled);
+}
+
 void cbmc_parse_optionst::get_command_line_options(optionst &options)
 {
   if(config.set(cmdline))
@@ -177,7 +194,13 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("show-vcc", true);
 
   if(cmdline.isset("cover"))
+  {
     parse_cover_options(cmdline, options);
+    // The default unwinding assertions option needs to be switched off when
+    // performing coverage checks because we intend to solve for coverage rather
+    // than assertions.
+    options.set_option("unwinding-assertions", false);
+  }
 
   if(cmdline.isset("mm"))
     options.set_option("mm", cmdline.get_value("mm"));
@@ -261,7 +284,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("unwind"))
   {
     options.set_option("unwind", cmdline.get_value("unwind"));
-    if(!cmdline.isset("unwinding-assertions"))
+    if(
+      !options.get_bool_option("unwinding-assertions") &&
+      !cmdline.isset("unwinding-assertions"))
     {
       log.warning() << "**** WARNING: Use --unwinding-assertions to obtain "
                        "sound verification results"
@@ -288,7 +313,9 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
   {
     options.set_option(
       "unwindset", cmdline.get_comma_separated_values("unwindset"));
-    if(!cmdline.isset("unwinding-assertions"))
+    if(
+      !options.get_bool_option("unwinding-assertions") &&
+      !cmdline.isset("unwinding-assertions"))
     {
       log.warning() << "**** WARNING: Use --unwinding-assertions to obtain "
                        "sound verification results"
@@ -305,11 +332,18 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     "self-loops-to-assumptions",
     !cmdline.isset("no-self-loops-to-assumptions"));
 
-  // all checks supported by goto_check
+  // 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);
 
   // generate unwinding assertions
-  if(cmdline.isset("unwinding-assertions"))
+  if(
+    options.get_bool_option("unwinding-assertions") ||
+    cmdline.isset("unwinding-assertions"))
   {
     options.set_option("unwinding-assertions", true);
     options.set_option("paths-symex-explore-all", true);
diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
index 8ec5b04ffaa..303c6feddac 100644
--- a/src/cbmc/cbmc_parse_options.h
+++ b/src/cbmc/cbmc_parse_options.h
@@ -34,6 +34,7 @@ class optionst;
 // clang-format off
 #define CBMC_OPTIONS \
   OPT_BMC \
+  "(no-standard-checks)" \
   "(preprocess)(slice-by-trace):" \
   OPT_FUNCTIONS \
   "(no-simplify)(full-slice)" \
@@ -91,6 +92,11 @@ class cbmc_parse_optionst : public parse_options_baset
   /// default behaviour, for example unit tests.
   static void set_default_options(optionst &);
 
+  /// \brief Setup default analysis flags.
+  ///
+  /// This function sets up the default analysis checks as discussed
+  /// in RFC https://github.com/diffblue/cbmc/issues/7975.
+  static void set_default_analysis_flags(optionst &, const bool enabled);
   static bool process_goto_program(goto_modelt &, const optionst &, messaget &);
 
   static int get_goto_program(
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp
index b64119b6b9e..868d23e71f0 100644
--- a/src/goto-analyzer/goto_analyzer_parse_options.cpp
+++ b/src/goto-analyzer/goto_analyzer_parse_options.cpp
@@ -56,6 +56,23 @@ goto_analyzer_parse_optionst::goto_analyzer_parse_optionst(
 {
 }
 
+void goto_analyzer_parse_optionst::set_default_analysis_flags(
+  optionst &options,
+  const bool enabled)
+{
+  // Checks enabled by default in v6.0+.
+  options.set_option("bounds-check", enabled);
+  options.set_option("pointer-check", enabled);
+  options.set_option("pointer-primitive-check", enabled);
+  options.set_option("div-by-zero-check", enabled);
+  options.set_option("signed-overflow-check", enabled);
+  options.set_option("undefined-shift-check", enabled);
+
+  // 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.
+}
+
 void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
 {
   if(config.set(cmdline))
@@ -67,7 +84,10 @@ void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("function"))
     options.set_option("function", cmdline.get_value("function"));
 
-  // all checks supported by goto_check
+  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);
 
   // The user should either select:
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h
index beda0d3a2d3..0e55007c81c 100644
--- a/src/goto-analyzer/goto_analyzer_parse_options.h
+++ b/src/goto-analyzer/goto_analyzer_parse_options.h
@@ -109,7 +109,8 @@ class optionst;
   "(show)(verify)(simplify):" \
   "(show-on-source)" \
   "(unreachable-instructions)(unreachable-functions)" \
-  "(reachable-functions)"
+  "(reachable-functions)"           \
+  "(no-standard-checks)"
 
 #define GOTO_ANALYSER_OPTIONS_AI \
   "(recursive-interprocedural)" \
@@ -188,6 +189,9 @@ class goto_analyzer_parse_optionst: public parse_options_baset
   virtual bool process_goto_program(const optionst &options);
 
   virtual int perform_analysis(const optionst &options);
+
+  // TODO: Add documentation
+  static void set_default_analysis_flags(optionst &options, const bool enabled);
 };
 
 #endif // CPROVER_GOTO_ANALYZER_GOTO_ANALYZER_PARSE_OPTIONS_H