Add model extraction for #unspecified and seq.unit

Author: jad-hamza

build.sbt

@@ -45,7 +45,7 @@ libraryDependencies ++= Seq(
 
 def ghProject(repo: String, version: String) = RootProject(uri(s"${repo}#${version}"))
 // lazy val smtlib = RootProject(file("../scala-smtlib"))
-lazy val smtlib = ghProject("https://github.com/epfl-lara/scala-smtlib.git", "5b9503e13d69c7116039a243025b2ce657c32c77")
+lazy val smtlib = ghProject("https://github.com/epfl-lara/scala-smtlib.git", "95b5d1ed2ee9c0c1ec5cabb3c0303d27a48131cd")
 
 lazy val scriptName = settingKey[String]("Name of the generated 'inox' script")
 

src/main/scala/inox/solvers/smtlib/SMTLIBParser.scala

@@ -106,6 +106,9 @@ trait SMTLIBParser {
     case SString(value) =>
       StringLiteral(utils.StringUtils.decode(value))
 
+    case FunctionApplication(QualifiedIdentifier(SimpleIdentifier(SSymbol("seq.unit")), None), Seq(SHexadecimal(hex))) =>
+      StringLiteral(utils.StringUtils.decode(hex.repr))
+
     case FunctionApplication(QualifiedIdentifier(SimpleIdentifier(SSymbol("distinct")), None), args) =>
       val es = args.map(fromSMT(_))
       val tpEs = (if (es.exists(_.getType == Untyped) && es.exists(_.getType != Untyped)) {
@@ -224,7 +227,9 @@ trait SMTLIBParser {
       val MapType(from, to) = fromSMT(sort)
       FiniteMap(Seq.empty, d, from, to)
 
-    case _ => throw new MissformedSMTException(term, "Unknown SMT term")
+    case _ => throw new MissformedSMTException(term,
+      " Unknown SMT term of class: " + term.getClass
+    )
   }
 
   protected def fromSMT(sort: Sort)(implicit context: Context): Type = sort match {

src/main/scala/inox/solvers/smtlib/Z3Target.scala

@@ -144,6 +144,12 @@ trait Z3Target extends SMTLIBTarget with SMTLIBDebugger {
             unsupported(t, "woot? tester for non-adt type")
         }
 
+      case (QualifiedIdentifier(SimpleIdentifier(SSymbol("#unspecified")), None), None) =>
+        throw new MissformedSMTException(t, "Cannot extract #unspecified symbol when type is unknown")
+
+      case (QualifiedIdentifier(SimpleIdentifier(SSymbol("#unspecified")), None), Some(tpe)) =>
+        Choose(ValDef.fresh("unspecified", tpe), BooleanLiteral(true))
+
       case (QualifiedIdentifier(ExtendedIdentifier(SSymbol("as-array"), k: SSymbol), _), Some(tpe @ MapType(keyType, valueType))) =>
         val Some(Lambda(Seq(arg), body)) = context.getFunction(k, FunctionType(Seq(keyType), valueType))