Hello, By PPL's Int64_Box.CC76_widening_assign , I get [1,1] \widen [1,2] = [1,2] whereas [1,+inf] is expected in this case. Here is my Java test code (below createIntBox (a,b) is a help function that creates an interval of dimension 1 between integers 'a' and 'b') Int64_Box b=createIntBox(1, 1); Int64_Box b2=createIntBox(1, 2); out.println(b+", " + b2); b2.CC76_widening_assign(b, new By_Reference<Integer>(0)); out.println(b+", " + b2); I get: A in 1, A in [1, 2] A in 1, A in [1, 2] I probably misunderstand something, but applying the original definition of widening as defined in CC76, we have the following: [1,1] \widening [1,2] = [1, +inf] which is different from PPL's result above. Strangely, if I change 'b2' to [1,3] ,i.e. Int64_Box b2=createIntBox(1, 3), I will get the expected results, i.e [1,1] \widening [1,3] = [1, +inf] So It becomes a bit confusing. Maybe PPL has another implementation of CC76's widening? Can you clarify a bit? Thanks. Zell. p.s For completeness, here is the 'createIntBox' part: private static Int64_Box createIntBox(int a, int b) { Linear_Expression_Variable var = new Linear_Expression_Variable(new Variable(0)); Linear_Expression le_a = new Linear_Expression_Coefficient(new Coefficient(a)); Linear_Expression le_b = new Linear_Expression_Coefficient(new Coefficient(b)); Int64_Box box=new Int64_Box(1, Degenerate_Element.UNIVERSE); box.add_constraint(new Constraint(var, Relation_Symbol.GREATER_OR_EQUAL, le_a)); box.add_constraint(new Constraint(var, Relation_Symbol.LESS_OR_EQUAL, le_b)); return box; }