title: Z3 Java API - get unsat core
body: <p>I am trying to figure out how to get the unsat core using the Java API for Z3. Our scenario is as follows (code is underneath, which works in rise4fun):</p>
  
  <ol>
  <li>We create the SMT2 input programtically</li>
  <li>The input contains function definitions, datatype declarations, and assertions</li>
  <li>We parse this using the parseSMTLIB2String API</li>
  <li>We ensure that the context and the solver have unsat_core -> true </li>
  <li>Z3 returns UNSAT for the provided input, which is correct</li>
  <li>The UNSAT core is always empty though. </li>
  <li>The same input produces an UNSAT core correctly on rise4fun (x1 x3)</li>
  </ol>
  
  <p>I am guessing I am misusing the API somehow... but not quite sure how/why. </p>
  
  <p>I have noticed that I cannot set the unsat core option in the SMT string that I pass to parseSMTLIB2String, because that is not allowed. I am guessing that is expected.</p>
  
  <p>Can someone point me in the right direction please?</p>
  
  <p>Thanks!!</p>
  
  <pre><code>(set-option :smt.macro-finder true)
  
  ;; The following is only for rise4fun, i cannot get it 
  ;; to work with the parse SMT Java API
  (set-option :produce-unsat-cores true)
  
  (define-sort Ref () Int)
  
  (declare-datatypes (T1 T2) ((Tuple2 (mk-Tuple2 (_1 T1)(_2 T2)))))
  (declare-datatypes (T1 T2 T3) ((Tuple3 (mk-Tuple3 (_1 T1)(_2 T2)(_3 T3)))))
  
  (define-sort Set (T) (Array T Bool))
  (define-sort Bag (T) (Array T Int))
  
  (declare-const emptySetOf_Int (Set Int))
  (assert (!(forall ((x Int)) (= (select emptySetOf_Int x) false)) :named AXIOM1))
  
  (declare-sort TopLevelDeclarations) (declare-const mk-TopLevelDeclarations TopLevelDeclarations)
  (declare-datatypes () ((A (mk-A (x Int)(y Int)))))
  
  (declare-datatypes () ((Any
    (lift-TopLevelDeclarations (sel-TopLevelDeclarations TopLevelDeclarations))
    (lift-A (sel-A A))
    null))
  )
  
  (declare-const heap (Array Ref Any))
  
  (define-fun deref ((ref Ref)) Any
    (select heap ref)
  )
  
  (define-fun deref-is-TopLevelDeclarations ((this Ref)) Bool
    (is-lift-TopLevelDeclarations (deref this))
  )
  
  (define-fun deref-TopLevelDeclarations ((this Ref)) TopLevelDeclarations
    (sel-TopLevelDeclarations (deref this))
  )
  
  (define-fun deref-is-A ((this Ref)) Bool
    (is-lift-A (deref this))
  )
  
  (define-fun deref-A ((this Ref)) A
    (sel-A (deref this))
  )
  
  (define-fun deref-isa-TopLevelDeclarations ((this Ref)) Bool
    (deref-is-TopLevelDeclarations this)
  )
  
  (define-fun deref-isa-A ((this Ref)) Bool
    (deref-is-A this)
  )
  
  (define-fun A!x ((this Ref)) Int
    (x (deref-A this))
  )
  
  (define-fun A!y ((this Ref)) Int
    (y (deref-A this))
  )
  
  (define-fun TopLevelDeclarations.inv ((this Ref)) Bool
    true
  )
  
  (assert (! (forall ((this Ref))
    (=&gt; (deref-is-TopLevelDeclarations this) (TopLevelDeclarations.inv this))
  ) :named x0))
  
  (define-fun A.inv ((this Ref)) Bool
    (and
      (&gt; (A!x this)  0)
      (&gt; (A!y this)  0)
      (&lt; (A!x this)  0)
    )
  )
  
  (assert (! (forall ((this Ref))
    (=&gt; (deref-is-A this) (A.inv this))
  ) :named x1))
  
  (assert (!(deref-is-TopLevelDeclarations 0) :named TOP))
  (assert (!(exists ((instanceOfA Ref)) (deref-is-A instanceOfA)) :named x3))
  
  (check-sat)
  (get-unsat-core)
  </code></pre>