title: Optimize in Z3 .NET API giving incorrect results - bug?
body: <p>I am using the .NET API for Z3 and I have discovered strange behaviour (possibly bug in the optimizer) using the code bellow. When run with the class Optimize, it incorrectly finds a solution, whereas when run with the class Solver, it correctly reports infeasible. Could anyone please run the code to verify my statement? Any hint on what is going on will be highly appreciated.</p>
  
  <p>Kind regards</p>
  
  <p>Marek</p>
  
  <pre><code>using System;
  using System.Collections.Generic;
  using Microsoft.Z3;
  
  namespace DS
  {
      class Program
      {
          static void Main(string[] args)
          {
              SMTtest smt = new SMTtest();
              if (smt.Solve())
              {
                  Console.WriteLine("Solved");
              }
              else
              {
                  Console.WriteLine("Infeasible");
              }
          }
      }
  
      class SMTtest
      {
          public bool Solve()
          {
              using (Context ctx = new Context(new Dictionary&lt;string, string&gt;() { { "model", "true" } }))
              {
                  Optimize optimizer = ctx.MkOptimize();
                  //Solver optimizer = ctx.MkSolver();
  
                  int numOfTasks = 19;
                  IntExpr[] time = new IntExpr[numOfTasks * 2];
                  BoolExpr[] select = new BoolExpr[numOfTasks];
  
                  for (int i = 0; i &lt; numOfTasks; i++)
                  {
                      select[i] = ctx.MkBoolConst("valid" + i.ToString());
                  }
                  for (int i = 0; i &lt; numOfTasks * 2; i++)
                  {
                      time[i] = ctx.MkIntConst("time" + i.ToString());
                  }
  
                  optimizer.Assert(ctx.MkEq(select[1], select[0]));
                  optimizer.Assert(ctx.MkImplies(select[0], ctx.MkLe(time[0], time[1])));
                  optimizer.Assert(ctx.MkImplies(select[0], ctx.MkGe(time[19], time[20])));
                  optimizer.Assert(ctx.MkEq(select[8], select[0]));
                  optimizer.Assert(ctx.MkImplies(select[0], ctx.MkLe(time[0], time[8])));
                  optimizer.Assert(ctx.MkImplies(select[0], ctx.MkGe(time[19], time[27])));
                  optimizer.Assert(ctx.MkImplies(select[0], ctx.MkOr(ctx.MkEq(time[0], time[1]), ctx.MkEq(time[0], time[8]))));
                  optimizer.Assert(ctx.MkImplies(select[0], ctx.MkOr(ctx.MkEq(time[19], time[20]), ctx.MkEq(time[19], time[27]))));
                  optimizer.Assert(ctx.MkEq(select[2], select[1]));
                  optimizer.Assert(ctx.MkImplies(select[1], ctx.MkLe(time[1], time[2])));
                  optimizer.Assert(ctx.MkImplies(select[1], ctx.MkGe(time[20], time[21])));
                  optimizer.Assert(ctx.MkEq(select[5], select[1]));
                  optimizer.Assert(ctx.MkImplies(select[1], ctx.MkLe(time[1], time[5])));
                  optimizer.Assert(ctx.MkImplies(select[1], ctx.MkGe(time[20], time[24])));
                  optimizer.Assert(ctx.MkImplies(select[1], ctx.MkOr(ctx.MkEq(time[1], time[2]), ctx.MkEq(time[1], time[5]))));
                  optimizer.Assert(ctx.MkImplies(select[1], ctx.MkOr(ctx.MkEq(time[20], time[21]), ctx.MkEq(time[20], time[24]))));
                  optimizer.Assert(ctx.MkImplies(select[3], ctx.MkEq(time[2], time[3])));
                  optimizer.Assert(ctx.MkImplies(select[3], ctx.MkEq(time[21], time[22])));
                  optimizer.Assert(ctx.MkImplies(select[4], ctx.MkEq(time[2], time[4])));
                  optimizer.Assert(ctx.MkImplies(select[4], ctx.MkEq(time[21], time[23])));
                  optimizer.Assert(ctx.MkEq(select[2], ctx.MkOr(select[3], select[4])));
                  optimizer.Assert(ctx.MkAtMost(new BoolExpr[] { select[3], select[4] }, 1));
                  optimizer.Assert(select[3]);
                  optimizer.Assert(ctx.MkEq(time[3], ctx.MkInt(0)));
                  optimizer.Assert(ctx.MkEq(time[22], ctx.MkInt(4)));
                  optimizer.Assert(ctx.MkNot(select[4]));
                  optimizer.Assert(ctx.MkImplies(select[6], ctx.MkEq(time[5], time[6])));
                  optimizer.Assert(ctx.MkImplies(select[6], ctx.MkEq(time[24], time[25])));
                  optimizer.Assert(ctx.MkImplies(select[7], ctx.MkEq(time[5], time[7])));
                  optimizer.Assert(ctx.MkImplies(select[7], ctx.MkEq(time[24], time[26])));
                  optimizer.Assert(ctx.MkEq(select[5], ctx.MkOr(select[6], select[7])));
                  optimizer.Assert(ctx.MkAtMost(new BoolExpr[] { select[6], select[7] }, 1));
                  optimizer.Assert(select[6]);
                  optimizer.Assert(ctx.MkEq(time[6], ctx.MkInt(0)));
                  optimizer.Assert(ctx.MkEq(time[25], ctx.MkInt(1)));
                  optimizer.Assert(ctx.MkImplies(select[7], ctx.MkGe(time[7], ctx.MkInt(7))));
                  optimizer.Assert(ctx.MkImplies(select[7], ctx.MkEq(time[26], ctx.MkAdd(time[7], ctx.MkInt(1)))));
                  optimizer.Assert(ctx.MkEq(select[9], select[8]));
                  optimizer.Assert(ctx.MkImplies(select[8], ctx.MkLe(time[8], time[9])));
                  optimizer.Assert(ctx.MkImplies(select[8], ctx.MkGe(time[27], time[28])));
                  optimizer.Assert(ctx.MkEq(select[12], select[8]));
                  optimizer.Assert(ctx.MkImplies(select[8], ctx.MkLe(time[8], time[12])));
                  optimizer.Assert(ctx.MkImplies(select[8], ctx.MkGe(time[27], time[31])));
                  optimizer.Assert(ctx.MkImplies(select[8], ctx.MkOr(ctx.MkEq(time[8], time[9]), ctx.MkEq(time[8], time[12]))));
                  optimizer.Assert(ctx.MkImplies(select[8], ctx.MkOr(ctx.MkEq(time[27], time[28]), ctx.MkEq(time[27], time[31]))));
                  optimizer.Assert(ctx.MkImplies(select[10], ctx.MkEq(time[9], time[10])));
                  optimizer.Assert(ctx.MkImplies(select[10], ctx.MkEq(time[28], time[29])));
                  optimizer.Assert(ctx.MkImplies(select[11], ctx.MkEq(time[9], time[11])));
                  optimizer.Assert(ctx.MkImplies(select[11], ctx.MkEq(time[28], time[30])));
                  optimizer.Assert(ctx.MkEq(select[9], ctx.MkOr(select[10], select[11])));
                  optimizer.Assert(ctx.MkAtMost(new BoolExpr[] { select[10], select[11] }, 1));
                  optimizer.Assert(ctx.MkNot(select[10]));
                  optimizer.Assert(ctx.MkImplies(select[11], ctx.MkGe(time[11], ctx.MkInt(7))));
                  optimizer.Assert(ctx.MkImplies(select[11], ctx.MkEq(time[30], ctx.MkAdd(time[11], ctx.MkInt(14)))));
                  optimizer.Assert(ctx.MkEq(select[13], select[12]));
                  optimizer.Assert(ctx.MkImplies(select[12], ctx.MkLe(time[12], time[13])));
                  optimizer.Assert(ctx.MkImplies(select[12], ctx.MkGe(time[31], time[32])));
                  optimizer.Assert(ctx.MkEq(select[16], select[12]));
                  optimizer.Assert(ctx.MkImplies(select[12], ctx.MkLe(time[12], time[16])));
                  optimizer.Assert(ctx.MkImplies(select[12], ctx.MkGe(time[31], time[35])));
                  optimizer.Assert(ctx.MkImplies(select[12], ctx.MkOr(ctx.MkEq(time[12], time[13]), ctx.MkEq(time[12], time[16]))));
                  optimizer.Assert(ctx.MkImplies(select[12], ctx.MkOr(ctx.MkEq(time[31], time[32]), ctx.MkEq(time[31], time[35]))));
                  optimizer.Assert(ctx.MkImplies(select[14], ctx.MkEq(time[13], time[14])));
                  optimizer.Assert(ctx.MkImplies(select[14], ctx.MkEq(time[32], time[33])));
                  optimizer.Assert(ctx.MkImplies(select[15], ctx.MkEq(time[13], time[15])));
                  optimizer.Assert(ctx.MkImplies(select[15], ctx.MkEq(time[32], time[34])));
                  optimizer.Assert(ctx.MkEq(select[13], ctx.MkOr(select[14], select[15])));
                  optimizer.Assert(ctx.MkAtMost(new BoolExpr[] { select[14], select[15] }, 1));
                  optimizer.Assert(select[14]);
                  optimizer.Assert(ctx.MkEq(time[14], ctx.MkInt(1)));
                  optimizer.Assert(ctx.MkEq(time[33], ctx.MkInt(5)));
                  optimizer.Assert(ctx.MkImplies(select[15], ctx.MkGe(time[15], ctx.MkInt(7))));
                  optimizer.Assert(ctx.MkImplies(select[15], ctx.MkEq(time[34], ctx.MkAdd(time[15], ctx.MkInt(11)))));
                  optimizer.Assert(ctx.MkImplies(select[17], ctx.MkEq(time[16], time[17])));
                  optimizer.Assert(ctx.MkImplies(select[17], ctx.MkEq(time[35], time[36])));
                  optimizer.Assert(ctx.MkImplies(select[18], ctx.MkEq(time[16], time[18])));
                  optimizer.Assert(ctx.MkImplies(select[18], ctx.MkEq(time[35], time[37])));
                  optimizer.Assert(ctx.MkEq(select[16], ctx.MkOr(select[17], select[18])));
                  optimizer.Assert(ctx.MkAtMost(new BoolExpr[] { select[17], select[18] }, 1));
                  optimizer.Assert(ctx.MkNot(select[17]));
                  optimizer.Assert(ctx.MkImplies(select[18], ctx.MkGe(time[18], ctx.MkInt(7))));
                  optimizer.Assert(ctx.MkImplies(select[18], ctx.MkEq(time[37], ctx.MkAdd(time[18], ctx.MkInt(12)))));
                  optimizer.Assert(select[0]);
  
                  optimizer.Assert(ctx.MkImplies(ctx.MkAnd(select[5], select[8]), ctx.MkLe(ctx.MkSub(time[8], time[5]), ctx.MkInt(0))));
                  optimizer.Assert(ctx.MkImplies(ctx.MkAnd(select[8], select[5]), ctx.MkLe(ctx.MkSub(time[5], time[8]), ctx.MkInt(0))));
  
                  optimizer.Assert(ctx.MkImplies(ctx.MkAnd(select[3], select[7]), ctx.MkOr(ctx.MkGe(time[3], time[26]), ctx.MkGe(time[7], time[22]))));
                  optimizer.Assert(ctx.MkImplies(ctx.MkAnd(select[3], select[15]), ctx.MkOr(ctx.MkGe(time[3], time[34]), ctx.MkGe(time[15], time[22]))));
                  optimizer.Assert(ctx.MkImplies(ctx.MkAnd(select[4], select[10]), ctx.MkOr(ctx.MkGe(time[4], time[29]), ctx.MkGe(time[10], time[23]))));
                  optimizer.Assert(ctx.MkImplies(ctx.MkAnd(select[4], select[17]), ctx.MkOr(ctx.MkGe(time[4], time[36]), ctx.MkGe(time[17], time[23]))));
                  optimizer.Assert(ctx.MkImplies(ctx.MkAnd(select[6], select[11]), ctx.MkOr(ctx.MkGe(time[6], time[30]), ctx.MkGe(time[11], time[25]))));
                  optimizer.Assert(ctx.MkImplies(ctx.MkAnd(select[6], select[14]), ctx.MkOr(ctx.MkGe(time[6], time[33]), ctx.MkGe(time[14], time[25]))));
                  optimizer.Assert(ctx.MkImplies(ctx.MkAnd(select[6], select[18]), ctx.MkOr(ctx.MkGe(time[6], time[37]), ctx.MkGe(time[18], time[25]))));
                  optimizer.Assert(ctx.MkImplies(ctx.MkAnd(select[7], select[15]), ctx.MkOr(ctx.MkGe(time[7], time[34]), ctx.MkGe(time[15], time[26]))));
                  optimizer.Assert(ctx.MkImplies(ctx.MkAnd(select[10], select[17]), ctx.MkOr(ctx.MkGe(time[10], time[36]), ctx.MkGe(time[17], time[29]))));
                  optimizer.Assert(ctx.MkImplies(ctx.MkAnd(select[11], select[14]), ctx.MkOr(ctx.MkGe(time[11], time[33]), ctx.MkGe(time[14], time[30]))));
                  optimizer.Assert(ctx.MkImplies(ctx.MkAnd(select[11], select[18]), ctx.MkOr(ctx.MkGe(time[11], time[37]), ctx.MkGe(time[18], time[30]))));
                  optimizer.Assert(ctx.MkImplies(ctx.MkAnd(select[14], select[18]), ctx.MkOr(ctx.MkGe(time[14], time[37]), ctx.MkGe(time[18], time[33]))));
  
  
                  if (optimizer.Check() == Status.SATISFIABLE)
                  {
                      ctx.Dispose();
                      return true;
                  }
                  ctx.Dispose();
                  return false;
              }
          }
      }
  }
  </code></pre>