Potential TruncDiv performance improvement

[superaxander]

I came across this cvc5 issue. The initial example here looks very similar to our truncated division implementation. Later in the conversation a supposedly faster alternative is mentioned:

(define-fun cdiv ((x Int) (y Int)) Int
  (ite (<= 0 x)
    (div x y)
    (- (div (- x) y))))

I checked with Z3 and CVC5 to see if the two definitions match and they do except when the divisor is 0 which should not matter. I think we should try and see if that definition is also faster for us.

Also mentioned in that issue (in fact that's what the issue is about) is that the macro definition (define-fun) seems to work a lot better than the quantifier version. I would be interested in seeing if this difference is also noticeable with Z3 and whether we can emit Z3 macros. (or just simply insert the operator inline instead of with a function) Unfortunately it seems that Viper encodes prover functions with declare-fun and a quantifier like normal functions.

Do we have any examples that are (relatively) slow due to truncdiv/truncmod?