diff --git a/sledge/src/report.ml b/sledge/src/report.ml
index ff91c5561..df0ea6a01 100644
--- a/sledge/src/report.ml
+++ b/sledge/src/report.ml
@@ -22,7 +22,11 @@ let unknown_call call =
         | _ -> () )
       call Llair.Term.pp call]
 
+let count = ref 0
+let invalid_access_count () = !count
+
 let invalid_access fmt_thunk pp access loc =
+  Int.incr count ;
   let rep fs =
     Format.fprintf fs "%a Invalid memory access@;<1 2>@[%a@]" Loc.pp
       (loc access) pp access
diff --git a/sledge/src/report.mli b/sledge/src/report.mli
index 04a8482e7..941b268c6 100644
--- a/sledge/src/report.mli
+++ b/sledge/src/report.mli
@@ -10,3 +10,4 @@
 val unknown_call : Llair.term -> unit
 val invalid_access_inst : (Formatter.t -> unit) -> Llair.inst -> unit
 val invalid_access_term : (Formatter.t -> unit) -> Llair.term -> unit
+val invalid_access_count : unit -> int
diff --git a/sledge/src/sledge.ml b/sledge/src/sledge.ml
index d764bf85f..cd6d50e86 100644
--- a/sledge/src/sledge.ml
+++ b/sledge/src/sledge.ml
@@ -42,7 +42,8 @@ let command ~summary ?readme param =
     try
       main () |> ignore ;
       Trace.flush () ;
-      Format.printf "@\nRESULT: Success@."
+      Format.printf "@\nRESULT: Success: Invalid Accesses: %i@."
+        (Report.invalid_access_count ())
     with exn ->
       let bt = Caml.Printexc.get_raw_backtrace () in
       Trace.flush () ;