Skip to content

Commit aee33f9

Browse files
committed
SMV: convert typecast expressions
The conversion of SMV IR to text now skips over the typecast expressions generated by the type checker.
1 parent b861e8b commit aee33f9

File tree

1 file changed

+5
-0
lines changed

1 file changed

+5
-0
lines changed

src/smvlang/expr2smv.cpp

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -584,6 +584,11 @@ expr2smvt::resultt expr2smvt::convert_rec(const exprt &src)
584584
return convert_binary(to_binary_expr(src), ">>", precedencet::SHIFT);
585585
}
586586

587+
else if(src.id() == ID_typecast)
588+
{
589+
return convert_rec(to_typecast_expr(src).op());
590+
}
591+
587592
else // no SMV language expression for internal representation
588593
return convert_norep(src);
589594
}

0 commit comments

Comments
 (0)