title: Z3 solver returning unsat when formula should be satisfiable
body: <p>I got a 'simple' formula that the Z3 solver (python interface) seems unable to handle. It is running for quite some time (30 minutes) and then returning unkown even though I can find a satisfying assignment by hand in under a minute. This is the formula:</p>
  
  <pre><code>[Or(&lt;uc 1.0&gt; == 0, &lt;uc 1.0&gt; == 1),
   Or(&lt;uc 1.1&gt; == 0, &lt;uc 1.1&gt; == 1),
   Or(&lt;uc 1.2&gt; == 0, &lt;uc 1.2&gt; == 1),
   &lt;uc 1.0&gt; + &lt;uc 1.1&gt; + &lt;uc 1.2&gt; == 1,
   Or(&lt;uc 0.0&gt; == 0, &lt;uc 0.0&gt; == 1),
   Or(&lt;uc 0.1&gt; == 0, &lt;uc 0.1&gt; == 1),
   Or(&lt;uc 0.2&gt; == 0, &lt;uc 0.2&gt; == 1),
   &lt;uc 0.0&gt; + &lt;uc 0.1&gt; + &lt;uc 0.2&gt; == 1,
   Or(&lt;uc 2.0&gt; == 0, &lt;uc 2.0&gt; == 1),
   Or(&lt;uc 2.1&gt; == 0, &lt;uc 2.1&gt; == 1),
   Or(&lt;uc 2.2&gt; == 0, &lt;uc 2.2&gt; == 1),
   &lt;uc 2.0&gt; + &lt;uc 2.1&gt; + &lt;uc 2.2&gt; == 1,
   ForAll(c,
          Or(c &gt; 1000,
             Or(c &lt; -1000,
                ForAll(b,
                       Or(b &gt; 1000,
                          Or(b &lt; -1000,
                             ForAll(a,
                                    Or(a &gt; 1000,
                                       Or(a &lt; -1000,
                                          And(And(And(True,
                                          a ==
                                          &lt;uc 0.0&gt;*b +
                                          &lt;uc 0.1&gt;*c +
                                          &lt;uc 0.2&gt;*a),
                                          b ==
                                          &lt;uc 1.0&gt;*b +
                                          &lt;uc 1.1&gt;*c +
                                          &lt;uc 1.2&gt;*a),
                                          c ==
                                          &lt;uc 2.0&gt;*b +
                                          &lt;uc 2.1&gt;*c +
                                          &lt;uc 2.2&gt;*a))))))))))]
  </code></pre>
  
  <p>It may look a bit scary but let me walk you through it. 
  &lt; uc i.j> are all integer variables. I first specify that they
  should be either 0 or 1 and then I'm introducing the constraint
  that exactly one of them should be 1 and the others 
  need to be 0 (using the sum).</p>
  
  <p>In the second part you can ignore all the Or's which  bascially just limit my search space for each variable to [-1000, 1000]. I then have the inner most constraints which should imply: &lt; uc 0.2> = 1 &lt; uc 1.0> = 1 &lt; uc 2.1> = 1 and all other  = 0. That's all. I'm pretty sure the solver
  should be able to solve this but no luck. I can change the sum
  constraint to something like Or(&lt; uc 1.0>,&lt; uc 1.1>,&lt; uc 1.2>) which, funny
  enough, solves my problem in this case (the solver
  returns the correct assignment in seconds) but in general, this is
  obviously, not equivalent to what I want to have.</p>
  
  <p>Questions:</p>
  
  <ul>
  <li>Is there something like a bit, which I could use instead of Integers?</li>
  <li>Some recommended way to express the fact that exactly one argument is 1?</li>
  <li>Some other way to make this solvable <strong>without</strong> changing the second part of the formula.</li>
  </ul>
  
  <p>Thank you very much! </p>
  
  <p>// Edit: After playing around with a few options I 'solved' it by placing the side conditions after the ForAll condition (just swapping the two lines of code). This shouldn't make a difference at all but now he is finding the correct assignment in 0.5 seconds - what? I also tried the example with 4 variables (a,b,c,d) instead (a,b,c) but then again it runs for hours... Any help? Also chaning the sum with a length And/Or did not work.</p>