title: (check-sat) then (check-sat-using qfnra-nlsat)
body: <p><strong>What I want to do:</strong> I would like to call <code>(check-sat)</code>, and then if the result is <code>unknown</code>, call <code>(check-sat-using qfnra-nlsat)</code>.</p>
  
  <p><strong>Why do I want to do this?:</strong> For my application the Z3 default tactics applied with <code>(check-sat)</code> are superior to anything I have devised using <code>(check-sat-using)</code>.  However, there are a few situations where <code>(check-sat)</code> returns <code>unknown</code>, but  <code>(check-sat-using ...)</code> with judiciously chosen tactics finds a result.  Here is an example:</p>
  
  <pre><code>(declare-fun x () Real)
  (declare-fun y () Real)
  (declare-fun z () Real)
  
  (declare-fun i () Int)
  (declare-fun j () Int)
  (declare-fun k () Int)
  
  (assert (= z (* x y)))
  (assert (= k (* i j)))
  (assert (&lt; k z))
  
  ; This returns unknown
  (check-sat)
  
  ; This gives a solution
  (check-sat-using qfnra-nlsat)
  (get-value (x y z i j k))
  </code></pre>
  
  <p><strong>What have I tried?:</strong> The closest I've come in a single SMT file is<code>(check-sat-using (or-else smt qfnra-nlsat)).</code> Unfortunately <code>(check-sat-using smt)</code> does not perform as well as <code>(check-sat)</code> for my purposes, so this is not an option.</p>