Z3 Array which cannot be mutated

Question

I have the following smtlib code:

(declare-fun res () (Array Int Int))
(declare-fun other () (Array Int Int))
(assert (not (=> (= res other) 
    (forall ((x Int))
                 (< (select res x) 4)))
    ))

(assert (= (select other 0) 1))
(check-sat)
(get-model)

If I run it with z3 4.8.7 it is SAT and I get this model:

(model 
  (define-fun other () (Array Int Int)
    (store ((as const (Array Int Int)) 1) 2 4))
  (define-fun res () (Array Int Int)
    (store ((as const (Array Int Int)) 1) 2 4))
)

This means that both arrays are 'mutated' in order to fullfill the assertion (in the end it is making the forall-clause failing). But I would like the other-array to be fixed. At the moment it behaves like a variable (say integer variable) but I want it be rather a constant (like a fixed number, i.e. 1, in case of integers). Refering to the statement (assert (= (select other 0) 1)) it simply should contain a 1 at position 0 and this must be fixed. Is there a way to model this? If the other-array would behave like that then the above input should be UNSAT.

Thanks

Dwight Guth Dwight Guth · Accepted Answer · 2020-05-15T17:11:18

If you don't want one of the arrays to be treated as having a variable interpretation, you need to use (define-fun) to define it rather than (declare-fun). declare-fun declares an uninterpreted function, which means Z3 is free to assign any interpretation to it. If you look, the model you get back gives you some examples of how to use define-fun to define an array in smtlib.

Z3 Array which cannot be mutated

2 Answers