(declare-fun pdiv (Int Int Int) Bool)
(assert (forall ((x Int) (y Int) (z Int)) (=> (= z (div x y)) (pdiv z x y))))
When I check sat, I've got unknown by Z3
Why "div" predicate doesn't work
Andrew
- 11
- 2