Skip to content

Commit c5d2dca

Browse files
authored
Merge pull request #7277 from tautschnig/cleanup/symex-verbose
Make symex assignment type invariant more verbose
2 parents 74b23a3 + aa9327d commit c5d2dca

File tree

1 file changed

+6
-2
lines changed

1 file changed

+6
-2
lines changed

src/goto-symex/goto_symex.cpp

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -45,8 +45,12 @@ void goto_symext::symex_assign(
4545
exprt lhs = clean_expr(o_lhs, state, true);
4646
exprt rhs = clean_expr(o_rhs, state, false);
4747

48-
DATA_INVARIANT(
49-
lhs.type() == rhs.type(), "assignments must be type consistent");
48+
DATA_INVARIANT_WITH_DIAGNOSTICS(
49+
lhs.type() == rhs.type(),
50+
"assignments must be type consistent, got",
51+
lhs.type().pretty(),
52+
rhs.type().pretty(),
53+
state.source.pc->source_location());
5054

5155
log.conditional_output(
5256
log.debug(), [this, &lhs](messaget::mstreamt &mstream) {

0 commit comments

Comments
 (0)