Неверный результат от z3

Question

Я пытаюсь доказать следующее с помощью Z3 SMT Solver: ((x*x) + x) = ((~x * ~x) + ~x).Это правильно из-за семантики переполнения в языке программирования C.

Теперь я написал следующий код smt-lib:

(declare-fun a () Int)

(define-fun myadd ((x Int) (y Int)) Int (mod (+ x y) 4294967296) )
(define-fun mynot ((x Int))         Int (- 4294967295 (mod x 4294967296)) )
(define-fun mymul ((x Int) (y Int)) Int (mod (* x y) 4294967296) )

(define-fun myfun1 ((x Int)) Int (myadd (mynot x) (mymul (mynot x) (mynot x))) )
(define-fun myfun2 ((x Int)) Int (myadd x (mymul x x)) )

(simplify (myfun1 0))
(simplify (myfun2 0))

(assert (= (myfun1 a) (myfun2 a)))
(check-sat)
(exit)

Вывод из z3:

0
0
unsat

Теперь мой вопрос: почему результат «ненасыщенный»?Команда упрощения в моем коде показывает, что можно получить правильное распределение, чтобы myfun1 и myfun2 имели одинаковый результат.

Что-то не так с моим кодом или это ошибка в z3?

Пожалуйста, кто-нибудь может мне помочь.Thx

Answer 1

Неправильный результат произошел из-за ошибки в препроцессоре формулы / выражения Z3.Ошибка была исправлена ​​и уже является частью текущей версии (v4.3.1).Ошибка затронула тесты, использующие формулы вида: (mod (+ a b)) или (mod (* a b)).

Мы можем повторить пример в режиме онлайн здесь и получить ожидаемый результат.