All Questions
Tagged with first-order-logic z3
1
question
0
votes
1
answer
59
views
Why doesn't the `div` predicate work here?
(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
- 11