title: Unsatisfiable Cores in Z3 Python
body: <p>I am working with the Python API of Z3 in an attempt to include support for it in a research tool that I am writing. I have a question regarding extracting the unsatisfiable core using the Python interface.</p>
  
  <p>I have the following simple query:</p>
  
  <pre><code>(set-option :produce-unsat-cores true)
  (assert (! (not (= (_ bv0 32) (_ bv0 32))) :named __constraint0))
  (check-sat)
  (get-unsat-core)
  (exit)
  </code></pre>
  
  <p>Running this query through the z3 executable (for <strong>Z3 4.1</strong>), I receive the expected result:</p>
  
  <pre><code>unsat
  (__constraint0)
  </code></pre>
  
  <p>For <strong>Z3 4.3</strong>, I obtain a segmentation fault:</p>
  
  <pre><code>unsat
  Segmentation fault
  </code></pre>
  
  <p>That isn't the main question, although that was an intriguing observation. I then modified the query (inside a file) as</p>
  
  <pre><code>(assert (! (not (= (_ bv0 32) (_ bv0 32))) :named __constraint0))
  (exit)
  </code></pre>
  
  <p>Using a file handler, I passed the contents of this file (in a variable `queryStr') to the following Python code:</p>
  
  <pre><code>import z3
  ...
  solver = z3.Solver()
  solver.reset()
  solver.add(z3.parse_smt2_string(queryStr))
  querySatResult = solver.check()
  if querySatResult == z3.sat:
      ...
  elif querySatResult == z3.unsat:
      print solver.unsat_core()
  </code></pre>
  
  <p>I receive the empty list from the `unsat_core' function: []. Am I using this function incorrectly? The docstring for the function suggests that I should instead be doing something similar to</p>
  
  <pre><code>solver.add(z3.Implies(p1, z3.Not(0 == 0)))
  </code></pre>
  
  <p>However, I was wondering if it were still possible to use the query as is, since it conforms to SMT-LIB v2.0 standards (I believe), and whether I was missing something obvious. </p>