diff --git a/sledge/src/config.ml b/sledge/src/config.ml
index 2f50e8745..38965931b 100644
--- a/sledge/src/config.ml
+++ b/sledge/src/config.ml
@@ -84,7 +84,10 @@ type t =
         (** Dump $(i,input.bc) translated to LLAIR in human-readable form to
             $(i,output.llair), or $(b,-) for $(b,stdout). *)
   ; trace: Trace.trace_mods_funs
-         [@aka ["t"]] [@docv "spec"] [@conv trace_conv]
+         [@aka ["t"]]
+         [@docv "spec"]
+         [@conv trace_conv]
+         [@default Trace.none.trace_mods_funs]
         (** Enable debug tracing according to $(i,spec), which is a sequence
             of module and function names separated by $(b,+) or $(b,-). For
             example, $(b,Control-Control.exec_inst) enables all tracing in
diff --git a/sledge/src/trace/trace.ml b/sledge/src/trace/trace.ml
index ac058a2fc..821f94b27 100644
--- a/sledge/src/trace/trace.ml
+++ b/sledge/src/trace/trace.ml
@@ -19,8 +19,8 @@ type trace_mod_funs =
 type trace_mods_funs = trace_mod_funs Map.M(String).t
 type config = {trace_all: bool; trace_mods_funs: trace_mods_funs}
 
-let config : config ref =
-  ref {trace_all= false; trace_mods_funs= Map.empty (module String)}
+let none = {trace_all= false; trace_mods_funs= Map.empty (module String)}
+let config : config ref = ref none
 
 let init ?(margin = 300) ~config:c () =
   Format.set_margin margin ;
diff --git a/sledge/src/trace/trace.mli b/sledge/src/trace/trace.mli
index 7f8bf6c24..5c143b532 100644
--- a/sledge/src/trace/trace.mli
+++ b/sledge/src/trace/trace.mli
@@ -21,6 +21,8 @@ type config =
   ; trace_mods_funs: trace_mods_funs
         (** Specify tracing of individual toplevel modules *) }
 
+val none : config
+
 val init : ?margin:int -> config:config -> unit -> unit
 (** Initialize the configuration of debug tracing. *)