Merge pull request #145 from jad-hamza/strpp

Stop Z3 zombies and add support for str.++

Author: samarion

src/main/scala/inox/solvers/SolverFactory.scala

@@ -36,14 +36,14 @@ object SolverFactory {
   import _root_.smtlib.interpreters._
 
   lazy val hasZ3 = try {
-    new Z3Interpreter("z3", Array("-in", "-smt2"))
+    new Z3Interpreter("z3", Array("-in", "-smt2")).interrupt()
     true
   } catch {
     case _: java.io.IOException => false
   }
 
   lazy val hasCVC4 = try {
-    new CVC4Interpreter("cvc4", Array("-q", "--lang", "smt2.5"))
+    new CVC4Interpreter("cvc4", Array("-q", "--lang", "smt2.5")).interrupt()
     true
   } catch {
     case _: java.io.IOException => false
@@ -131,7 +131,7 @@ object SolverFactory {
         case None if noPrefixName.startsWith("smt-z3:") =>
           val z3Exec = getZ3Executable(noPrefixName)
           val hasZ3Exec = try {
-            new Z3Interpreter(z3Exec, Array("-in", "-smt2"))
+            new Z3Interpreter(z3Exec, Array("-in", "-smt2")).interrupt()
             true
           } catch {
             case _: java.io.IOException => false

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

@@ -153,6 +153,11 @@ 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("str.++")), None), strs), _) =>
+        val strings = strs.map(fromSMT(_, Some(StringType())))
+        if (strings.isEmpty) StringLiteral("")
+        else strings.tail.foldRight(strings.head)(StringConcat(_, _))
+
       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))
 

src/main/scala/inox/solvers/unrolling/UnrollingSolver.scala

@@ -831,7 +831,7 @@ trait AbstractUnrollingSolver extends Solver { self =>
   }).recover {
     case e @ (_: InternalSolverError | _: Unsupported) =>
       if (reporter.isDebugEnabled) reporter.debug(e)
-      else if (!silentErrors) reporter.error(e.getMessage)
+      else if (!silentErrors && !abort) reporter.error(e.getMessage)
       config.cast(Unknown)
   }.get)
 }