add an "--add-assert-to-pc" option

[Laplace-Demon]

When an assertion is done, add it to assume to boost symbolic execution

[Laplace-Demon]

added it in webassembly rac mode 123935903ed81999430c55154f2f903d4b6ecd89

[redianthus]

Actually, it would be something more like "adding assert to PC"

[redianthus]

I am also tempted to think this should be the default.

Or we could have two primitives, one that adds to the pc (called "assert_and_hint" or something) and one that does not. The first one should have a name that suggests that it can be used to help the SMT

[Laplace-Demon]

I agree, I think it's mostly better to have previous assertions available in path conditions.

If I recall right, this is an option of Weasel code generator, and Owi primitives are not exposed to the Wasm file. In that case, having assert_and_hint seems to only serve internal use, and does not make much difference. But I think it may be interesting in the setting where the user call owi_assert directly? (maybe in the C examples, I'm not sure)

[redianthus]

But I think it may be interesting in the setting where the user call owi_assert directly?

Yes, that's mostly what I'm thinking of. It would be useful to add to the PC to help solvers, but sometimes it may also hurt performances so we should let the user decide and try to find what's the best default.