CODEWITHSUNDEEP
z3smtformal-verification
Daneshvar Amrollahi
Daneshvar Amrollahi

Reputation: 75

Expecting unsat instad of sat in Z3

I am facing a situation in which I am expecting to get UNSAT from Z3, but I'm getting SAT instead.

Here are the 4 constraints I believe are given to Z3:

1. (i = 0) ==> (forall j: 0 <= j < n ==> a[j] = b[j])

2. (i = 1) ==> (exists j: 0 <= j < n ==> a[j] != b[j])

3. i = 0

4. a[0] != b[0]

This should be obviously UNSAT. Because according to 1 and 3, we conclude that the array's a and b should be equal in every index. Thus a[0] can't be not-equal to b[0].

Here is the output's of Z3_ast_to_string(...) (I'm using the C API) for each constraint mentioned above:

1.

(let ((a!1 (concat (select memcmp_return_value #x00000003)
                   (concat (select memcmp_return_value #x00000002)
                           (concat (select memcmp_return_value #x00000001)
                                   (select memcmp_return_value #x00000000)))))
      (a!2 (forall ((fqv Int))
             (let ((a!1 (concat (select fqv #x00000003)
                                (concat (select fqv #x00000002)
                                        (concat (select fqv #x00000001)
                                                (select fqv #x00000000))))))
               (=> (and (bvsle #x00000000 a!1) (bvslt a!1 #x00000005))
                   (= (select a a!1) (select b a!1)))))))
  (=> (= #x00000000 a!1) a!2))

2.

(let ((a!1 (concat (select memcmp_return_value #x00000003)
                   (concat (select memcmp_return_value #x00000002)
                           (concat (select memcmp_return_value #x00000001)
                                   (select memcmp_return_value #x00000000)))))
      (a!2 (exists ((eqv Int))
             (let ((a!1 (concat (select eqv #x00000003)
                                (concat (select eqv #x00000002)
                                        (concat (select eqv #x00000001)
                                                (select eqv #x00000000))))))
               (and (bvsle #x00000000 a!1)
                    (bvslt a!1 #x00000005)
                    (not (= (select a a!1) (select b a!1))))))))
  (=> (= #x00000001 a!1) a!2))

3.

(let ((a!1 (concat (select memcmp_return_value #x00000003)
                   (concat (select memcmp_return_value #x00000002)
                           (concat (select memcmp_return_value #x00000001)
                                   (select memcmp_return_value #x00000000))))))
  (= #x00000000 a!1))

4.

(let ((a!1 (concat (select a #x00000003)
                   (concat (select a #x00000002)
                           (concat (select a #x00000001) (select a #x00000000)))))
      (a!2 (concat (select b #x00000003)
                   (concat (select b #x00000002)
                           (concat (select b #x00000001) (select b #x00000000))))))
  (not (= a!1 a!2)))

Note that memcmp_return_value represents i, fqv represents the forall quantified variable, and eqv represents the exists quantified variable.

The returned model be Z3 is:

(define-fun a2 () (Array (_ BitVec 32) (_ BitVec 8))
  (_ as-array k!22))
(define-fun fqv1 () (Array (_ BitVec 32) (_ BitVec 8))
  (_ as-array k!21))
(define-fun memcmp_return_value0 () (Array (_ BitVec 32) (_ BitVec 8))
  (_ as-array k!20))
(define-fun b3 () (Array (_ BitVec 32) (_ BitVec 8))
  (_ as-array k!23))
(define-fun k!23 ((x!0 (_ BitVec 32))) (_ BitVec 8)
  (ite (= x!0 #x00000003) #x00
    #x00))
(define-fun k!20 ((x!0 (_ BitVec 32))) (_ BitVec 8)
  (ite (= x!0 #x00000000) #x00
  (ite (= x!0 #x00000002) #x00
  (ite (= x!0 #x00000001) #x00
  (ite (= x!0 #x00000003) #x00
    #x00)))))
(define-fun k!21 ((x!0 (_ BitVec 32))) (_ BitVec 8)
  (ite (= x!0 #x00000002) #x00
  (ite (= x!0 #x00000000) #x00
  (ite (= x!0 #x00000003) #x80
  (ite (= x!0 #x00000001) #x00
    #x00)))))
(define-fun k!22 ((x!0 (_ BitVec 32))) (_ BitVec 8)
  (ite (= x!0 #x00000003) #x01
    #x01))

Is there any problem with the Z3_ast's created? Why is this giving me SAT?

Upvotes: 0

Views: 65

Answers (1)

alias
alias

Reputation: 30418

You really need to post the model speculated by z3. But it seems that what z3 is printing there doesn't match your narrative.

Take a look at (1). What's the value of a!1? Looks like it is the concatenation of the first 4 values in the array mem_cmp_return_value, in pseudo-code:

      memcmp_return_value[3:0]

this contradicts your claim that memcmp_return_value corresponds to i, since it is used clearly as an array. Ignoring that for a second, you then say:

  (and (bvsle #x00000000 a!1) (bvslt a!1 #x00000005))

which says this concatenation must be less than 5. z3 can easily pick an array where this is not true, this making (1) vacuously true.

I see similar problems in the other ones too.

Looks like your C/C++ program confused some variables there; it'd be best to be explicit with n is.

Long story short, impossible to answer without seeing your program that generated these constraints. But the parts you've shown us doesn't match the narrative you've given; and looks like this is indeed SAT as you're conflating the length of the array (n) with the concatenation of the values stored in the array itself.

Upvotes: 1

Related Questions