Malte Schwerhoff

I don't see why not. Would you be willing to commit a corresponding PR? I suggest the following: * [config.scala](https://github.com/viperproject/silicon/blob/master/src/main/scala/Config.scala): a suitable config option that defaults to `0`/`None` * Z3...

Yes! 🕺 I saw these in PyZ3, but did not knew that they were usable via the SMT-LIB frontend. I'm curious to see how much they can improve performance.

1. In my impression, the div-mod behaviour implemented by Java, C++ or Rust is more standard than that of Python. Thus, I'd expect the following to pass (comments indicate what...

Additional information: - According to [SMT-LIB's integer theory](http://smtlib.cs.uiowa.edu/theories-Ints.shtml), it defines division and modulo according to [Boute's Euclidean definition](https://core.ac.uk/download/pdf/55698442.pdf). - Boogie (at least by default) also directly encodes div and mod...

Decisions taken during the Viper meeting on 22nd April 2021: 1. Viper will have fixed semantics of division and modulo. If front-ends need custom semantics, they'll have to axiomatise it....

Which behaviour?

Thanks for clarifying, sounds OK to me. Out of curiosity: does the transformation, in absence of decreases clauses, actually do something (that affects the IDE)?

Resolved in Silicon with PR https://github.com/viperproject/silicon/pull/597. Corresponding regression in PR https://github.com/viperproject/silver/pull/554. The latter should only be accepted once this Carbon is was resolved.

I don't have a strong opinion, but we should be careful not to let such corner cases prevent (in general important) optimisations.

Thank you for reporting these two issues. It would be great if you replaced this single issue with two separate ones: one for the exception (ideally with a way of...