seahorn / crab

A library for building abstract interpretation-based analyses
Apache License 2.0
234 stars 32 forks source link

Bug in flat_boolean_domain #64

Closed ffrohn closed 7 months ago

ffrohn commented 7 months ago

This line looks very suspicious. Shouldn't the inequation be the other way around? I didn't try to create an example that triggers the bug (if it is one), I just stumbled across this line when I was looking at the code to understand how Booleans are handled.

caballa commented 7 months ago

Hi Florian,

Thank you for reporting this bug. It has been fixed in commit 4d934fe