I am trying to learn using z3. So this question might be silly.
Why do I get a unexpected values for x___0 from Z3 when I use bvsmod as compared to bvadd in the following code. I'm using SSA to implement execution flow here.
Z3 instructions:
(set-option :pp.bv-literals false)
;
; The code
; x %= 5
; x * 2 == 8
; Implement SSA
; x1 = x0 % 5
; x1 * 2 == 8
;
(push)
(set-info :status unknown)
(declare-const x___0 (_ BitVec 32))
(declare-const x___1 (_ BitVec 32))
(assert (= x___1 (bvsmod x___0 (_ bv5 32))))
(assert (= (bvmul x___1 (_ bv2 32)) (_ bv8 32)))
(check-sat)
(get-model)
(pop)
;
; The code
; x += 1
; x * 2 == 8
; Implement SSA
; x1 = x0 + 1
; x1 * 2 == 8
;
(push)
(declare-const x___0 (_ BitVec 32))
(declare-const x___1 (_ BitVec 32))
(assert (= x___1 (bvadd x___0 (_ bv1 32))))
(assert (= (bvmul x___1 (_ bv2 32)) (_ bv8 32)))
(check-sat)
(get-model)
(pop)
Results:
sat
(model
(define-fun x___1 () (_ BitVec 32)
(_ bv4 32))
(define-fun x___0 () (_ BitVec 32)
(_ bv3720040335 32))
)
sat
(model
(define-fun x___1 () (_ BitVec 32)
(_ bv4 32))
(define-fun x___0 () (_ BitVec 32)
(_ bv3 32))
)
In case of equation where I use bvadd x___0 get a value 3, which makes sense.
Why do I get a value 3720040335 in case of bvsmod, which is no where near the expected value i.e. some value ending with 4?
There's nothing wrong with the value you are getting. Your encoding is just fine.
Notice that you are using 32-bit signed integers (implicitly implied by the call to bvsmod.) The model returned gives you the value 32-bit bit-vector value whose decimal equivalent is 3720040335. When interpreted as a signed-value, this is actually -574926961, and you can verify (-574926961) % 5 indeed equals 4 as you requested.
Note that the solver is free to give you any model that satisfies your constraints. If you want a more specific value, you'll need to add additional constraints to encode what "simple" should formally mean.