Open
Description
ID_onehot
and ID_onehot0
expressions are used in cbmc/develop but there are no corresponding expression types in std_expr.h
. Moreover, ID_onehot
and ID_onehot0
are not assigned in cbmc/develop (they are assigned in EBMC).
New expression types should be added to std_expr.h
and then the code in cbmc/develop should be refactored to use those instead of plain exprt
.
Metadata
Metadata
Assignees
Labels
No labels