You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
The incremental smt2 decision procedure struct encoding function expects the struct_exprt type to be a struct_type_tag and not an inlined struct_typet.
This is causes the struct_typet to not be encoded (while the outer struct_exprt is encoded) and when passed to the convert_type_to_smt_sort function it causes an invariant violation.
Note that the inline struct is added by overflow operations instrumentation.