Closed
Description
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.
Metadata
Assignees
Labels
No labels