Skip to main content
edited tags; edited title
Link
Trebor
  • 4.3k
  • 1
  • 9
  • 40

Why "div" predicate doesn't the `div` predicate work here?

Source Link

Why "div" predicate doesn't work

(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