Questions tagged [z3]
The z3 tag has no usage guidance.
2
questions
4
votes
3
answers
344
views
How does Z3 "exhaustively search" real numbers?
I was looking at this tutorial: https://colab.research.google.com/github/philzook58/z3_tutorial/blob/master/Z3%20Tutorial.ipynb#scrollTo=4yuA2Fry68Y6&line=4&uniqifier=1 .
It says "Proof = ...
- 143
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