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.