 <p>You're not using the Java API, except for the call to <code>parseSMTLIB2String</code>. This function does not execute any SMT commands and there is no function that would do that for you. <code>parseSMTLIB2String</code> exists exclusively to parse assertions, it will ignore everything else. For this particular problem, I recommend to simply pass the problem file to <code>z3.exe</code> either as a command line argument or via stdin (use <code>-in</code> option). This produces</p> <pre><code>unsat (x1 x3) </code></pre> <p>If the intent is to use the Java API for other things at a later point, see the <a href="https://github.com/Z3Prover/z3/blob/master/examples/java/JavaExample.java#L2078" rel="nofollow">Java API unsat core example</a>.</p>