diff --git a/README.rst b/README.rst
index 022e8501..baf10a9b 100644
--- a/README.rst
+++ b/README.rst
@@ -87,8 +87,8 @@ The verifier accepts the following command line arguments::
   --read-only-segments ARG Mark segments as read-only (0-indexed) when loading
                            ELF
   --script FILENAME        Save macaw CFGs to the provided directory
-  --no-assume-stack-scope  Don't add additional assumptions about stack frame
-                           scoping
+  --assume-stack-scope     Add additional assumptions about stack frame scoping 
+                           during function calls (unsafe)
   --ignore-warnings ARG    Don't raise any of the given warning types
   --always-classify-return Always resolve classifier failures by assuming
                            function returns, if possible.
diff --git a/docs/user-manual/invoking.tex b/docs/user-manual/invoking.tex
index 7101ee07..f2e0effb 100644
--- a/docs/user-manual/invoking.tex
+++ b/docs/user-manual/invoking.tex
@@ -88,11 +88,25 @@ \section{Invoking the \pate{} Verifier}
   --read-only-segments ARG Mark segments as read-only (0-indexed) when loading
                            ELF
   --script FILENAME        Save macaw CFGs to the provided directory
-  --no-assume-stack-scope  Don't add additional assumptions about stack frame
-                           scoping
+  --assume-stack-scope     Add additional assumptions about stack frame 
+                           scoping during function calls (unsafe)
   --ignore-warnings ARG    Don't raise any of the given warning types
 \end{verbatim}
 
+\subsection{--assume-stack-scope}
+
+This flag causes \pate{} to assume that out-of-scope stack slots 
+(i.e. slots that are past the current stack pointer) are always equal between
+the two binaries.
+Although in actuality they may have differing out-of-scope stack
+contents, programs that exercise proper stack hygiene should never
+access those values. By assuming they are equal, \pate{} avoids 
+creating spurious counter-examples where under-specified pointers
+alias inequivalent, but out-of-scope, stack slots.
+This is a fairly strong assumption that can have unintended side-effects,
+including assuming \emph{false} when out-of-scope stack contents are
+\emph{provably} inequivalent.
+
 
 %%% Local Variables:
 %%% mode: latex
diff --git a/src/Pate/CLI.hs b/src/Pate/CLI.hs
index 399466e9..f6292ea0 100644
--- a/src/Pate/CLI.hs
+++ b/src/Pate/CLI.hs
@@ -94,7 +94,7 @@ mkRunConfig archLoader opts rcfg mtt = let
         , PC.cfgRescopingFailureMode = rerrMode opts
         , PC.cfgScriptPath = scriptPath opts
         , PC.cfgTraceTree = fromMaybe noTraceTree mtt
-        , PC.cfgStackScopeAssume = not $ noAssumeStackScope opts
+        , PC.cfgStackScopeAssume = assumeStackScope opts
         , PC.cfgIgnoreWarnings = ignoreWarnings opts
         , PC.cfgAlwaysClassifyReturn = alwaysClassifyReturn opts
         , PC.cfgTraceConstraints = traceConstraints opts
@@ -147,7 +147,7 @@ data CLIOptions = CLIOptions
   , jsonToplevel :: Bool
   , readOnlySegments :: [Int]
   , scriptPath :: Maybe FilePath
-  , noAssumeStackScope :: Bool
+  , assumeStackScope :: Bool
   , ignoreWarnings :: [String]
   , alwaysClassifyReturn :: Bool
   , preferTextInput :: Bool
@@ -462,8 +462,8 @@ cliOptions = OA.info (OA.helper <*> parser)
          <> OA.help "Save macaw CFGs to the provided directory"
          ))
     <*> OA.switch
-         ( OA.long "no-assume-stack-scope"
-         <> OA.help "Don't add additional assumptions about stack frame scoping"
+         ( OA.long "assume-stack-scope"
+         <> OA.help "Add additional assumptions about stack frame scoping during function calls (unsafe)"
          )
     <*> OA.many (OA.strOption
         ( OA.long "ignore-warnings"
diff --git a/src/Pate/Config.hs b/src/Pate/Config.hs
index a0c66b0e..d07adda3 100644
--- a/src/Pate/Config.hs
+++ b/src/Pate/Config.hs
@@ -314,7 +314,7 @@ defaultVerificationCfg =
                      , cfgIgnoreDivergedControlFlow = False
                      , cfgTargetEquivRegs = []
                      , cfgRescopingFailureMode = ThrowOnEqRescopeFailure
-                     , cfgStackScopeAssume = True
+                     , cfgStackScopeAssume = False
                      , cfgScriptPath = Nothing
                      , cfgIgnoreWarnings = []
                      , cfgAlwaysClassifyReturn = False
diff --git a/tests/aarch32/scripted/challenge10.args b/tests/aarch32/scripted/challenge10.args
index b6af41ea..7f51ca27 100644
--- a/tests/aarch32/scripted/challenge10.args
+++ b/tests/aarch32/scripted/challenge10.args
@@ -8,4 +8,5 @@
 -e ContinueAfterRecoverableFailures
 -r AllowEqRescopeFailure
 -s transport_handler
---script challenge10.pate
\ No newline at end of file
+--script challenge10.pate
+--assume-stack-scope
\ No newline at end of file
diff --git a/tests/template.mk b/tests/template.mk
index fddd41a1..eaf659c2 100644
--- a/tests/template.mk
+++ b/tests/template.mk
@@ -46,8 +46,7 @@ malloc-%.exe: ./build/malloc-%.s ./build/link.ld
 %.test_run: %.original.exe %.patched.exe
 	../../pate.sh -o $(basename $@).original.exe -p $(basename $@).patched.exe \
 		`( (test -f $(basename $@).toml && echo "-b $(basename $@).toml") || echo "")` \
-		`( (test -f $(basename $@).pate && echo "--script $(basename $@).pate") || echo "")` \
-		--no-assume-stack-scope
+		`( (test -f $(basename $@).pate && echo "--script $(basename $@).pate") || echo "")`
 
 .PRECIOUS: ./build/%.s ./build/%.i %.exe malloc-%.exe ./unequal/%.original.exe ./unequal/%.patched.exe