Skip to content

Commit b49d81d

Browse files
committed
proof rules: rewrite warning text
1 parent 6611aa5 commit b49d81d

File tree

1 file changed

+3
-2
lines changed

1 file changed

+3
-2
lines changed

src/proof_rules/unroll.rs

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -101,15 +101,16 @@ impl Encoding for UnrollAnnotation {
101101

102102
let k: u128 = lit_u128(k);
103103

104+
// TODO: these should be warning diagnostics emitted to the user
104105
match enc_env.direction {
105106
Direction::Down => {
106107
if !is_top_lit(terminator) {
107-
tracing::warn!("Top terminator is not used with down direction!");
108+
tracing::warn!("Unrolling terminator is not top element (down direction)");
108109
}
109110
}
110111
Direction::Up => {
111112
if !is_bot_lit(terminator) {
112-
tracing::warn!("Bottom terminator is not used with up direction!");
113+
tracing::warn!("Unrolling terminator is not bottom element (up direction)");
113114
}
114115
}
115116
}

0 commit comments

Comments
 (0)