Replies: 1 comment
-
These constraints only apply to the constant |
Beta Was this translation helpful? Give feedback.
0 replies
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Uh oh!
There was an error while loading. Please reload this page.
-
Please advise, intuitively I don't understand the behavior of z3.
As a result, the return value of findMin has been limited to i~3,
but the final m1 may be a value much greater than 3.
(declare-const aa (Array Int Int))
(assert (forall((i Int)) (=> (and (>= i 0) (< i 4))
(and (>= (findMin aa i 4) i)
(< (findMin aa i 4) 4)) ;return i~3
)))
(declare-const cc0 (Array Int Int))
(declare-const m0 Int) (declare-const m1 Int)
(assert (= m0 (findMin aa 0 4)))
(assert (= cc0 (store (store
aa m0 (select aa 0)) 0 (select aa m0))))
(assert (= m1 (findMin cc0 1 4)))
;m1 may be >3
Beta Was this translation helpful? Give feedback.
All reactions