add a _s suffix to signed operations ?

[zapashcanon]

I was looking at the following output from Owi: Assert failure: (bool.eq (i32.add (i32.and symbol_0 symbol_1) (i32.shr (i32.xor symbol_0 symbol_1) (i32 1))) (i32.div (i32.add symbol_0 symbol_1) (i32 2))). And as the code was generated from C code, it was not clear to me whether the i32.div was operating on signed or unsigned integers.

After looking at the code here, I understand that it is operating on signed integers.

What would you think of adding a _s prefix on signed version as it is done in Wasm? It debugging easier IMO so I'm all for it, but maybe it is this way to be compatible with the smtlib or something I'm not aware of?

(I could have owi wasm2wat out.wasm after running owi c but did not think about it at first, and it's not really smooth when debugging stuff)

[filipeom]

What would you think of adding a _s prefix on signed version as it is done in Wasm?

For me, since I'm aware of this difference, it doesn't affect me 😅 . However, I agree that this change should be made.

but maybe it is this way to be compatible with the smtlib or something I'm not aware of?

It was implemented this way because other theories, like Ints, don't have the concept of unsigned values. Therefore, having a Div_s for mathematical integers might be confusing, as it could imply the existence of a Div_u as well. However, perhaps we should introduce Div | Div_s | Div_u and other similar operators to make it more explicit what expressions we are constructing and printing?