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
If Haybale encounters a function that returns a 0 length slice (e.g. &mut []) when symbolically exectuing rust code, it aborts with the following boolector failure:
[boolector] boolector_bitvec_sort: 'width' must be > 0
I can't see any reason why this case should be impossible for haybale to analyze, so I am assuming this is a bug. My apologies if this is the intended behavior.
An example of a test that triggers this can be found here: hudson-ayers@1150cbd . Feel free to incorporate this test into your repo if you like. Notably, if you replace &mut [] with self.a in ez2(), the test passes.