Move "seq.unit hex" from SMT extraction to Z3

Author: jad-hamza

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

@@ -106,9 +106,6 @@ 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)) {

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

@@ -150,6 +150,9 @@ trait Z3Target extends SMTLIBTarget with SMTLIBDebugger {
       case (QualifiedIdentifier(SimpleIdentifier(SSymbol("#unspecified")), None), Some(tpe)) =>
         Choose(ValDef.fresh("unspecified", tpe), BooleanLiteral(true))
 
+      case (FunctionApplication(QualifiedIdentifier(SimpleIdentifier(SSymbol("seq.unit")), None), Seq(SHexadecimal(hex))), _) =>
+        StringLiteral(utils.StringUtils.decode(hex.repr))
+
       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))