slicing: better wording in the model

moves-rwth · Jul 1, 2024 · dbb1d67 · dbb1d67
1 parent efe6614
commit dbb1d67
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 2 deletions.
diff --git 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
@@ -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(