diff --git a/src/slicing/model.rs b/src/slicing/model.rs
index ac16a08..78d3d22 100644
--- a/src/slicing/model.rs
+++ b/src/slicing/model.rs
@@ -63,6 +63,11 @@ impl SliceModel {
         })
     }
 
+    /// Return the number of statements in this model.
+    pub fn len(&self) -> usize {
+        self.stmts.len()
+    }
+
     /// Iterate over all [`Ident`]s for slice variables.
     pub fn iter_variables(&self) -> impl Iterator<Item = Ident> + '_ {
         self.stmts.iter().map(|(stmt, _res)| stmt.ident)
diff --git a/src/smt/pretty_model.rs b/src/smt/pretty_model.rs
index a6fc252..e3ec2f7 100644
--- a/src/smt/pretty_model.rs
+++ b/src/smt/pretty_model.rs
@@ -85,8 +85,9 @@ pub fn pretty_vc_value<'smt, 'ctx>(
         let slice_pre = pretty_eval_result(value)
             .append(Doc::line_())
             .append(Doc::text(format!(
-                "(slicing removed {} statements)",
-                num_sliced_stmts
+                "(slicing removed {}/{} assertions)",
+                num_sliced_stmts,
+                slice_model.len()
             )));
         lines.push(Doc::nil());
         lines.push(