Z3:unknown result in Z3 C API

Question

In current Z3 context,assert " try(X,i,j) = ((X[i][j] == i*j)) " is already existed.the type of X is (Array Int (Array Int Int)).try(X,i,j) is a function and return type is bool.here is the Z3 context:

 (kernel
      (forall ((Y (Array Int (Array Int Int))) (i Int) (j Int))
        (let ((a!1 (= (+ (select (select Y i) j) (* (- 1) j i)) 0)))
          (= (try Y i j) a!1))))

I want prove Z3 ast:

 forall i[0..99],j[0..199]. try(X,i,j) 
    =>
       (forall i[0..49],j[0..199]. try(X,i,j) 
    &&  forall i[50..99],j[0..199]. try(X,i,j))

in other words, I check is not of this assert is sat. Z3 check result is unknow. but when i prove Z3 ast:

forall i[0..99],j[0..199]. (X[i][j] == i*j)
=>
  (forall i[0..49],j[0..199]. (X[i][j] == i*j)
&& forall i[50..99],j[0..199]. (X[i][j] == i*j))

Z3 prove result is valid,in other words,not of this assert is unsat.

Christoph Wintersteiger Christoph Wintersteiger · Accepted Answer · 2015-02-03T10:20:05

I'm not sure that I understand the question, but in general we cannot expect Z3 to solve all formulas with quantifiers. In this particular case it might help to enable the macro-finder, which propagates function definitions like the

(forall ... (= (try ...) def )))

which replaces all occurrences of try with def. The option name for that is smt.macro_finder.

Z3:unknown result in Z3 C API

1 Answers