Promotion from integer to boolean

ID0000751: This issue was created automatically from Mantis Issue 751. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0000751	Frama-C	Kernel > ACSL implementation	public	2011-03-11	2014-02-12

Reporter	signoles	Assigned To	virgile	Resolution	fixed
Priority	normal	Severity	minor	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	-	Target Version	-	Fixed in Version	Frama-C Nitrogen-20111001

Description :

At this day, in the predicate or term "0 == !1 (merged)", 0 is an integer while !1 (merged) is a boolean. Both members of the equality should have the same type (boolean). Thus a solution could be that the normalization translates "0 == !1 (merged)" to "(0 == 0) == (0 == !1 (merged))".