diff --git a/scripts/cargo-rmc b/scripts/cargo-rmc
index 501b4052203e..c5361d5b6cbd 100755
--- a/scripts/cargo-rmc
+++ b/scripts/cargo-rmc
@@ -31,6 +31,11 @@ def main():
     parser.add_argument("--wkdir", default=".")
     parser.add_argument("--function", default="main")
     parser.add_argument("crate", help="crate to verify")
+    parser.add_argument("--no-default-checks", action="store_true", help="Disable all default checks")
+    parser.add_argument("--no-memory-safety-checks", action="store_true", help="Disable default memory safety checks")
+    parser.add_argument("--no-overflow-checks", action="store_true", help="Disable default overflow checks")
+    parser.add_argument("--no-unwinding-checks", action="store_true", help="Disable default unwinding checks")
+    parser.add_argument("--dry-run", action="store_true", help="Print commands instead of running them")
     parser.add_argument("cbmc_args", nargs=argparse.REMAINDER,
                         default=[], help="Pass through directly to CBMC")
     args = parser.parse_args()
@@ -41,8 +46,12 @@ def main():
     if not rmc.dependencies_in_path():
         return 1
 
+    # Add some CBMC flags by default unless `--no-default-checks` is being used
+    if not args.no_default_checks:
+        rmc.add_selected_default_cbmc_flags(args)
+
     rmc.cargo_build(args.crate, args.target_dir,
-                    args.verbose, args.debug, args.mangler)
+                    args.verbose, args.debug, args.mangler, args.dry_run)
 
     pattern = os.path.join(args.target_dir, "debug", "deps", "*.json")
     jsons = glob.glob(pattern)
@@ -51,11 +60,11 @@ def main():
         return 1
     cbmc_filename = os.path.join(args.target_dir, "cbmc.out")
     c_filename = os.path.join(args.target_dir, "cbmc.c")
-    if EXIT_CODE_SUCCESS != rmc.symbol_table_to_gotoc(jsons[0], cbmc_filename, args.verbose, args.keep_temps):
+    if EXIT_CODE_SUCCESS != rmc.symbol_table_to_gotoc(jsons[0], cbmc_filename, args.verbose, args.keep_temps, args.dry_run):
         return 1
 
     if args.gen_c:
-        if EXIT_CODE_SUCCESS != rmc.goto_to_c(cbmc_filename, c_filename, args.verbose):
+        if EXIT_CODE_SUCCESS != rmc.goto_to_c(cbmc_filename, c_filename, args.verbose, args.dry_run):
             return 1
 
     if "--function" not in args.cbmc_args:
@@ -64,9 +73,9 @@ def main():
     if args.visualize:
         return rmc.run_visualize(cbmc_filename, args.cbmc_args, \
                                  args.verbose, args.quiet, args.keep_temps, \
-                                 args.function, args.srcdir, args.wkdir, args.target_dir)
+                                 args.function, args.srcdir, args.wkdir, args.target_dir, args.dry_run)
     else:
-        return rmc.run_cbmc(cbmc_filename, args.cbmc_args, args.verbose, args.quiet)
+        return rmc.run_cbmc(cbmc_filename, args.cbmc_args, args.verbose, args.quiet, args.dry_run)
 
 
 if __name__ == "__main__":
diff --git a/scripts/rmc b/scripts/rmc
index 8f6fb137beb7..f1a62274ad53 100755
--- a/scripts/rmc
+++ b/scripts/rmc
@@ -27,6 +27,11 @@ def main():
     parser.add_argument("--visualize", action="store_true")
     parser.add_argument("--srcdir", default=".")
     parser.add_argument("--wkdir", default=".")
+    parser.add_argument("--no-default-checks", action="store_true", help="Disable all default checks")
+    parser.add_argument("--no-memory-safety-checks", action="store_true", help="Disable default memory safety checks")
+    parser.add_argument("--no-overflow-checks", action="store_true", help="Disable default overflow checks")
+    parser.add_argument("--no-unwinding-checks", action="store_true", help="Disable default unwinding checks")
+    parser.add_argument("--dry-run", action="store_true", help="Print commands instead of running them")
     parser.add_argument("cbmc_args", nargs=argparse.REMAINDER,
                         default=[], help="Pass through directly to CBMC")
     args = parser.parse_args()
@@ -41,6 +46,10 @@ def main():
 
     if not rmc.dependencies_in_path():
         return 1
+    
+    # Add some CBMC flags by default unless `--no-default-checks` is being used
+    if not args.no_default_checks:
+        rmc.add_selected_default_cbmc_flags(args)
 
     base, ext = os.path.splitext(args.input)
     if ext != ".rs":
@@ -51,18 +60,18 @@ def main():
     c_filename = base + ".c"
     symbols_filename = base + ".symbols"
 
-    if EXIT_CODE_SUCCESS != rmc.compile_single_rust_file(args.input, json_filename, args.verbose, args.debug, args.keep_temps, args.mangler):
+    if EXIT_CODE_SUCCESS != rmc.compile_single_rust_file(args.input, json_filename, args.verbose, args.debug, args.keep_temps, args.mangler, args.dry_run):
         return 1
 
-    if EXIT_CODE_SUCCESS != rmc.symbol_table_to_gotoc(json_filename, goto_filename, args.verbose, args.keep_temps):
+    if EXIT_CODE_SUCCESS != rmc.symbol_table_to_gotoc(json_filename, goto_filename, args.verbose, args.keep_temps, args.dry_run):
         return 1
 
     if args.gen_c:
-        if EXIT_CODE_SUCCESS != rmc.goto_to_c(goto_filename, c_filename, args.verbose):
+        if EXIT_CODE_SUCCESS != rmc.goto_to_c(goto_filename, c_filename, args.verbose, args.dry_run):
             return 1
 
     if args.gen_symbols:
-        if EXIT_CODE_SUCCESS != rmc.goto_to_symbols(goto_filename, symbols_filename, args.verbose):
+        if EXIT_CODE_SUCCESS != rmc.goto_to_symbols(goto_filename, symbols_filename, args.verbose, args.dry_run):
             return 1
 
     if "--function" not in args.cbmc_args:
@@ -70,11 +79,13 @@ def main():
     
     args.cbmc_args.append(str(RMC_C_LIB))
     if args.visualize:
-        retcode = rmc.run_visualize(goto_filename, args.cbmc_args, \
+        # Use a separate set of flags for coverage checking (empty for now)
+        cover_args = []
+        retcode = rmc.run_visualize(goto_filename, args.cbmc_args, cover_args, \
                                     args.verbose, args.quiet, args.keep_temps, \
-                                    args.function, args.srcdir, args.wkdir)
+                                    args.function, args.srcdir, args.wkdir, args.dry_run)
     else:
-        retcode = rmc.run_cbmc(goto_filename, args.cbmc_args, args.verbose, args.quiet)
+        retcode = rmc.run_cbmc(goto_filename, args.cbmc_args, args.verbose, args.quiet, args.dry_run)
     if retcode == CBMC_VERIFICATION_FAILURE_EXIT_CODE and args.allow_cbmc_verification_failure:
         retcode = EXIT_CODE_SUCCESS
     return retcode
diff --git a/scripts/rmc.py b/scripts/rmc.py
index 95fd31725a98..24b48f7d5578 100644
--- a/scripts/rmc.py
+++ b/scripts/rmc.py
@@ -5,12 +5,40 @@
 import atexit
 import os
 import os.path
+import re
 
 
 RMC_CFG = "rmc"
 RMC_RUSTC_EXE = "rmc-rustc"
 EXIT_CODE_SUCCESS = 0
 
+MEMORY_SAFETY_CHECKS = ["--bounds-check",
+                        "--pointer-check",
+                        "--pointer-primitive-check"]
+OVERFLOW_CHECKS = ["--conversion-check",
+                   "--div-by-zero-check",
+                   "--float-overflow-check",
+                   "--nan-check",
+                   "--pointer-overflow-check",
+                   "--signed-overflow-check",
+                   "--undefined-shift-check",
+                   "--unsigned-overflow-check"]
+UNWINDING_CHECKS = ["--unwinding-assertions"]
+
+# A Scanner is intended to match a pattern with an output
+# and edit the output based on an edit function
+class Scanner:
+    def __init__(self, pattern, edit_fun):
+        self.pattern  = re.compile(pattern)
+        self.edit_fun = edit_fun
+
+    # Returns whether the scanner's pattern matches some text
+    def match(self, text):
+        return self.pattern.search(text) != None
+
+    # Returns an edited output based on the scanner's edit function
+    def edit_output(self, text):
+        return self.edit_fun(text)
 
 def is_exe(name):
     from shutil import which
@@ -31,11 +59,29 @@ def delete_file(filename):
     except OSError:
         pass
 
+# Add a set of CBMC flags to the CBMC arguments
+def add_set_cbmc_flags(args, flags):
+    # We print a warning if the user has passed the flag via `cbmc_args`
+    # Otherwise we append it to the CBMC arguments
+    for arg in flags:
+        # This behavior must be reviewed if the set of flags is extended
+        if arg in args.cbmc_args:
+            print("WARNING: Default CBMC argument `{}` not added (already specified)".format(arg))
+        else:
+            args.cbmc_args.append(arg)
+
+# Add sets of selected default CBMC flags
+def add_selected_default_cbmc_flags(args):
+    if not args.no_memory_safety_checks:
+        add_set_cbmc_flags(args, MEMORY_SAFETY_CHECKS)
+    if not args.no_overflow_checks:
+        add_set_cbmc_flags(args, OVERFLOW_CHECKS)
+    if not args.no_unwinding_checks:
+        add_set_cbmc_flags(args, UNWINDING_CHECKS)
 
 def add_rmc_rustc_debug_to_env(env):
     env["RUSTC_LOG"] = env.get("RUSTC_LOG", "rustc_codegen_llvm::gotoc")
 
-
 def print_rmc_step_status(step_name, completed_process, verbose=False):
     status = "PASS"
     if completed_process.returncode != EXIT_CODE_SUCCESS:
@@ -44,27 +90,40 @@ def print_rmc_step_status(step_name, completed_process, verbose=False):
         print(f"[RMC] stage: {step_name} ({status})")
         print(f"[RMC] cmd: {' '.join(completed_process.args)}")
 
-def run_cmd(cmd, label=None, cwd=None, env=None, output_to=None, quiet=False, verbose=False, debug=False):
-    process = subprocess.run(
-        cmd, universal_newlines=True, stdout=subprocess.PIPE, stderr=subprocess.STDOUT,
-        env=env, cwd=cwd)
+def run_cmd(cmd, label=None, cwd=None, env=None, output_to=None, quiet=False, verbose=False, debug=False, scanners=[], dry_run=False):
+    # If this a dry run, we emulate running a successful process whose output is the command itself
+    # We set `output_to` to `stdout` so that the output is not omitted below
+    if dry_run:
+        if output_to == None:
+            output_to = "stdout"
+        cmd_line = ' '.join(cmd)
+        process = subprocess.CompletedProcess(None, EXIT_CODE_SUCCESS, stdout=cmd_line)
+    else:
+        process = subprocess.run(
+            cmd, universal_newlines=True, stdout=subprocess.PIPE, stderr=subprocess.STDOUT,
+            env=env, cwd=cwd)
     
     # Print status
     if label != None:
         print_rmc_step_status(label, process, verbose)
     
+    stdout = process.stdout
+    for scanner in scanners:
+        if scanner.match(stdout):
+            stdout = scanner.edit_output(stdout)
+
     # Write to stdout if specified, or if failure, or verbose or debug
     if (output_to == "stdout" or process.returncode != EXIT_CODE_SUCCESS or verbose or debug) and not quiet:
-        print(process.stdout)
+        print(stdout)
     
     # Write to file if given
     if output_to != None and output_to != "stdout":
         with open(output_to, "w") as f:
-            f.write(process.stdout)
+            f.write(stdout)
     
     return process.returncode
 
-def compile_single_rust_file(input_filename, output_filename, verbose=False, debug=False, keep_temps=False, mangler="v0"):
+def compile_single_rust_file(input_filename, output_filename, verbose=False, debug=False, keep_temps=False, mangler="v0", dry_run=False):
     if not keep_temps:
         atexit.register(delete_file, output_filename)
     build_cmd = [RMC_RUSTC_EXE, "-Z", "codegen-backend=gotoc", "-Z", f"symbol-mangling-version={mangler}",
@@ -73,10 +132,10 @@ def compile_single_rust_file(input_filename, output_filename, verbose=False, deb
     if debug:
         add_rmc_rustc_debug_to_env(build_env)
 
-    return run_cmd(build_cmd, env=build_env, label="compile", verbose=verbose, debug=debug)
+    return run_cmd(build_cmd, env=build_env, label="compile", verbose=verbose, debug=debug, dry_run=dry_run)
 
 
-def cargo_build(crate, target_dir="target", verbose=False, debug=False, mangler="v0"):
+def cargo_build(crate, target_dir="target", verbose=False, debug=False, mangler="v0", dry_run=False):
     rustflags = ["-Z", "codegen-backend=gotoc", "-Z", f"symbol-mangling-version={mangler}", f"--cfg={RMC_CFG}"]
     rustflags = " ".join(rustflags)
     if "RUSTFLAGS" in os.environ:
@@ -89,20 +148,30 @@ def cargo_build(crate, target_dir="target", verbose=False, debug=False, mangler=
                  }
     if debug:
         add_rmc_rustc_debug_to_env(build_env)
-    return run_cmd(build_cmd, env=build_env, cwd=crate, label="build", verbose=verbose, debug=debug)
+    return run_cmd(build_cmd, env=build_env, cwd=crate, label="build", verbose=verbose, debug=debug, dry_run=dry_run)
 
+def append_unwind_tip(text):
+    unwind_tip = ("[RMC] info: Verification output shows one or more unwinding failures.\n"
+                  "[RMC] tip: Consider increasing the unwinding value or disabling `--unwinding-assertions`.\n")
+    return text + unwind_tip
 
-def symbol_table_to_gotoc(json_filename, cbmc_filename, verbose=False, keep_temps=False):
+def symbol_table_to_gotoc(json_filename, cbmc_filename, verbose=False, keep_temps=False, dry_run=False):
     if not keep_temps:
         atexit.register(delete_file, cbmc_filename)
     cmd = ["symtab2gb", json_filename, "--out", cbmc_filename]
-    return run_cmd(cmd, label="to-gotoc", verbose=verbose)
+    return run_cmd(cmd, label="to-gotoc", verbose=verbose, dry_run=dry_run)
 
-def run_cbmc(cbmc_filename, cbmc_args, verbose=False, quiet=False):
+def run_cbmc(cbmc_filename, cbmc_args, verbose=False, quiet=False, dry_run=False):
     cbmc_cmd = ["cbmc"] + cbmc_args + [cbmc_filename]
-    return run_cmd(cbmc_cmd, label="cbmc", output_to="stdout", verbose=verbose, quiet=quiet)
-
-def run_visualize(cbmc_filename, cbmc_args, verbose=False, quiet=False, keep_temps=False, function="main", srcdir=".", wkdir=".", outdir="."):
+    scanners = []
+    if "--unwinding-assertions" in cbmc_args:
+        # Pass a scanner that shows a tip if the CBMC output contains unwinding failures
+        unwind_asserts_pattern = ".*unwinding assertion.*: FAILURE"
+        unwind_asserts_scanner = Scanner(unwind_asserts_pattern, append_unwind_tip)
+        scanners.append(unwind_asserts_scanner)
+    return run_cmd(cbmc_cmd, label="cbmc", output_to="stdout", verbose=verbose, quiet=quiet, scanners=scanners, dry_run=dry_run)
+
+def run_visualize(cbmc_filename, prop_args, cover_args, verbose=False, quiet=False, keep_temps=False, function="main", srcdir=".", wkdir=".", outdir=".", dry_run=False):
     results_filename = os.path.join(outdir, "results.xml")
     coverage_filename = os.path.join(outdir, "coverage.xml")
     property_filename = os.path.join(outdir, "property.xml")
@@ -117,27 +186,29 @@ def run_visualize(cbmc_filename, cbmc_args, verbose=False, quiet=False, keep_tem
     # 4) cbmc --xml-ui --show-properties ~/rmc/library/rmc/rmc_lib.c temp.goto > property.xml
     # 5) cbmc-viewer --result results.xml --coverage coverage.xml --property property.xml --srcdir . --goto temp.goto --reportdir report
 
-    run_goto_cc(cbmc_filename, temp_goto_filename, verbose, quiet, function=function)
+    run_goto_cc(cbmc_filename, temp_goto_filename, verbose, quiet, function=function, dry_run=dry_run)
     
-    def run_cbmc_local(cbmc_args, output_to):
+    def run_cbmc_local(cbmc_args, output_to, dry_run=False):
         cbmc_cmd = ["cbmc"] + cbmc_args + [temp_goto_filename]
-        return run_cmd(cbmc_cmd, label="cbmc", output_to=output_to, verbose=verbose, quiet=quiet)
+        return run_cmd(cbmc_cmd, label="cbmc", output_to=output_to, verbose=verbose, quiet=quiet, dry_run=dry_run)
+
+    cbmc_prop_args = prop_args + ["--xml-ui"]
+    cbmc_cover_args = cover_args + ["--xml-ui"]
 
-    cbmc_xml_args = cbmc_args + ["--xml-ui"]
-    retcode = run_cbmc_local(cbmc_xml_args + ["--trace"], results_filename)
-    run_cbmc_local(cbmc_xml_args + ["--cover", "location"], coverage_filename)
-    run_cbmc_local(cbmc_xml_args + ["--show-properties"], property_filename)
+    retcode = run_cbmc_local(cbmc_prop_args + ["--trace"], results_filename, dry_run=dry_run)
+    run_cbmc_local(cbmc_cover_args + ["--cover", "location"], coverage_filename, dry_run=dry_run)
+    run_cbmc_local(cbmc_prop_args + ["--show-properties"], property_filename, dry_run=dry_run)
 
     run_cbmc_viewer(temp_goto_filename, results_filename, coverage_filename,
-                    property_filename, verbose, quiet, srcdir, wkdir, os.path.join(outdir, "report"))
+                    property_filename, verbose, quiet, srcdir, wkdir, os.path.join(outdir, "report"), dry_run=dry_run)
 
     return retcode
 
-def run_goto_cc(src, dst, verbose=False, quiet=False, function="main"):
+def run_goto_cc(src, dst, verbose=False, quiet=False, function="main", dry_run=False):
     cmd = ["goto-cc"] + ["--function", function] + [src] + ["-o", dst]
-    return run_cmd(cmd, label="goto-cc", verbose=verbose, quiet=quiet)
+    return run_cmd(cmd, label="goto-cc", verbose=verbose, quiet=quiet, dry_run=dry_run)
 
-def run_cbmc_viewer(goto_filename, results_filename, coverage_filename, property_filename, verbose=False, quiet=False, srcdir=".", wkdir=".", reportdir="report"):
+def run_cbmc_viewer(goto_filename, results_filename, coverage_filename, property_filename, verbose=False, quiet=False, srcdir=".", wkdir=".", reportdir="report", dry_run=False):
     cmd = ["cbmc-viewer"] + \
           ["--result", results_filename] + \
           ["--coverage", coverage_filename] + \
@@ -146,17 +217,17 @@ def run_cbmc_viewer(goto_filename, results_filename, coverage_filename, property
           ["--wkdir", os.path.realpath(wkdir)] + \
           ["--goto", goto_filename] + \
           ["--reportdir", reportdir]
-    return run_cmd(cmd, label="cbmc-viewer", verbose=verbose, quiet=quiet)
+    return run_cmd(cmd, label="cbmc-viewer", verbose=verbose, quiet=quiet, dry_run=dry_run)
 
 
-def run_goto_instrument(input_filename, output_filename, args, verbose=False):
+def run_goto_instrument(input_filename, output_filename, args, verbose=False, dry_run=False):
     cmd = ["goto-instrument"] + args + [input_filename]
-    return run_cmd(cmd, label="goto-instrument", verbose=verbose, output_to=output_filename)
+    return run_cmd(cmd, label="goto-instrument", verbose=verbose, output_to=output_filename, dry_run=dry_run)
 
 
-def goto_to_c(goto_filename, c_filename, verbose=False):
-    return run_goto_instrument(goto_filename, c_filename, ["--dump-c"], verbose)
+def goto_to_c(goto_filename, c_filename, verbose=False, dry_run=False):
+    return run_goto_instrument(goto_filename, c_filename, ["--dump-c"], verbose, dry_run=dry_run)
 
 
-def goto_to_symbols(goto_filename, symbols_filename, verbose=False):
-    return run_goto_instrument(goto_filename, symbols_filename, ["--show-symbol-table"], verbose)
+def goto_to_symbols(goto_filename, symbols_filename, verbose=False, dry_run=False):
+    return run_goto_instrument(goto_filename, symbols_filename, ["--show-symbol-table"], verbose, dry_run=dry_run)
diff --git a/src/test/cbmc/CodegenConstValue/main.rs b/src/test/cbmc/CodegenConstValue/main.rs
index 34199e30b430..c64ec0fc2996 100644
--- a/src/test/cbmc/CodegenConstValue/main.rs
+++ b/src/test/cbmc/CodegenConstValue/main.rs
@@ -1,5 +1,12 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// rmc-flags: --no-memory-safety-checks
+
+// We use `--no-memory-safety-checks` in this test to avoid getting
+// a verification failure:
+// [main.pointer_dereference.5] line 16 dereference failure: pointer outside object bounds in *lut_ptr: FAILURE
+// Tracking issue: https://github.com/model-checking/rmc/issues/307
 const DEC_DIGITS_LUT: &'static [u8] = b"ab";
 fn main() {
     // The next two assertions don't go through to CBMC
diff --git a/src/test/cbmc/DynTrait/boxed_closure.rs b/src/test/cbmc/DynTrait/boxed_closure.rs
index 6f2e6042fbfd..04930cd0f544 100644
--- a/src/test/cbmc/DynTrait/boxed_closure.rs
+++ b/src/test/cbmc/DynTrait/boxed_closure.rs
@@ -1,6 +1,13 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
+//rmc-flags: --no-memory-safety-checks
+
+// We use `--no-memory-safety-checks` in this test to avoid getting
+// a verification failure:
+// [pointer_dereference.7] invalid function pointer: FAILURE
+// Tracking issue: https://github.com/model-checking/rmc/issues/307
+
 // Check that we can codegen a boxed dyn closure
 
 fn main() {
diff --git a/src/test/cbmc/DynTrait/dyn_fn_param.rs b/src/test/cbmc/DynTrait/dyn_fn_param.rs
index 6dfc62c6bfa9..51aa618616e0 100644
--- a/src/test/cbmc/DynTrait/dyn_fn_param.rs
+++ b/src/test/cbmc/DynTrait/dyn_fn_param.rs
@@ -1,6 +1,13 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
+//rmc-flags: --no-memory-safety-checks
+
+// We use `--no-memory-safety-checks` in this test to avoid getting
+// a verification failure:
+// [pointer_dereference.14] invalid function pointer: FAILURE
+// Tracking issue: https://github.com/model-checking/rmc/issues/307
+
 // Check that we can pass a dyn function pointer to a stand alone
 // function definition
 
diff --git a/src/test/cbmc/FunctionCall_Ret-Param/main.rs b/src/test/cbmc/FunctionCall_Ret-Param/main.rs
index 7344666bd9a8..10f8d1b0203b 100644
--- a/src/test/cbmc/FunctionCall_Ret-Param/main.rs
+++ b/src/test/cbmc/FunctionCall_Ret-Param/main.rs
@@ -1,8 +1,13 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
+// rmc-flags: --no-unwinding-checks
 // cbmc-flags: --unwind 10
 
+// We use `--no-unwinding-checks` in this test to avoid getting
+// a verification failure (the loop being unwound depends on
+// a nondet. variable)
+
 include!("../../rmc-prelude.rs");
 
 fn main() {
diff --git a/src/test/cbmc/LoopLoop_NonReturning/main.rs b/src/test/cbmc/LoopLoop_NonReturning/main.rs
index 9e88fe1c4b50..f3f24ec4e71f 100644
--- a/src/test/cbmc/LoopLoop_NonReturning/main.rs
+++ b/src/test/cbmc/LoopLoop_NonReturning/main.rs
@@ -1,7 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// cbmc-flags: --unwind 10 --unwinding-assertions
+// cbmc-flags: --unwind 10
 
 include!("../../rmc-prelude.rs");
 
diff --git a/src/test/cbmc/LoopLoop_NonReturning/main_no_unwind_asserts.rs b/src/test/cbmc/LoopLoop_NonReturning/main_no_unwind_asserts.rs
new file mode 100644
index 000000000000..75d177d0f177
--- /dev/null
+++ b/src/test/cbmc/LoopLoop_NonReturning/main_no_unwind_asserts.rs
@@ -0,0 +1,40 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// rmc-flags: --no-default-checks
+// cbmc-flags: --unwind 9
+
+include!("../../rmc-prelude.rs");
+
+// This example tests the RMC flag `--no-default-checks`
+//
+// It is the same as `main.rs` except for the flags passed to RMC and CBMC
+// Running it with `--unwind 10` is not enough to unwind the loop
+// and generates this verification output:
+//
+// [main.unwind.0] line 30 unwinding assertion loop 0: FAILURE
+// [main.assertion.1] line 38 assertion failed: a == 0: SUCCESS
+// ** 1 of 2 failed (2 iterations)
+// VERIFICATION FAILED
+//
+// But with `--no-default-checks` we will avoid introducing a unwinding assertion:
+//
+// [main.assertion.1] line 38 assertion failed: a == 0: SUCCESS
+//
+// ** 0 of 1 failed (1 iterations)
+// VERIFICATION SUCCESSFUL
+fn main() {
+    let mut a: u32 = __nondet();
+
+    if a < 1024 {
+        loop {
+            a = a / 2;
+
+            if a == 0 {
+                break;
+            }
+        }
+
+        assert!(a == 0);
+    }
+}
diff --git a/src/test/cbmc/LoopWhile_NonReturning/main.rs b/src/test/cbmc/LoopWhile_NonReturning/main.rs
index 48aeb4c8ef30..17c634651615 100644
--- a/src/test/cbmc/LoopWhile_NonReturning/main.rs
+++ b/src/test/cbmc/LoopWhile_NonReturning/main.rs
@@ -1,7 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// cbmc-flags: --unwind 11 --unwinding-assertions
+// cbmc-flags: --unwind 11
 
 include!("../../rmc-prelude.rs");
 
diff --git a/src/test/cbmc/LoopWhile_NonReturning/main_no_unwind_asserts.rs b/src/test/cbmc/LoopWhile_NonReturning/main_no_unwind_asserts.rs
new file mode 100644
index 000000000000..4c5e6181ed5b
--- /dev/null
+++ b/src/test/cbmc/LoopWhile_NonReturning/main_no_unwind_asserts.rs
@@ -0,0 +1,37 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// rmc-flags: --no-default-checks
+// cbmc-flags: --unwind 10
+
+include!("../../rmc-prelude.rs");
+
+// This example tests the RMC flag `--no-default-checks`
+//
+// It is the same as `main.rs` except for the flags passed to RMC and CBMC
+// Running it with `--unwind 10` is not enough to unwind the loop
+// and generates this verification output:
+//
+// [main.unwind.0] line 30 unwinding assertion loop 0: FAILURE
+// [main.assertion.1] line 34 assertion failed: a == 0: SUCCESS
+//
+// ** 1 of 2 failed (2 iterations)
+// VERIFICATION FAILED
+//
+// But with `--no-default-checks` we will avoid introducing a unwinding assertion:
+//
+// [main.assertion.1] line 34 assertion failed: a == 0: SUCCESS
+//
+// ** 0 of 1 failed (1 iterations)
+// VERIFICATION SUCCESSFUL
+fn main() {
+    let mut a: u32 = __nondet();
+
+    if a < 1024 {
+        while a > 0 {
+            a = a / 2;
+        }
+
+        assert!(a == 0);
+    }
+}
diff --git a/src/test/cbmc/PointerOffset/Stable/main.rs b/src/test/cbmc/PointerOffset/Stable/main.rs
index 07467bd01386..9d6ecad8d5a4 100644
--- a/src/test/cbmc/PointerOffset/Stable/main.rs
+++ b/src/test/cbmc/PointerOffset/Stable/main.rs
@@ -1,5 +1,14 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// rmc-flags: --no-overflow-checks
+
+// We use `--no-overflow-checks` in this test to avoid getting
+// a verification failure:
+// [overflow.1] arithmetic overflow on signed - in var_11 - var_12: FAILURE
+// [overflow.2] arithmetic overflow on signed - in var_11 - var_12: FAILURE
+// Tracking issue: https://github.com/model-checking/rmc/issues/307
+
 fn main() {
     // pub unsafe fn offset_from(self, origin: *const T) -> isize
     // Calculates the distance between two pointers. The returned value
diff --git a/src/test/cbmc/PointerOffset/Unstable/main.rs b/src/test/cbmc/PointerOffset/Unstable/main.rs
index 93246a1c461f..0ada27120326 100644
--- a/src/test/cbmc/PointerOffset/Unstable/main.rs
+++ b/src/test/cbmc/PointerOffset/Unstable/main.rs
@@ -1,5 +1,14 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// rmc-flags: --no-overflow-checks
+
+// We use `--no-overflow-checks` in this test to avoid getting
+// a verification failure:
+// [overflow.2] arithmetic overflow on signed - in var_23 - var_24: FAILURE
+// [overflow.4] arithmetic overflow on signed - in var_33 - var_34: FAILURE
+// Tracking issue: https://github.com/model-checking/rmc/issues/307
+
 #![feature(core_intrinsics)]
 use std::intrinsics::ptr_offset_from;
 
diff --git a/src/test/cbmc/Pointers_OtherTypes/main.rs b/src/test/cbmc/Pointers_OtherTypes/main.rs
index 5bc83711b1ce..a09ec879dc68 100644
--- a/src/test/cbmc/Pointers_OtherTypes/main.rs
+++ b/src/test/cbmc/Pointers_OtherTypes/main.rs
@@ -1,5 +1,13 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// rmc-flags: --no-overflow-checks
+
+// We use `--no-overflow-checks` in this test to avoid getting
+// a verification failure:
+// [main.NaN.1] line 25 NaN on * in var_30 * 0.0f: FAILURE
+// Tracking issue: https://github.com/model-checking/rmc/issues/307
+
 include!("../../rmc-prelude.rs");
 
 fn main() {
diff --git a/src/test/cbmc/Slice/main.rs b/src/test/cbmc/Slice/main.rs
index 419493b77b57..eaf911150ec1 100644
--- a/src/test/cbmc/Slice/main.rs
+++ b/src/test/cbmc/Slice/main.rs
@@ -1,7 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// cbmc-flags: --unwind 6 --unwinding-assertions
+// cbmc-flags: --unwind 6
 
 fn main() {
     let name: &str = "hello";
diff --git a/src/test/cbmc/Strings/main.rs b/src/test/cbmc/Strings/main.rs
index a9b7cdaf6008..c7cc4fc3193e 100644
--- a/src/test/cbmc/Strings/main.rs
+++ b/src/test/cbmc/Strings/main.rs
@@ -1,5 +1,17 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// rmc-flags: --no-overflow-checks
+
+// We use `--no-overflow-checks` in this test to avoid getting
+// a verification failure:
+// [_RINvMNtCs9Odk7Lrvgnw_4core6optionINtB3_6OptioncE5ok_orjECs21hi0yVfW1J_4main.overflow.1] line 569 arithmetic overflow on unsigned - in *((unsigned int *)((unsigned char *)&self + 0)) - 1114112: FAILURE
+// [_RNvXsG_NtCs9Odk7Lrvgnw_4core6optionINtB5_6OptioncENtNtB7_3cmp9PartialEq2eqCs21hi0yVfW1J_4main.overflow.1] line 160 arithmetic overflow on unsigned - in *((unsigned int *)((unsigned char *)&(*var_4) + 0)) - 1114112: FAILURE
+// [_RNvXsG_NtCs9Odk7Lrvgnw_4core6optionINtB5_6OptioncENtNtB7_3cmp9PartialEq2eqCs21hi0yVfW1J_4main.overflow.2] line 160 arithmetic overflow on unsigned - in *((unsigned int *)((unsigned char *)&(*var_7) + 0)) - 1114112: FAILURE
+// [_RNvXsG_NtCs9Odk7Lrvgnw_4core6optionINtB5_6OptioncENtNtB7_3cmp9PartialEq2eqCs21hi0yVfW1J_4main.overflow.3] line 160 arithmetic overflow on unsigned - in *((unsigned int *)((unsigned char *)&(*var_13.0) + 0)) - 1114112: FAILURE
+// [_RNvXsG_NtCs9Odk7Lrvgnw_4core6optionINtB5_6OptioncENtNtB7_3cmp9PartialEq2eqCs21hi0yVfW1J_4main.overflow.4] line 160 arithmetic overflow on unsigned - in *((unsigned int *)((unsigned char *)&(*var_13.1) + 0)) - 1114112: FAILURE
+// Tracking issue: https://github.com/model-checking/rmc/issues/307
+
 fn test1() {
     let str = "foo";
     let string = str.to_string();
diff --git a/src/test/cbmc/SwitchInt/main.rs b/src/test/cbmc/SwitchInt/main.rs
index b16413d70175..9c341457e204 100644
--- a/src/test/cbmc/SwitchInt/main.rs
+++ b/src/test/cbmc/SwitchInt/main.rs
@@ -1,7 +1,13 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// cbmc-flags: --unwind 2 --unwinding-assertions
+// rmc-flags: --no-overflow-checks
+// cbmc-flags: --unwind 2
+
+// We use `--no-overflow-checks` in this test to avoid getting
+// a verification failure:
+// [_RNvCs21hi0yVfW1J_4main14doswitch_chars.overflow.1] line 17 arithmetic overflow on unsigned - in *((unsigned int *)((unsigned char *)&var_7 + 0)) - 1114112: FAILURE
+// Tracking issue: https://github.com/model-checking/rmc/issues/307
 
 fn doswitch_int() -> i32 {
     for i in [99].iter() {
diff --git a/src/test/cbmc/Whitespace/main.rs b/src/test/cbmc/Whitespace/main.rs
index b602f93ad621..3e321e7a83b2 100644
--- a/src/test/cbmc/Whitespace/main.rs
+++ b/src/test/cbmc/Whitespace/main.rs
@@ -1,7 +1,14 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// cbmc-flags: --unwind 2 --unwinding-assertions
+// rmc-flags: --no-overflow-checks
+// cbmc-flags: --unwind 2
+
+// We use `--no-overflow-checks` in this test to avoid getting
+// a verification failure:
+// [_RNvXs3_NtNtCs9Odk7Lrvgnw_4core3str4iterNtB5_11CharIndicesNtNtNtNtB9_4iter6traits8iterator8Iterator4nextCs21hi0yVfW1J_4main.overflow.1] line 141 arithmetic overflow on unsigned - in *((unsigned int *)((unsigned char *)&var_4 + 0)) - 1114112: FAILURE
+// [_RNvXs5_NtNtCs9Odk7Lrvgnw_4core3str7patternINtB5_19MultiCharEqSearcherNtB7_12IsWhitespaceENtB5_8Searcher4nextCs21hi0yVfW1J_4main.overflow.1] line 641 arithmetic overflow on unsigned - in *((unsigned int *)((unsigned char *)&var_5 + 8)) - 1114112: FAILURE
+// Tracking issue: https://github.com/model-checking/rmc/issues/307
 
 fn main() {
     let mut iter = "A few words".split_whitespace();
diff --git a/src/test/expected/dry-run/expected b/src/test/expected/dry-run/expected
new file mode 100644
index 000000000000..e862a76a7290
--- /dev/null
+++ b/src/test/expected/dry-run/expected
@@ -0,0 +1,3 @@
+rmc-rustc -Z codegen-backend=gotoc -Z symbol-mangling-version=v0 --cfg=rmc
+symtab2gb
+cbmc --bounds-check --pointer-check --pointer-primitive-check --conversion-check --div-by-zero-check --float-overflow-check --nan-check --pointer-overflow-check --signed-overflow-check --undefined-shift-check --unsigned-overflow-check --unwinding-assertions --function main
diff --git a/src/test/expected/dry-run/main.rs b/src/test/expected/dry-run/main.rs
new file mode 100644
index 000000000000..0530bb82ed2c
--- /dev/null
+++ b/src/test/expected/dry-run/main.rs
@@ -0,0 +1,9 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// rmc-flags: --dry-run
+
+// `--dry-run` causes RMC to print out commands instead of running them
+// In `expected` you will find substrings of these commands because the
+// concrete paths depend on your working directory.
+fn main() {}
diff --git a/src/test/expected/unwind_tip/expected b/src/test/expected/unwind_tip/expected
new file mode 100644
index 000000000000..278819fbbe48
--- /dev/null
+++ b/src/test/expected/unwind_tip/expected
@@ -0,0 +1,2 @@
+[RMC] info: Verification output shows one or more unwinding failures.
+[RMC] tip: Consider increasing the unwinding value or disabling `--unwinding-assertions`.
diff --git a/src/test/expected/unwind_tip/main.rs b/src/test/expected/unwind_tip/main.rs
new file mode 100644
index 000000000000..66b974f5cac3
--- /dev/null
+++ b/src/test/expected/unwind_tip/main.rs
@@ -0,0 +1,29 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// cbmc-flags: --unwind 9
+
+include!("../../rmc-prelude.rs");
+
+// This example is a copy of the `cbmc` test in
+// `src/test/cbmc/LoopLoop_NonReturning/main_no_unwind_asserts.rs`
+//
+// The verification output should show an unwinding assertion failure.
+//
+// In this test, we check that RMC warns the user about unwinding failures
+// and makes a recommendation to fix the issue.
+fn main() {
+    let mut a: u32 = __nondet();
+
+    if a < 1024 {
+        loop {
+            a = a / 2;
+
+            if a == 0 {
+                break;
+            }
+        }
+
+        assert!(a == 0);
+    }
+}
diff --git a/src/test/firecracker/virtio-block-parse/main.rs b/src/test/firecracker/virtio-block-parse/main.rs
index 6809364c220f..79dae3416031 100644
--- a/src/test/firecracker/virtio-block-parse/main.rs
+++ b/src/test/firecracker/virtio-block-parse/main.rs
@@ -1,13 +1,15 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// --unwinding-assertions
-//
+
+// rmc-flags: --no-overflow-checks
+
+// We use `--no-overflow-checks` in this test to avoid getting
+// a verification failure:
+// [overflow.1] arithmetic overflow on unsigned + in var_6 + var_7: FAILURE
+// Tracking issue: https://github.com/model-checking/rmc/issues/307
+
 // Example from Firecracker virtio block device
 // We test the parse function against an arbitrary guest memory
-// Outstanding issues:
-//   - Padstone-4795 (std::io:error in enum variant)
-// RMC changes
-//   - strict is_valid check and loop in descriptor chain check during parse
 
 #![allow(dead_code)]
 #![allow(unused_variables)]
diff --git a/src/test/prusti/Binary_search_fail.rs b/src/test/prusti/Binary_search_fail.rs
index 1aaa60f36767..40223377b0ac 100644
--- a/src/test/prusti/Binary_search_fail.rs
+++ b/src/test/prusti/Binary_search_fail.rs
@@ -1,7 +1,7 @@
 // Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// cbmc-flags: --unwind 4 --unwinding-assertions
+// cbmc-flags: --unwind 4
 
 use std::cmp::Ordering::*;
 
diff --git a/src/test/smack/loops/gauss_sum_nondet.rs b/src/test/smack/loops/gauss_sum_nondet.rs
index 7f4c999a4bfc..33c70312017f 100644
--- a/src/test/smack/loops/gauss_sum_nondet.rs
+++ b/src/test/smack/loops/gauss_sum_nondet.rs
@@ -3,7 +3,7 @@
 // @flag --no-memory-splitting --unroll=4
 // @expect verified
 
-// cbmc-flags: --unwind 5 --unwinding-assertions
+// cbmc-flags: --unwind 5
 
 include!("../../rmc-prelude.rs");
 
diff --git a/src/test/smack/loops/gauss_sum_nondet_fail.rs b/src/test/smack/loops/gauss_sum_nondet_fail.rs
index b1d96e29a762..d29f31dc2d50 100644
--- a/src/test/smack/loops/gauss_sum_nondet_fail.rs
+++ b/src/test/smack/loops/gauss_sum_nondet_fail.rs
@@ -3,7 +3,7 @@
 // @flag --no-memory-splitting --unroll=10
 // @expect error
 
-// cbmc-flags: --unwind 5 --unwinding-assertions
+// cbmc-flags: --unwind 5
 
 include!("../../rmc-prelude.rs");
 
diff --git a/src/test/smack/loops/iterator.rs b/src/test/smack/loops/iterator.rs
index 8081798312cb..7d810fe79e03 100644
--- a/src/test/smack/loops/iterator.rs
+++ b/src/test/smack/loops/iterator.rs
@@ -3,7 +3,7 @@
 // @flag --no-memory-splitting --unroll=4
 // @expect verified
 
-// cbmc-flags: --unwind 5 --unwinding-assertions
+// cbmc-flags: --unwind 5
 
 fn fac(n: u64) -> u64 {
     match n {
diff --git a/src/test/smack/loops/iterator_fail.rs b/src/test/smack/loops/iterator_fail.rs
index 051dd8b3581f..72fca0cf5134 100644
--- a/src/test/smack/loops/iterator_fail.rs
+++ b/src/test/smack/loops/iterator_fail.rs
@@ -3,7 +3,7 @@
 // @flag --no-memory-splitting --unroll=10
 // @expect error
 
-// cbmc-flags: --unwind 5 --unwinding-assertions
+// cbmc-flags: --unwind 5
 
 fn fac(n: u64) -> u64 {
     match n {
diff --git a/src/tools/compiletest/src/runtest.rs b/src/tools/compiletest/src/runtest.rs
index 1bb368bf1fd5..3272274b1299 100644
--- a/src/tools/compiletest/src/runtest.rs
+++ b/src/tools/compiletest/src/runtest.rs
@@ -2478,8 +2478,11 @@ impl<'test> TestCx<'test> {
         let parent_dir = self.testpaths.file.parent().unwrap();
         // The name of the function to test is the same as the stem of `*.expected` file
         let function_name = self.testpaths.file.file_stem().unwrap().to_str().unwrap();
+        // `cargo-rmc` has issues with default flags so we pass `--no-default-checks` to disable them
+        // https://github.com/model-checking/rmc/issues/289
         cargo
             .arg("rmc")
+            .arg("--no-default-checks")
             .args(["--function", function_name])
             .arg("--target")
             .arg(self.output_base_dir().join("target"))