diff --git a/Source/DafnyCore/DafnyConsolePrinter.cs b/Source/DafnyCore/DafnyConsolePrinter.cs
index 93b994df0b0..ecbeecf9fd1 100644
--- a/Source/DafnyCore/DafnyConsolePrinter.cs
+++ b/Source/DafnyCore/DafnyConsolePrinter.cs
@@ -66,7 +66,7 @@ public void WriteSourceCodeSnippet(Boogie.IToken tok, TextWriter tw) {
     tw.WriteLine("");
   }
 
-  public static readonly Option<bool> ShowSnippets = new("--show-snippets",
+  public static readonly Option<bool> ShowSnippets = new("--show-snippets", () => true,
     "Show a source code snippet for each Dafny message.");
 
   static DafnyConsolePrinter() {
diff --git a/Source/DafnyCore/Generic/Reporting.cs b/Source/DafnyCore/Generic/Reporting.cs
index 784491fc004..345bf8c1e3a 100644
--- a/Source/DafnyCore/Generic/Reporting.cs
+++ b/Source/DafnyCore/Generic/Reporting.cs
@@ -240,7 +240,7 @@ public override bool Message(MessageSource source, ErrorLevel level, string erro
           errorLine += "\n";
         }
 
-        if (Options.Get(DafnyConsolePrinter.ShowSnippets)) {
+        if (Options.Get(DafnyConsolePrinter.ShowSnippets) && tok != Token.NoToken) {
           TextWriter tw = new StringWriter();
           new DafnyConsolePrinter(Options).WriteSourceCodeSnippet(tok.ToRange(), tw);
           Options.OutputWriter.Write(tw.ToString());
diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index 36d2e8932f7..a7dbb00efaf 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -83,7 +83,10 @@ static DafnyDriver() {
       "/compileVerbose:0",
       
       // Set a default time limit, to catch cases where verification time runs off the rails
-      "/timeLimit:300"
+      "/timeLimit:300",
+
+      // test results do not include source code snippets
+      "/showSnippets:0"
     };
 
     public static readonly string[] NewDefaultArgumentsForTesting = new[] {
@@ -94,7 +97,10 @@ static DafnyDriver() {
       "--use-basename-for-filename",
 
       // Set a default time limit, to catch cases where verification time runs off the rails
-      "--verification-time-limit=300"
+      "--verification-time-limit=300",
+
+      // test results do not include source code snippets
+      "--show-snippets:false"
     };
 
     public static int Main(string[] args) {
diff --git a/Source/IntegrationTests/LitTests.cs b/Source/IntegrationTests/LitTests.cs
index 0baebd911f3..c724037a644 100644
--- a/Source/IntegrationTests/LitTests.cs
+++ b/Source/IntegrationTests/LitTests.cs
@@ -57,15 +57,15 @@ IEnumerable<string> AddExtraArgs(IEnumerable<string> args, IEnumerable<string> l
         return (extraDafnyArguments is null ? args : args.Append(extraDafnyArguments)).Concat(local);
       }
 
-      string[] defaultResolveArgs = new[] { "resolve", "--use-basename-for-filename" };
-      string[] defaultVerifyArgs = new[] { "verify", "--use-basename-for-filename", "--cores:2", "--verification-time-limit:300" };
+      string[] defaultResolveArgs = new[] { "resolve", "--use-basename-for-filename", "--show-snippets:false" };
+      string[] defaultVerifyArgs = new[] { "verify", "--use-basename-for-filename", "--show-snippets:false", "--cores:2", "--verification-time-limit:300" };
       //string[] defaultTranslateArgs = new[] { "translate", "--use-basename-for-filename", "--cores:2", "--verification-time-limit:300" };
-      string[] defaultBuildArgs = new[] { "build", "--use-basename-for-filename", "--cores:2", "--verification-time-limit:300" };
-      string[] defaultRunArgs = new[] { "run", "--use-basename-for-filename", "--cores:2", "--verification-time-limit:300" };
+      string[] defaultBuildArgs = new[] { "build", "--use-basename-for-filename", "--show-snippets:false", "--cores:2", "--verification-time-limit:300" };
+      string[] defaultRunArgs = new[] { "run", "--use-basename-for-filename", "--show-snippets:false", "--cores:2", "--verification-time-limit:300" };
 
       var substitutions = new Dictionary<string, object> {
         { "%diff", "diff" },
-        { "%trargs", "--use-basename-for-filename --cores:2 --verification-time-limit:300" },
+        { "%trargs", "--use-basename-for-filename --show-snippets:false --cores:2 --verification-time-limit:300" },
         { "%binaryDir", "." },
         { "%z3", Path.Join("z3", "bin", $"z3-{DafnyOptions.DefaultZ3Version}") },
         { "%repositoryRoot", RepositoryRoot.Replace(@"\", "/") },
diff --git a/Test/cli/projectFile/dfyconfig.toml b/Test/cli/projectFile/dfyconfig.toml
index 48c886a1b0f..ecbf61daf32 100644
--- a/Test/cli/projectFile/dfyconfig.toml
+++ b/Test/cli/projectFile/dfyconfig.toml
@@ -2,4 +2,5 @@ includes = ["src/**/*"]
 excludes = ["**/excluded.dfy"]
 
 [options]
-warn-shadowing = true
\ No newline at end of file
+warn-shadowing = true
+show-snippets = false
diff --git a/Test/cli/projectFile/projectFile.dfy b/Test/cli/projectFile/projectFile.dfy
index 8f57479d67c..317f57b480d 100644
--- a/Test/cli/projectFile/projectFile.dfy
+++ b/Test/cli/projectFile/projectFile.dfy
@@ -1,34 +1,34 @@
 // A project file can specify input files and configure options
-// RUN: %baredafny resolve --use-basename-for-filename "%S/dfyconfig.toml" > "%t"
+// RUN: %baredafny resolve --show-snippets:false --use-basename-for-filename "%S/dfyconfig.toml" > "%t"
 
 // Test using a URL instead of a local file as a project file
-// RUN: ! %baredafny resolve --use-basename-for-filename "https://github.com/dafny-lang/dafny/blob/master/dfyconfig.toml"
+// RUN: ! %baredafny resolve --show-snippets:false --use-basename-for-filename "https://github.com/dafny-lang/dafny/blob/master/dfyconfig.toml"
 
 // Test option override behavior
-// RUN: %baredafny resolve --use-basename-for-filename "%S/dfyconfig.toml" --warn-shadowing=false >> "%t"
+// RUN: %baredafny resolve --show-snippets:false --use-basename-for-filename "%S/dfyconfig.toml" --warn-shadowing=false >> "%t"
 
 // Multiple project files are not allowed
-// RUN: ! %baredafny resolve --use-basename-for-filename "%S/dfyconfig.toml" "%S/broken/dfyconfig.toml"
+// RUN: ! %baredafny resolve --show-snippets:false --use-basename-for-filename "%S/dfyconfig.toml" "%S/broken/dfyconfig.toml"
 
 // Project files may not contain unknown properties
-// RUN: ! %baredafny resolve --use-basename-for-filename "%S/broken/dfyconfig.toml"
+// RUN: ! %baredafny resolve --show-snippets:false --use-basename-for-filename "%S/broken/dfyconfig.toml"
 
 // Warn if file contains options that don't exist
-// RUN: %baredafny resolve --use-basename-for-filename "%S/broken/invalidOption.toml" >> "%t"
+// RUN: %baredafny resolve --show-snippets:false --use-basename-for-filename "%S/broken/invalidOption.toml" >> "%t"
 
 // Project files must be files on disk.
-// RUN: ! %baredafny resolve --use-basename-for-filename "%S/doesNotExist/dfyconfig.toml"
+// RUN: ! %baredafny resolve --show-snippets:false --use-basename-for-filename "%S/doesNotExist/dfyconfig.toml"
 
 // Project file options must have the right type
-// RUN: ! %baredafny resolve --use-basename-for-filename "%S/badTypes/dfyconfig.toml" 2>> "%t"
+// RUN: ! %baredafny resolve --show-snippets:false --use-basename-for-filename "%S/badTypes/dfyconfig.toml" 2>> "%t"
 
 // A project file without includes will take all .dfy files as input
-// RUN: %baredafny resolve --use-basename-for-filename "%S/noIncludes/dfyconfig.toml" >> "%t"
+// RUN: %baredafny resolve --show-snippets:false --use-basename-for-filename "%S/noIncludes/dfyconfig.toml" >> "%t"
 
 // Files included by the project file and on the CLI, duplicate is ignored.
-// RUN: %baredafny resolve --use-basename-for-filename "%S/dfyconfig.toml" "%S/src/input.dfy" >> "%t"
+// RUN: %baredafny resolve --show-snippets:false --use-basename-for-filename "%S/dfyconfig.toml" "%S/src/input.dfy" >> "%t"
 
 // Files excluded by the project file and included on the CLI, are included
-// RUN: ! %baredafny resolve --use-basename-for-filename "%S/dfyconfig.toml" "%S/src/excluded.dfy" >> "%t"
+// RUN: ! %baredafny resolve --show-snippets:false --use-basename-for-filename "%S/dfyconfig.toml" "%S/src/excluded.dfy" >> "%t"
 
-// RUN: %diff "%s.expect" "%t"
\ No newline at end of file
+// RUN: %diff "%s.expect" "%t"
diff --git a/Test/cli/zeroCores.dfy b/Test/cli/zeroCores.dfy
index 3ac64189bbb..073f8bc2ad7 100644
--- a/Test/cli/zeroCores.dfy
+++ b/Test/cli/zeroCores.dfy
@@ -1,10 +1,10 @@
-// RUN: ! %baredafny verify --use-basename-for-filename --cores=0 "%s" 2> "%t"
-// RUN: ! %baredafny verify --use-basename-for-filename --cores=earga "%s" 2>> "%t"
-// RUN: ! %baredafny verify --use-basename-for-filename --cores=earga% "%s" 2>> "%t"
-// RUN: ! %baredafny verify --use-basename-for-filename "%s" >> "%t"
-// RUN: ! %baredafny verify --use-basename-for-filename --cores=1 "%s" >> "%t"
-// RUN: ! %baredafny verify --use-basename-for-filename --cores=0% "%s" >> "%t"
-// RUN: ! %baredafny verify --use-basename-for-filename --cores=50% "%s" >> "%t"
+// RUN: ! %baredafny verify --show-snippets:false --use-basename-for-filename --cores=0 "%s" 2> "%t"
+// RUN: ! %baredafny verify --show-snippets:false --use-basename-for-filename --cores=earga "%s" 2>> "%t"
+// RUN: ! %baredafny verify --show-snippets:false --use-basename-for-filename --cores=earga% "%s" 2>> "%t"
+// RUN: ! %baredafny verify --show-snippets:false --use-basename-for-filename "%s" >> "%t"
+// RUN: ! %baredafny verify --show-snippets:false --use-basename-for-filename --cores=1 "%s" >> "%t"
+// RUN: ! %baredafny verify --show-snippets:false --use-basename-for-filename --cores=0% "%s" >> "%t"
+// RUN: ! %baredafny verify --show-snippets:false --use-basename-for-filename --cores=50% "%s" >> "%t"
 // RUN: %diff "%s.expect" "%t"
 
 method Foo() ensures false {
diff --git a/Test/dafny0/Stdin.dfy b/Test/dafny0/Stdin.dfy
index 5dfe4c43341..d33f243a419 100644
--- a/Test/dafny0/Stdin.dfy
+++ b/Test/dafny0/Stdin.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 0 %stdin "module A{}" %baredafny verify --stdin > "%t"
-// RUN: %exits-with 4 %stdin "method a() { assert false; }" %baredafny verify --stdin >> "%t"
+// RUN: %exits-with 0 %stdin "module A{}" %baredafny verify --show-snippets:false --stdin > "%t"
+// RUN: %exits-with 4 %stdin "method a() { assert false; }" %baredafny verify --show-snippets:false --stdin >> "%t"
 // RUN: %diff "%s.expect" "%t"
 
diff --git a/Test/dafny4/parse-errors.dfy b/Test/dafny4/parse-errors.dfy
index 2cd126cd4bf..33e71cf0dc6 100644
--- a/Test/dafny4/parse-errors.dfy
+++ b/Test/dafny4/parse-errors.dfy
@@ -1,4 +1,4 @@
-// RUN: ! %baredafny resolve --use-basename-for-filename "%s" > "%t"
+// RUN: ! %baredafny resolve --show-snippets:false --use-basename-for-filename "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 datatype D = B | CCC | E { predicate IsFailure() { E? } function PropagateFailure(): D { E } }
diff --git a/Test/dafny4/parse-errors2.dfy b/Test/dafny4/parse-errors2.dfy
index 314dc77f1f6..2a9c7405ae2 100644
--- a/Test/dafny4/parse-errors2.dfy
+++ b/Test/dafny4/parse-errors2.dfy
@@ -1,4 +1,4 @@
-// RUN: ! %baredafny resolve --use-basename-for-filename "%s" > "%t"
+// RUN: ! %baredafny resolve --use-basename-for-filename --show-snippets:false "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 datatype D = D(z: int, 2: int)
diff --git a/Test/git-issues/git-issue-1309.dfy b/Test/git-issues/git-issue-1309.dfy
index de033a7817d..cc127b077a9 100644
--- a/Test/git-issues/git-issue-1309.dfy
+++ b/Test/git-issues/git-issue-1309.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 2 %baredafny verify --use-basename-for-filename "%s" > "%t"
+// RUN: %exits-with 2 %baredafny verify --show-snippets:false --use-basename-for-filename "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // Example for Issue 1309 -- not yet fixed
diff --git a/Test/git-issues/git-issue-1992.dfy b/Test/git-issues/git-issue-1992.dfy
index 6e06f17a5e3..521c8750f39 100644
--- a/Test/git-issues/git-issue-1992.dfy
+++ b/Test/git-issues/git-issue-1992.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %baredafny verify --use-basename-for-filename "%s" > "%t"
+// RUN: %exits-with 4 %baredafny verify --use-basename-for-filename --show-snippets:false "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 function foo(x: int): int {
diff --git a/Test/git-issues/git-issue-2477.dfy b/Test/git-issues/git-issue-2477.dfy
index 8ce74a53ee3..76efd22a839 100644
--- a/Test/git-issues/git-issue-2477.dfy
+++ b/Test/git-issues/git-issue-2477.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %baredafny verify --use-basename-for-filename --cores:2 --verification-time-limit:300 "%s" > "%t"
+// RUN: %exits-with 4 %baredafny verify --show-snippets:false --use-basename-for-filename --cores:2 --verification-time-limit:300 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 trait T {
diff --git a/Test/git-issues/git-issue-2507.dfy b/Test/git-issues/git-issue-2507.dfy
index 5fde00689d9..444f65b0997 100644
--- a/Test/git-issues/git-issue-2507.dfy
+++ b/Test/git-issues/git-issue-2507.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 2 %baredafny resolve --use-basename-for-filename "%s" > "%t"
+// RUN: %exits-with 2 %baredafny resolve --use-basename-for-filename --show-snippets:false "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 method Test(i: int) {
diff --git a/Test/git-issues/git-issue-2959.dfy b/Test/git-issues/git-issue-2959.dfy
index 67565586e4b..bce0d4ff9b8 100644
--- a/Test/git-issues/git-issue-2959.dfy
+++ b/Test/git-issues/git-issue-2959.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 3 %baredafny build --use-basename-for-filename --enforce-determinism "%s" > "%t"
+// RUN: %exits-with 3 %baredafny build --show-snippets:false --use-basename-for-filename --enforce-determinism "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 method NondetIf() returns (x: int) {
diff --git a/Test/git-issues/git-issue-2959a.dfy b/Test/git-issues/git-issue-2959a.dfy
index f1f28186c4f..7d756809fac 100644
--- a/Test/git-issues/git-issue-2959a.dfy
+++ b/Test/git-issues/git-issue-2959a.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %baredafny build --use-basename-for-filename --enforce-determinism "%s" > "%t"
+// RUN: %exits-with 4 %baredafny build --show-snippets:false --use-basename-for-filename --enforce-determinism "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 method AlsoNondetIf() returns (x: int) {
diff --git a/Test/git-issues/git-issue-2959b.dfy b/Test/git-issues/git-issue-2959b.dfy
index 4762ddf6341..ecf87cd9e8c 100644
--- a/Test/git-issues/git-issue-2959b.dfy
+++ b/Test/git-issues/git-issue-2959b.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %baredafny build --use-basename-for-filename "%s" > "%t"
+// RUN: %exits-with 4 %baredafny build --show-snippets:false --use-basename-for-filename "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 method NondetIf() returns (x: int) {
diff --git a/Test/git-issues/git-issue-3288b.dfy b/Test/git-issues/git-issue-3288b.dfy
index 165477c7016..2a4776232ee 100644
--- a/Test/git-issues/git-issue-3288b.dfy
+++ b/Test/git-issues/git-issue-3288b.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 2 %baredafny verify --use-basename-for-filename "%s" > "%t"
+// RUN: %exits-with 2 %baredafny verify --show-snippets:false --use-basename-for-filename "%s" > "%t"
 // RUN: %diff "%s.expect" "%t" 
 
 module M {
diff --git a/Test/git-issues/git-issue-3366.dfy b/Test/git-issues/git-issue-3366.dfy
index 5faf713fddc..4df2ea4099f 100644
--- a/Test/git-issues/git-issue-3366.dfy
+++ b/Test/git-issues/git-issue-3366.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 2 %baredafny verify --use-basename-for-filename "%s" > "%t"
+// RUN: %exits-with 2 %baredafny verify --show-snippets:false --use-basename-for-filename "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 class C<T> {
diff --git a/Test/git-issues/git-issue-3370.dfy b/Test/git-issues/git-issue-3370.dfy
index d575ece70af..b4ef20b046a 100644
--- a/Test/git-issues/git-issue-3370.dfy
+++ b/Test/git-issues/git-issue-3370.dfy
@@ -1,5 +1,5 @@
-// RUN: %baredafny build --use-basename-for-filename "%s" > "%t"
-// RUN: %exits-with 4 %baredafny build --use-basename-for-filename --enforce-determinism "%s" >> "%t"
+// RUN: %baredafny build --use-basename-for-filename --show-snippets:false "%s" > "%t"
+// RUN: %exits-with 4 %baredafny build --use-basename-for-filename --show-snippets:false --enforce-determinism "%s" >> "%t"
 // RUN: %diff "%s.expect" "%t"
 
 method m() {
diff --git a/Test/git-issues/git-issue-3377.dfy b/Test/git-issues/git-issue-3377.dfy
index 8407fa07189..8c378861643 100644
--- a/Test/git-issues/git-issue-3377.dfy
+++ b/Test/git-issues/git-issue-3377.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 2 %baredafny test --use-basename-for-filename "%s" > "%t"
+// RUN: %exits-with 2 %baredafny test --show-snippets:false --use-basename-for-filename "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 method {:extern} {:test} m(i: int, ghost j: int) 
diff --git a/Test/git-issues/git-issue-3451/git-issue-3451.dfy b/Test/git-issues/git-issue-3451/git-issue-3451.dfy
index eec2674936d..86bc23528da 100644
--- a/Test/git-issues/git-issue-3451/git-issue-3451.dfy
+++ b/Test/git-issues/git-issue-3451/git-issue-3451.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 2 %baredafny resolve --use-basename-for-filename "%s" > "%t"
+// RUN: %exits-with 2 %baredafny resolve --show-snippets:false --use-basename-for-filename "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // The #line should no longer be special
diff --git a/Test/git-issues/git-issue-3451/git-issue-3451a.dfy b/Test/git-issues/git-issue-3451/git-issue-3451a.dfy
index e9dde98f053..cf84557d8e4 100644
--- a/Test/git-issues/git-issue-3451/git-issue-3451a.dfy
+++ b/Test/git-issues/git-issue-3451/git-issue-3451a.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 2 %baredafny resolve --use-basename-for-filename "%s" > "%t"
+// RUN: %exits-with 2 %baredafny resolve --use-basename-for-filename --show-snippets:false "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // The #line should no longer be special
diff --git a/Test/git-issues/git-issue-3513/git-issue-3513.dfy b/Test/git-issues/git-issue-3513/git-issue-3513.dfy
index 84057e6ac84..2fdd65f2c73 100644
--- a/Test/git-issues/git-issue-3513/git-issue-3513.dfy
+++ b/Test/git-issues/git-issue-3513/git-issue-3513.dfy
@@ -1,8 +1,8 @@
-// RUN: %exits-with 2 %baredafny resolve --use-basename-for-filename "%s" > "%t"
-// RUN: %exits-with 2 %baredafny resolve --use-basename-for-filename --library:"%S/src/A.dfy" "%s" >> "%t"
-// RUN: %baredafny resolve --use-basename-for-filename --library:"%S/src/A.dfy,%S/src/sub/B.dfy" "%s" >> "%t"
-// RUN: %baredafny resolve --use-basename-for-filename --library:"%S/src/A.dfy , %S/src/sub/B.dfy" "%s" >> "%t"
-// RUN: %baredafny resolve --use-basename-for-filename --library:"%S/src" "%s" >> "%t"
+// RUN: %exits-with 2 %baredafny resolve --show-snippets:false --use-basename-for-filename "%s" > "%t"
+// RUN: %exits-with 2 %baredafny resolve --show-snippets:false --use-basename-for-filename --library:"%S/src/A.dfy" "%s" >> "%t"
+// RUN: %baredafny resolve --show-snippets:false --use-basename-for-filename --library:"%S/src/A.dfy,%S/src/sub/B.dfy" "%s" >> "%t"
+// RUN: %baredafny resolve --show-snippets:false --use-basename-for-filename --library:"%S/src/A.dfy , %S/src/sub/B.dfy" "%s" >> "%t"
+// RUN: %baredafny resolve --show-snippets:false --use-basename-for-filename --library:"%S/src" "%s" >> "%t"
 // RUN: %diff "%s.expect" "%t"
 
 module M {
diff --git a/Test/git-issues/git-issue-3757.dfy b/Test/git-issues/git-issue-3757.dfy
index d85cdf3c99b..a8e3992a630 100644
--- a/Test/git-issues/git-issue-3757.dfy
+++ b/Test/git-issues/git-issue-3757.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 2 %baredafny resolve --use-basename-for-filename "%s" > "%t"
+// RUN: %exits-with 2 %baredafny resolve --show-snippets:false --use-basename-for-filename "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 const
diff --git a/Test/git-issues/git-issue-3757a.dfy b/Test/git-issues/git-issue-3757a.dfy
index 83c6a4f0475..6bf915c2216 100644
--- a/Test/git-issues/git-issue-3757a.dfy
+++ b/Test/git-issues/git-issue-3757a.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 2 %baredafny resolve --use-basename-for-filename "%s" > "%t"
+// RUN: %exits-with 2 %baredafny resolve --show-snippets:false --use-basename-for-filename "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 const +
diff --git a/Test/git-issues/git-issue-3839/git-issue-3839a.dfy b/Test/git-issues/git-issue-3839/git-issue-3839a.dfy
index 90b0ea43a0f..467b950aafe 100644
--- a/Test/git-issues/git-issue-3839/git-issue-3839a.dfy
+++ b/Test/git-issues/git-issue-3839/git-issue-3839a.dfy
@@ -1,4 +1,4 @@
-// RUN: ! %baredafny test --use-basename-for-filename "%s" > "%t"
+// RUN: ! %baredafny test --use-basename-for-filename --show-snippets:false "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 method {:test} M(x: int) returns (r: int)
diff --git a/Test/git-issues/git-issue-3855.dfy b/Test/git-issues/git-issue-3855.dfy
index cea1bca62f6..25c43b1c088 100644
--- a/Test/git-issues/git-issue-3855.dfy
+++ b/Test/git-issues/git-issue-3855.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %baredafny verify --warn-deprecation:false --use-basename-for-filename "%s" > "%t"
+// RUN: %exits-with 4 %baredafny verify --show-snippets:false --warn-deprecation:false --use-basename-for-filename "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 // Nearly verbatim copy of the text case given in the issue
 //SIMULADA 
diff --git a/Test/lit.site.cfg b/Test/lit.site.cfg
index 8aa922d728c..fe4c93bd4f7 100644
--- a/Test/lit.site.cfg
+++ b/Test/lit.site.cfg
@@ -114,6 +114,7 @@ config.suffixes.append('.transcript')
 dafnyArgs = [
     # We do not want absolute or relative paths in error messages, just the basename of the file
     'useBaseNameForFileName',
+    'showSnippets:0',
 
     # Try to verify 2 verification conditions at once
     'vcsCores:2',
@@ -155,7 +156,7 @@ def buildCmd(cmd, args):
 dafny = addParams(buildCmd(dafnyExecutable, dafnyArgs))
 boogie = buildCmd(boogieExecutable, boogieArgs)
 
-standardArguments = addParams(' '.join(["--use-basename-for-filename"]))
+standardArguments = addParams(' '.join(["--use-basename-for-filename", "--show-snippets"]))
 
 # Inform user what executable is being used
 lit_config.note(f'Using Dafny (%dafny): {dafny}\n')
diff --git a/Test/logger/TextLogger.dfy b/Test/logger/TextLogger.dfy
index 41d2f96b36f..a5e01450cf6 100644
--- a/Test/logger/TextLogger.dfy
+++ b/Test/logger/TextLogger.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %baredafny verify --log-format:text --isolate-assertions "%s" > "%t"
+// RUN: %exits-with 4 %baredafny verify --show-snippets:false --log-format:text --isolate-assertions "%s" > "%t"
 // RUN: %OutputCheck --file-to-check "%t" "%s"
 // CHECK: Overall outcome: Errors
 // CHECK: Overall time: .*
diff --git a/Test/logger/TextLoggerBatch.dfy b/Test/logger/TextLoggerBatch.dfy
index e2351b3c63b..7981884545a 100644
--- a/Test/logger/TextLoggerBatch.dfy
+++ b/Test/logger/TextLoggerBatch.dfy
@@ -1,4 +1,4 @@
-// RUN: %exits-with 4 %baredafny verify --log-format:text "%s" > "%t"
+// RUN: %exits-with 4 %baredafny verify --show-snippets:false --log-format:text "%s" > "%t"
 // RUN: %OutputCheck --file-to-check "%t" "%s"
 // CHECK: Overall outcome: Errors
 // CHECK: Overall time: .*
diff --git a/docs/HowToFAQ/Errors-CommandLine.md b/docs/HowToFAQ/Errors-CommandLine.md
index 93078b048e9..0a7c0edf6f8 100644
--- a/docs/HowToFAQ/Errors-CommandLine.md
+++ b/docs/HowToFAQ/Errors-CommandLine.md
@@ -235,7 +235,7 @@ The `printIncludes` option has these alternatives: None, Immediate, Transitive.
 
 <!-- %no-check TODO: Outputs the help document  -->
 ```bash 
-dafny resolve --quantifier-syntax:2 null.dfy
+dafny resolve --show-snippets:false --quantifier-syntax:2 null.dfy
 ```
 
 This is a generic error message about command-line arguments,
diff --git a/docs/OnlineTutorial/Lemmas.md b/docs/OnlineTutorial/Lemmas.md
index 055931e98c2..f2fa5a5e651 100644
--- a/docs/OnlineTutorial/Lemmas.md
+++ b/docs/OnlineTutorial/Lemmas.md
@@ -29,7 +29,7 @@ for zero in an array. What makes this problem interesting is that the array we a
 searching in has two special properties: all elements are non-negative, and each successive
 element decreases by at most one from the previous element. In code:
 
-<!-- %check-verify Lemmas.1.expect -->
+<!-- %check-verify Lemmas.1.expect %options -->
 ```dafny
 method FindZero(a: array<int>) returns (index: int)
   requires forall i :: 0 <= i < a.Length ==> 0 <= a[i]
diff --git a/docs/check-examples b/docs/check-examples
index 9b8088a383a..d716422a203 100755
--- a/docs/check-examples
+++ b/docs/check-examples
@@ -120,8 +120,9 @@ dafny="$dafnydir/dafny"
 outdir="$dir/../Test/docexamples"
 
 coverage=0
+permOptions="--show-snippets:false "
 defOptions="--function-syntax:4 --use-basename-for-filename --unicode-char:false"
-legacyOptions="-functionSyntax:4 -useBaseNameForFileName"
+legacyOptions="-functionSyntax:4 -useBaseNameForFileName -showSnippets:0"
 
 while getopts 'c' opt; do
   case "$opt" in
@@ -366,7 +367,7 @@ do
         if [ "$coverage" == "1" ] ; then
           f=$outdir/$(basename $file)_${n}.dfy
           if  [ "$command" == "%check-legacy" ]; then
-            echo "// RUN: %exits-with" $expectedExit "%baredafny" $verb $dOptions ${options[@]} '"%s" > "%t"' > "$f"
+            echo "// RUN: %exits-with" $expectedExit "%baredafny" "/showSnippets:0" $verb $dOptions ${options[@]} '"%s" > "%t"' > "$f"
             echo " " >> $f
             cat $text >> $f
           elif [ "$command" == "%check-cli" ]; then
@@ -379,11 +380,11 @@ do
         else
           if [ "$command" == "%check-legacy" ]; then
             isverbose=-compileVerbose:$checkIds
-            (cd "$dir"; "$dafny" $verb $dOptions $isverbose ${options[@]} $text   ) > "$actualOut" 2> "$actualError"
+            (cd "$dir"; "$dafny" /showSnippets:0 $dOptions $isverbose ${options[@]} $text   ) > "$actualOut" 2> "$actualError"
           else
             isverbose=
             if [ "$checkIds" == "1" ]; then isverbose="--verbose" ; fi
-            ( cd "$dir" ; "$dafny" $verb $isverbose $dOptions ${options[@]} $text ) > "$actualOut" 2> "$actualError"
+            ( cd "$dir" ; "$dafny" $verb $isverbose $permOptions $dOptions ${options[@]} $text ) > "$actualOut" 2> "$actualError"
           fi
           actualExit=$?
           if [ "$useHeadings" == "1" ]; then
diff --git a/docs/dev/news/4087.feat b/docs/dev/news/4087.feat
new file mode 100644
index 00000000000..92101bb037d
--- /dev/null
+++ b/docs/dev/news/4087.feat
@@ -0,0 +1 @@
+errors issued in command-line mode now show source code context by default; this behavior can be disabled using the option --show-snippets:false.