title: Scala^Z3 (Z3 Version 3.2) and parsesmtlib2string(...) not working
body: <p>While trying to implement a test using parsesmtlib2string I hit an error:</p>
  
  <pre><code>println("Hello World!");
  var smtlib2String = ""
  smtlib2String += "(declare-fun x () bool)" + "\n"
  smtlib2String += "(declare-fun y () bool)" + "\n"
  smtlib2String += "(assert (= x y))" + "\n"
  smtlib2String += "(assert (= x true))" + "\n"
  //  smtlib2String += "(check-sat)" + "\n"
  //  smtlib2String += "(model)" + "\n"
  smtlib2String += "(exit)" + "\n"
  
  val cfg = new Z3Config
  val z3 = new Z3Context(cfg)
  
  z3.parseSMTLIB2String(smtlib2String)
  </code></pre>
  
  <p>When uncommenting "Check-sat" I get "unknown". 
  When uncommenting "model" I get "unsupported".</p>
  
  <p>Using F# with Z3 3.2 it would just give me a Term back, but in Scala the return type is Unit. I looked through the Z3-C API but didn't find a good example on how to use ist.</p>
  
  <p>So, what is the best way to get a model using smtlib2string?</p>
  
  <p>Btw: Using Scala^Z3 and building a Z3AST works just fine and I can get a model using .checkAndGetModel(). The SMT-LIB2 Code above works fine with the F# .NET parsesmtlib2string method.</p>
  
  <p>Using one of "getSMTLIBFormulas, getSMTLIBAssumptions, getSMTLIBDecls, getSMTLIBSorts" yields "Error: parser (data) is not available".</p>
  
  <p>Using "getSMTLIBError.size" yields "0".</p>