Incorrect constraint simplification

[yav]

I tried CN at this commit: a6e088fca806bd94

I tried it on the following example:

signed int add_2(signed int x, signed int y)                                     
/*@ requires x == 0i32 @*/                                                          
/*@ ensures return == y @*/                                                         
{                                                                                
  return x + y;                                                                  
}

I run:

cn test.c --state-file=out.html

This results in:

[1/1]: add_2
test.c:5:3: error: Unprovable constraint
  return x + y;
  ^~~~~~~~~~~~~ 
Constraint from (test.c:3:10:)
Consider the state in out.html

When I look in out.html I see the following:

The constraint on the LHS looks OK, but the simplified version looks quite wrong.

[dc-mak]

That's embarrassing - should be fixed by https://github.com/rems-project/cerberus/commit/10506fa4f31c7302e2ab1ec1dd76002662fe5dcc

[yav]

I tried it and it works. Thanks!