title: Read func interp of a z3 array from the z3 model
body: <p>Suppose I have 2 arrays in a formula whose satisfiability I want to check using z3. If z3 returns sat, I want to read in the first array in the z3 model and pretty print it as a key, value pair and a default value. Later I want to convert it to a map and do further analysis on it. Here's the example I run:</p>
  
  <pre class="lang-cpp prettyprint-override"><code>void find_model_example_arr() {
    std::cout &lt;&lt; "find_model_example_involving_array\n";
    context c;
    sort arr_sort = c.array_sort(c.int_sort(), c.int_sort());
    expr some_array_1 = c.constant("some_array_1", arr_sort);
    expr some_array_2 = c.constant("some_array_2", arr_sort);
    solver s(c);
  
    s.add(select(some_array_1, 0) &gt; 0);
    s.add(select(some_array_2, 5) &lt; -4);
    std::cout &lt;&lt; s.check() &lt;&lt; "\n";
  
    model m = s.get_model();
    std::cout &lt;&lt; m &lt;&lt; "\n";
  
    expr some_array_1_eval = m.eval(some_array_1);
  
    std::cout &lt;&lt; "\nsome_array_1_eval = " &lt;&lt; some_array_1_eval &lt;&lt; "\n";
  
    func_decl some_array_1_eval_func_decl = some_array_1_eval.decl();
    std::cout &lt;&lt; "\nThe Z3 expr(fun_decl) for some_array_1_eval is : " &lt;&lt; some_array_1_eval_func_decl &lt;&lt; "\n";
  
    // ERROR here
    func_interp fun_interp = m.get_func_interp(some_array_1_eval_func_decl);
    // This works well 
    //func_interp fun_interp = m.get_func_interp(m.get_func_decl(0)); 
  
    std::cout &lt;&lt; "\nThe Z3 expr(fun_interp) for the array is : " &lt;&lt; fun_interp &lt;&lt; "\n";
  
    unsigned num_entries = fun_interp.num_entries();
    for(unsigned i = 0; i &lt; num_entries; i++) 
    {
      z3::func_entry entry = fun_interp.entry(i);
      z3::expr k = entry.arg(0);
  
      z3::expr v = entry.value();
  
      std::cout &lt;&lt; "\n(key,value): (" &lt;&lt; k &lt;&lt; "," &lt;&lt; v &lt;&lt; ")";
    }
  
    z3::expr default_value = fun_interp.else_value();
    std::cout &lt;&lt; "\nDefault value:" &lt;&lt; default_value;
  }
  </code></pre>
  
  <p>I get the following output:</p>
  
  <pre><code>find_model_example_involving_array 
  sat 
  (define-fun some_array_1 () (Array Int Int)   
    (_ as-array k!0)) 
  (define-fun some_array_2 () (Array Int Int)  
    (_ as-array k!1))
  (define-fun k!0 ((x!1 Int)) Int
    (ite (= x!1 0) 1
      1)) 
  (define-fun k!1 ((x!1 Int)) Int
    (ite (= x!1 5) (- 5)
      (- 5)))
  
  some_array_1_eval = (_ as-array k!0)
  
  The Z3 expr(fun_decl) for some_array_1_eval is : 
  (declare-fun as-array () (Array  Int Int)) 
  unexpected error: invalid argument
  </code></pre>
  
  <p>Instead if I comment out the first line and use the second, ie use the following code block:</p>
  
  <pre><code>// ERROR here
  // func_interp fun_interp = m.get_func_interp(some_array_1_eval_func_decl);
  // This works well 
  func_interp fun_interp = m.get_func_interp(m.get_func_decl(0)); 
  </code></pre>
  
  <p>I get the output I am looking for:</p>
  
  <pre><code>(key,value): (0,1)
  Default value:1
  </code></pre>
  
  <p>Here's the problem though? How do I figure out that m.get_func_decl(0) is the one corresponding to some_array_1? For instance, if I use m.get_func_decl(1), I get wrong (key, value) pairs. Is other words how do I get a func_interp of an array (defined as a z3 expr) from a model?</p>