Z3's Spacer limitation for inferring quantified interpretations for non-linear CHCs?

[btwael]

Hello,

If we consider the following two programs:

Program 1:

int main() {
  unsigned int N;
  assume(N > 0);
  int array[N];
  unsigned int i = 0;
  while(i < N) {
    array[i] = 0;
    i++;
  }
  for(unsigned int k = 0; k < N; k++) {
    assert(array[k] == 0);
  }
  return 0;
}

Program 2:

void init_0(int array[], unsigned int N) {
  unsigned int i = 0;
  while(i < N) {
    array[i] = 0;
    i = i + 1;
  }
}
int main() {
  unsigned int N;
  assume(N > 0);
  int array[N];
  init_0(array, N);
  for(unsigned int k = 0; k < N; k++) {
    assert(array[k] == 0);
  }
  return 0;
}

I could model their safety verification using CHCs in SMT-LIB2 format. For the first one, I will get a linear CHCs problem with one unknown loop invariant to synthesize; and for the second program with the procedure call (assuming there is no inlining), a non-linear CHCs problem for which we have to find the precondition and the summary of the procedure init_0 as well as the invariant for the loop inside init_0. By example:

CHCs for program 1:

(set-logic HORN)

(declare-fun inv0 ((Array Int Int) Int Int) Bool)

(assert (forall
            ((arr (Array Int Int)) (i Int) (N Int))
            (=> (and (= i 0) (> N 0))
                (inv0 arr i N))))

(assert (forall
            ((arr (Array Int Int)) (i Int) (N Int)
             (|arr'| (Array Int Int)) (|i'| Int))
            (=> (and (inv0 arr i N)
                     (< i N)
                     (= |arr'| (store arr i 0))
                     (= |i'| (+ i 1)))
                (inv0 |arr'| |i'| N))))

 (assert (forall
            ((arr (Array Int Int)) (i Int) (N Int))
            (=> (and (inv0 arr i N)
                     (= i N)
                     (not (forall ((k Int)) (=> (and (<= 0 k) (< k N)) (= (select arr k) 0)))))
                false)))

(check-sat)
(get-model)

CHCs for program 2:

(set-logic HORN)

(declare-fun inv0 ((Array Int Int) Int Int (Array Int Int)) Bool)
(declare-fun |array_init_0@pre| ((Array Int Int) Int) Bool)
(declare-fun |array_init_0@summary| ((Array Int Int) Int (Array Int Int)) Bool)

(assert (forall
            ((arr (Array Int Int)) (N Int))
            (=> (> N 0)
                (|array_init_0@pre| arr N))))

(assert (forall
            ((arr (Array Int Int)) (N Int) (i Int))
            (=> (and (|array_init_0@pre| arr N) (= i 0))
                (inv0 arr i N arr))))

(assert (forall
            ((arr_0 (Array Int Int)) (i Int) (N Int) (arr (Array Int Int))
             (|arr'| (Array Int Int)) (|i'| Int))
            (=> (and (inv0 arr_0 i N arr)
                     (< i N)
                     (= |arr'| (store arr i 0))
                     (= |i'| (+ i 1)))
                (inv0 arr_0 |i'| N |arr'|))))

 (assert (forall
            ((arr_0 (Array Int Int)) (i Int) (N Int) (arr (Array Int Int)))
            (=> (and (inv0 arr_0 i N arr)
                     (= i N))
                (|array_init_0@summary| arr_0 N arr))))

 (assert (forall
            ((arr (Array Int Int)) (i Int) (N Int) (|arr'| (Array Int Int)) (k Int))
            (=> (and (> N 0)
                     (|array_init_0@pre| arr N)
                     (|array_init_0@summary| arr N |arr'|)
                     (<= 0 k) (< k N)
                     (not (= (select |arr'| k) 0)))
                false)))

(check-sat)
(get-model)

If I, now, call Z3's Spacer to solve this two problems using the any of the commands below:

z3 fp.spacer.mbqi=true fp.spacer.q3.use_qgen=true <smt-file>
z3 fp.spacer.mbqi=false fp.spacer.q3.use_qgen=true <smt-file>

Spacer will successfully solves the first problem of program 1 and timeouts for the second program.

My questions are the following

• Is it possible to make Spacer solve the second program's CHCs? if yes, what options must I use?
• Is there any limitation in the algorithm that Spacer implements to handle quantifiers that forbids/limits solving non-linear CHCs that require quantified interpretations?

Thank you so much!