`div` returns two functions `div0` and `mod0` when `get-model`

[chansey97]

Hi,

Thank you for this awesome library.

I have a question about div:

In z3-4.8.12, when using div where the two arguments are both symbols, it will returns two unexpected div0 and mod0.

(declare-const _v10 Int)
(declare-const _v11 Int)
(assert (= 2 (div _v10 _v11)))
(assert (not (= _v11 0)))
(check-sat)
sat
(get-model)
(
  (define-fun _v10 () Int
    2)
  (define-fun _v11 () Int
    1)
  (define-fun div0 ((x!0 Int) (x!1 Int)) Int
    2)
  (define-fun mod0 ((x!0 Int) (x!1 Int)) Int
    0)
)

If the second argument of div is a numeric constant, then no problem:

(declare-const _v10 Int)
(assert (= 2 (div _v10 1)))
(check-sat)
sat
(get-model)
(
  (define-fun _v10 () Int
    2)
)

I also tried * where the two arguments are both symbols, no problem:

(declare-const _v10 Int)
(declare-const _v11 Int)
(assert (= 2 (* _v10 _v11)))
(check-sat)
sat
(get-model)
(
  (define-fun _v10 () Int
    2)
  (define-fun _v11 () Int
    1)
)

PS. I originally used the old version z3-4.8.7, it won't generate these two unexpected functions as well:

$ z3 -version
Z3 version 4.8.7 - 64 bit

$ z3 -in
(declare-const _v10 Int)
(declare-const _v11 Int)
(assert (= 2 (div _v10 _v11)))
(assert (not (= _v11 0)))
(check-sat)
sat
(get-model)
(model
  (define-fun _v11 () Int
    (- 1))
  (define-fun _v10 () Int
    (- 2))
)

Is the z3-4.8.12's behavior expected?

Why z3-4.8.12 return these two functions in a model?

Very thanks.

[chansey97]

I think I have understood the meaning of the div. It means division with quotient and remainder. It does not force the reminder to be equal to 0. I misunderstood it before, sorry.

Reference: http://smtlib.cs.uiowa.edu/theories-Ints.shtml