main: early exit for --no-verify for just model checking

src/main.rs

@@ -773,6 +773,15 @@ fn verify_files_main(
         }
     }
 
+    // If `--no-verify` is set and we don't need to print SMT-LIB or explain the
+    // core VC, we can return early.
+    if options.debug_options.no_verify
+        && !options.debug_options.print_smt
+        && !options.lsp_options.explain_core_vc
+    {
+        return Ok(true);
+    }
+
     let mut verify_units: Vec<Item<VerifyUnit>> = source_units
         .into_iter()
         .flat_map(|item| item.flat_map(SourceUnit::into_verify_unit))

website/docs/model-checking.md

@@ -88,7 +88,8 @@ Expected reward from Storm: ≈ 0.9999995232
 The result is approximate because it was computed via floating-point arithmetic.
 To get exact results at the expense of slower computation, you can add the `--storm-exact` flag.
 
-You can also use the `--run-storm` parameter with the [`verify` command](./caesar/README.md#subcommand-caesar-verify) or with [our LSP server](./caesar/vscode-and-lsp.md).
+You can also use the `--run-storm` flag with the [`verify` command](./caesar/README.md#subcommand-caesar-verify) or with [our LSP server](./caesar/vscode-and-lsp.md).
+Furthermore, you can set the `--no-verify` flag to only run model checking and not run Caesar's deductive verification.
 
 ### Option B: Generating JANI Manually {#generating-jani-manually}