diff --git a/package.json b/package.json
index a3d76700..abfb51b3 100644
--- a/package.json
+++ b/package.json
@@ -139,6 +139,11 @@
                 "title": "Run last model check again",
                 "category": "TLA+"
             },
+            {
+                "command": "tlaplus.model.check.runAgainWithOptions",
+                "title": "Run last model check with new options",
+                "category": "TLA+"
+            },
             {
                 "command": "tlaplus.model.check.stop",
                 "title": "Stop model checking process",
@@ -200,6 +205,10 @@
                     "command": "tlaplus.model.check.runAgain",
                     "when": "tlaplus.tlc.canRunAgain"
                 },
+                {
+                    "command": "tlaplus.model.check.runAgainWithOptions",
+                    "when": "tlaplus.tlc.canRunAgain"
+                },
                 {
                     "command": "tlaplus.model.check.customRun",
                     "when": "editorLangId == tlaplus"
diff --git a/src/commands/checkModel.ts b/src/commands/checkModel.ts
index 85852e64..a15f2aa1 100644
--- a/src/commands/checkModel.ts
+++ b/src/commands/checkModel.ts
@@ -13,6 +13,7 @@ import { ToolOutputChannel } from '../outputChannels';
 
 export const CMD_CHECK_MODEL_RUN = 'tlaplus.model.check.run';
 export const CMD_CHECK_MODEL_RUN_AGAIN = 'tlaplus.model.check.runAgain';
+export const CMD_CHECK_MODEL_RUN_AGAIN_WITH_OPTIONS = 'tlaplus.model.check.runAgainWithOptions';
 export const CMD_CHECK_MODEL_CUSTOM_RUN = 'tlaplus.model.check.customRun';
 export const CMD_CHECK_MODEL_STOP = 'tlaplus.model.check.stop';
 export const CMD_CHECK_MODEL_DISPLAY = 'tlaplus.model.check.display';
@@ -53,7 +54,8 @@ export async function checkModel(
 
 export async function runLastCheckAgain(
     diagnostic: vscode.DiagnosticCollection,
-    extContext: vscode.ExtensionContext
+    extContext: vscode.ExtensionContext,
+    withNewOptions = false,
 ): Promise<void> {
     if (!lastCheckFiles) {
         vscode.window.showWarningMessage('No last check to run');
@@ -62,7 +64,7 @@ export async function runLastCheckAgain(
     if (!canRunTlc(extContext)) {
         return;
     }
-    doCheckModel(lastCheckFiles, true, extContext, diagnostic, false);
+    doCheckModel(lastCheckFiles, true, extContext, diagnostic, withNewOptions);
 }
 
 export async function checkModelCustom(
diff --git a/src/main.ts b/src/main.ts
index b04aeaa6..c80d7d2c 100644
--- a/src/main.ts
+++ b/src/main.ts
@@ -2,7 +2,8 @@ import * as vscode from 'vscode';
 import * as path from 'path';
 import { CMD_CHECK_MODEL_RUN, CMD_CHECK_MODEL_STOP, CMD_CHECK_MODEL_DISPLAY, CMD_SHOW_TLC_OUTPUT,
     CMD_CHECK_MODEL_CUSTOM_RUN, checkModel, displayModelChecking, stopModelChecking,
-    showTlcOutput, checkModelCustom, CMD_CHECK_MODEL_RUN_AGAIN, runLastCheckAgain} from './commands/checkModel';
+    showTlcOutput, checkModelCustom, CMD_CHECK_MODEL_RUN_AGAIN, CMD_CHECK_MODEL_RUN_AGAIN_WITH_OPTIONS,
+    runLastCheckAgain} from './commands/checkModel';
 import { CMD_EVALUATE_SELECTION, evaluateSelection, CMD_EVALUATE_EXPRESSION,
     evaluateExpression } from './commands/evaluateExpression';
 import { parseModule, CMD_PARSE_MODULE } from './commands/parseModule';
@@ -50,6 +51,9 @@ export function activate(context: vscode.ExtensionContext): void {
         vscode.commands.registerCommand(
             CMD_CHECK_MODEL_RUN_AGAIN,
             () => runLastCheckAgain(diagnostic, context)),
+        vscode.commands.registerCommand(
+            CMD_CHECK_MODEL_RUN_AGAIN_WITH_OPTIONS,
+            () => runLastCheckAgain(diagnostic, context, true)),
         vscode.commands.registerCommand(
             CMD_CHECK_MODEL_CUSTOM_RUN,
             () => checkModelCustom(diagnostic, context)),