Add string parsing for Z3 4.8.12

Author: jad-hamza

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

@@ -224,7 +224,9 @@ trait SMTLIBParser {
       val MapType(from, to) = fromSMT(sort)
       FiniteMap(Seq.empty, d, from, to)
 
-    case _ => throw new MissformedSMTException(term, "Unknown SMT term of class: " + term.getClass)
+    case _ => throw new MissformedSMTException(term,
+      s"Unknown SMT term of class: ${term.getClass}:\n$term"
+    )
   }
 
   protected def fromSMT(sort: Sort)(implicit context: Context): Type = sort match {

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

@@ -153,11 +153,17 @@ trait Z3Target extends SMTLIBTarget with SMTLIBDebugger {
       case (FunctionApplication(QualifiedIdentifier(SimpleIdentifier(SSymbol("seq.unit")), None), Seq(SHexadecimal(hex))), _) =>
         StringLiteral(utils.StringUtils.decode(hex.repr))
 
+      case (FunctionApplication(QualifiedIdentifier(SimpleIdentifier(SSymbol("seq.unit")), None), args), Some(StringType())) =>
+        StringLiteral(args.map(fromSMT(_, Some(CharType())).asInstanceOf[CharLiteral].value).mkString)
+
       case (FunctionApplication(QualifiedIdentifier(SimpleIdentifier(SSymbol("str.++")), None), strs), _) =>
         val strings = strs.map(fromSMT(_, Some(StringType())))
         if (strings.isEmpty) StringLiteral("")
         else strings.tail.foldRight(strings.head)(StringConcat(_, _))
 
+      case (QualifiedIdentifier(SMTIdentifier(SSymbol("Char"), Seq(SNumeral(n))), None), Some(CharType())) =>
+        CharLiteral(n.toChar)
+
       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))