title: Z3 using parseSMTLIB2String in Java API delivers false UNSAT once it devilverd one UNSAT
body: <p>My implementation of the Z3 SMT solver is rough, but I found the Java API to be very inaccessible.
  I use parseSMTLIB2String and it does the job well, until a SAT-check returns one UNSATISFIABLE. It then continues to return UNSATISFIABLE even with previous values that returned SATISFIABLE. Am I using the solver wrong?</p>
  
  <pre><code>public static Boolean checkSat(int checkMakespan, Flowshop fs) {
      String smtString = FlowShopSmtGen.generateSMTFromFlowshop(fs, checkMakespan);
      HashMap&lt;String, String&gt; cfg = new HashMap&lt;&gt;();
      Context ctx = new Context(cfg);
      BoolExpr fsresult = ctx.parseSMTLIB2String(smtString, null, null, null, null);
  
      Solver solver = ctx.mkSolver();
      solver.add(fsresult);
      Status s = solver.check();
      System.out.println(s);
  
      if (s == Status.SATISFIABLE) {
          return true;
      } else {
          return false;
      }
  }
  </code></pre>