Weird result provided by Bitvector Division by Zero

[yu810226]

Hi,
I saw discussion related to this topic, but is quite a while ago. issue 190

I run z3 (version 4.8.0) for the following contents:

(assert (= x (bvudiv #b0 #b0)))
(assert (= x #b1))
(check-sat)
(get-model)

The result is:

(model
  (define-fun x () (_ BitVec 1)
    #b1)
)

which make sense to me if we consider we are solving equations: x * 0 = 0

But if I try to modify #b1 to #b0 like below contents:

(assert (= x (bvudiv #b0 #b0)))
(assert (= x #b0))
(check-sat)
(get-model)

I got unsat from z3. If I did not mess up the concept, I think the result should be sat.
I also try to use (set-logic QF_UFBV). But still got the same result.

And after running the above code, the result of the following contents is also weird to me:

(declare-const y (_ BitVec 1))  
(assert (bvumul_noovfl x y))  
(assert (not (= (bvudiv (bvmul x y) y) x)))  
(check-sat)  
(get-model)

I got result:

(model  
  (define-fun y () (_ BitVec 1)  
    #b0)  
  (define-fun x () (_ BitVec 1)  
    #b0)  
)

From previous result, this should be unsat.

Is there any reason for results like this?

Thanks!

[NikolajBjorner]

I don't see why the second case should be unsat. If bvudiv(0,0) = 1, then 0 != 1 is satisfied along with that multiplication of 0 and 0 does not overflow.
By default, Z3 implements the "hardware" semantics of division by 0, which is 2^n - 1, where n is the bit-width. For bit-width = 1, the result of division by 0 is 1. You can turn off the hardware semantics using the configuration option rewriter.hi_div0. In this case division is under-specified.

   z3 bv.smt2 rewriter.hi_div0=true
   unsat
   sat
      (model
          (define-fun y () (_ BitVec 1)
         #b0)
         (define-fun x () (_ BitVec 1)
         #b0)
     )

    z3 bv.smt2 rewriter.hi_div0=false
    sat
    sat
    (model
         (define-fun y () (_ BitVec 1)
        #b0)
        (define-fun x () (_ BitVec 1)
        #b0)
       (define-fun bvudiv0 ((x!0 (_ BitVec 1))) (_ BitVec 1)
              #b1)
     )

[NikolajBjorner]

can we close this?

[yu810226]

Yes, thanks a lot for your explanation!:)
Good to know how z3 implements division by 0.