diff --git a/Source/ExecutionEngine/CommandLineOptions.cs b/Source/ExecutionEngine/CommandLineOptions.cs
index 764ea17a4..a6f5bfd60 100644
--- a/Source/ExecutionEngine/CommandLineOptions.cs
+++ b/Source/ExecutionEngine/CommandLineOptions.cs
@@ -1667,6 +1667,14 @@ that makes all verification conditions valid.  Without option
      {:subsumption n}
        Overrides the /subsumption command-line setting for this assertion.
 
+     {:isolate}
+       Places this assertion into a separate VC, where all other assertions are assumptions.
+       In the remaining VC, this assertion becomes an assumption
+
+     {:isolate ""paths""}
+       Similar to the above, except a separate VC is created for each control flow path that leads to the marked assertion.
+       However, only goto commands that are annotated with {:allow_split} cause additional VCs to be created.
+
      {:focus}
        Splits verification into two problems. First problem deletes all paths
        that do not have the focus block. Second problem considers the paths