证明溢出检查表达式正确

我有一个C++函数,它包含一个表达式(溢出检查),这是可以用手证明的。我有一个优化的想法,这对我来说似乎是正确的,我找不到一个反例,但我想确保它是正确的。我听说过Z3,它看起来非常适合。我写了一个公式,Z3说 unsat 但问题是我不相信我得到的结果,因为我不完全理解我是否做得对(基于我以前获得的非凡结果的恐惧,但这是我的错,我认识到了)。

C++函数:

template <typename T>
bool add(int radix, int digit, T& n)
{
    assert(radix > 2);
    assert(radix <= 36);
    assert(digit >= 0);
    assert(digit < radix);

    T max = std::numeric_limits<T>::max();
    assert(max >= radix);

    // the overflows check
    if ((n > (max / radix)) || ((n * radix) > (max - digit)))
        return false;

    n = n * radix + digit;
    return true;
}

我想证明(除法是整数,不是实数部分):

(n > (max / radix)) || ((n * radix) > (max - digit)) & =; n > ((max - digit) / radix)

或者更一般地说,如果这些表达式在 (n * radix) > max 或 (n * radix + digit) > max

Z3代码我有:

(declare-const radix Int)
(assert (>= radix 2))
(assert (<= radix 36)) ; this is the upper bound we officially support

(declare-const digit Int)
(assert (>= digit 0))
(assert (< digit radix))

(declare-const max Int)
(assert (> max 0))
(assert (>= max radix)) ; this is a reasonable requirement
;(assert (>= max 256)) ; the smallest upper bound for C++ fundamentals, but UDTs can have it lower

(declare-const n Int)
(assert (<= n max))
;(assert (>= n 0)) ; not really, but usually

; our current check
;(assert (not (or
;  (> n (div max radix))
;  (> (* n radix) (- max digit))
;)))
; our optimized check
(assert (not
  (> n (div (- max digit) radix))
))

(assert (or
  (> (* n radix) max)           ; check no mul overflow
  (> (+ n digit) max)           ; check no add overflow
  (> (+ (* n radix) digit) max) ; check no muladd overflow
))

(check-sat)
(get-model)
(exit)

https://rise4fun.com/Z3/po1h