title: Strange results with quantified formula
body: <p>I am getting some strange results when I use the ForAll quantifier. My goal is to restrict the interpretation of a function foo to the following:</p>
  
  <pre><code>\Ax,y. foo(x,y)= if x=A &amp;&amp; y=B then C1 else C2
  </code></pre>
  
  <p>So if i assert the above into a context I should get back an interpretation for foo which essentially equivalent to the above. However I do not. What i get back is something like</p>
  
  <pre><code>foo(x,y)= if x=A &amp;&amp; y=B then C1 else C1
  </code></pre>
  
  <p>And I have no idea why. The code I am using is below (accessing Z3 via the .net API)</p>
  
  <pre><code>let ctx = new Context()
  let Sort1 = ctx.MkEnumSort("S1", [|"A";"AA"|])
  let Sort2 = ctx.MkEnumSort("S2", [|"B"|])
  let Sort3 = ctx.MkEnumSort("S3", [|"C1";"C2"|]) 
  let s1 = ctx.MkSymbol "s1"
  let s2 = ctx.MkSymbol "s2"
  let types = [|Sort1:&gt;Sort; Sort2:&gt;Sort |]
  let names = [|s1:&gt;Symbol ; s2:&gt;Symbol|]
  let vars = [| ctx.MkConst(names.[0],types.[0]);ctx.MkConst(names.[1],types.[1])|]
  
  let FDecl = ctx.MkFuncDecl("foo", [|Sort1:&gt;Sort;Sort2:&gt;Sort|], Sort3) 
  let f_body = ctx.MkITE(ctx.MkAnd(ctx.MkEq(vars.[0],getZ3Id("A",Sort1)), 
                                   ctx.MkEq(vars.[1], getZ3Id("B",Sort2))),
                         getZ3Id("C1",Sort3), 
                         getZ3Id("C2",Sort3)) 
  let f_app = FDecl.Apply vars //ctx.MkApp(FDecl, vars)
  let body = ctx.MkEq(f_app, f_body)
  
  let std_weight = uint32 1
  let form = ctx.MkForall(types, names, body, std_weight, null, null, null, null) 
             :&gt; BoolExpr
  let s = ctx.MkSolver() 
  satisfy s [|form|]
  s.Model
  </code></pre>
  
  <p>where <code>getZ3Id</code> converts the given string to the corresponding constant in the Enum</p>
  
  <pre><code>let getZ3Id (id,sort:EnumSort) = 
    let matchingConst zconst = zconst.ToString().Equals(id)
    Array.find matchingConst sort.Consts
  </code></pre>
  
  <p>And <code>satisfy</code> is:</p>
  
  <pre><code>let satisfy (s:Solver) formula =
      s.Assert (formula)
      let res = s.Check() 
      assert (res = Status.SATISFIABLE)
      s.Model
  </code></pre>
  
  <p>The model returns an interpretation for foo that returns C1 no matter what</p>
  
  <pre><code>(define-fun foo ((x!1 S1) (x!2 S2)) S3
    (ite (and (= x!1 A) (= x!2 B)) C1
      C1))
  </code></pre>
  
  <p>Could someone point out where I'm going wrong?
  thanks
  PS Also what is the difference between the two API calls to MkForAll - one takes sorts and names and other takes "bound constants"?</p>
  
  <hr>
  
  <p>Here is my further problem:
  If i define</p>
  
  <pre><code>let set1 = Set.map (fun (p:string)-&gt; ctx.MkConst(p,Sort3)) 
                     (new Set&lt;string&gt;(["C1"]))
  </code></pre>
  
  <p>and change the body of f</p>
  
  <pre><code>let f_body = ctx.MkITE(ctx.MkAnd(ctx.MkEq(vars.[0],getZ3Id("A",Sort1))), 
                                   ctx.MkEq(vars.[1], getZ3Id("B",Sort2))),
                         mkZ3Set ctx set1,
                         ctx.MkEmptySet Sort3)
  </code></pre>
  
  <p>where </p>
  
  <pre><code>let mkZ3Set (ctx:Context) exprs sort =
    Set.fold (fun xs x-&gt; ctx.MkSetAdd(xs,x)) (ctx.MkEmptySet(sort)) exprs
  </code></pre>
  
  <p>The Z3 formula looks reasonable</p>
  
  <pre><code>form= (forall ((s1 S1))
    (= (foo s1)
       (ite (and (= s1 A))
            (store ((as const (Array S3 Bool)) false) C1 true)
            ((as const (Array S3 Bool)) false))))
  </code></pre>
  
  <p>yet Z3 returns Unsatisfiable. Can you tell me why?</p>