unrolling solver correclty interrupts its solver

Fixes a bug, where UnrollingSolver was interrupted but was not
stopping its internal solver, leading to a timeout not being
respected if the internal solver was stucked in a complicated
check operation. UnrollingSolver now takes a Solver with
Interruptible.

In order to do that, Leon now relies on a more recent version of
scala-smtlib, that provides a feature to kill the solver process
in a relatively clean way. Update the SMTLIBSolver code to
actually perform the kill operation on the interrupt.

project/Build.scala

@@ -80,6 +80,6 @@ object Leon extends Build {
     def project(repo: String, version: String) = RootProject(uri(s"${repo}#${version}"))
 
     lazy val bonsai      = project("git://github.com/colder/bonsai.git",     "8f485605785bda98ac61885b0c8036133783290a")
-    lazy val scalaSmtLib = project("git://github.com/regb/scala-smtlib.git", "1b85768a2a5384170a6d90f4aea56ca7330939fd")
+    lazy val scalaSmtLib = project("git://github.com/regb/scala-smtlib.git", "e721cf606f73c6ba41f7622c141a1eefef2c712d")
   }
 }

src/main/scala/leon/solvers/combinators/UnrollingSolver.scala

@@ -14,7 +14,7 @@ import solvers.templates._
 import utils.Interruptible
 import evaluators._
 
-class UnrollingSolver(val context: LeonContext, program: Program, underlying: IncrementalSolver) extends Solver with Interruptible {
+class UnrollingSolver(val context: LeonContext, program: Program, underlying: IncrementalSolver with Interruptible) extends Solver with Interruptible {
 
   val (feelingLucky, useCodeGen) = locally {
     var lucky            = false
@@ -255,9 +255,11 @@ class UnrollingSolver(val context: LeonContext, program: Program, underlying: In
 
   override def interrupt(): Unit = {
     interrupted = true
+    solver.interrupt()
   }
 
   override def recoverInterrupt(): Unit = {
+    solver.recoverInterrupt()
     interrupted = false
   }
 }

src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala

@@ -18,8 +18,15 @@ abstract class SMTLIBSolver(val context: LeonContext,
                             val program: Program)
   extends IncrementalSolver with Interruptible with SMTLIBTarget {
 
-  override def interrupt: Unit = {}
-  override def recoverInterrupt(): Unit = {}
+  protected var interrupted = false
+
+  override def interrupt: Unit = {
+    interrupted = true
+    interpreter.interrupt()
+  }
+  override def recoverInterrupt(): Unit = {
+    interrupted = false
+  }
 
   override def name: String = "smt-"+targetName
 

src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala

@@ -13,7 +13,7 @@ import Definitions._
 import utils.Bijection
 
 import _root_.smtlib.common._
-import _root_.smtlib.printer.{PrettyPrinter => SMTPrinter}
+import _root_.smtlib.printer.{RecursivePrinter => SMTPrinter}
 import _root_.smtlib.parser.Commands.{Constructor => SMTConstructor, _}
 import _root_.smtlib.parser.Terms.{Identifier => SMTIdentifier, Let => SMTLet, _}
 import _root_.smtlib.parser.CommandsResponses.{Error => ErrorResponse, _}
@@ -323,7 +323,7 @@ trait SMTLIBTarget {
         declareVariable(FreshIdentifier("Unit").setType(UnitType))
 
       case IntLiteral(i) => if (i > 0) Ints.NumeralLit(i) else Ints.Neg(Ints.NumeralLit(-i))
-      case CharLiteral(c) => FixedSizeBitVectors.BitVectorLit(Hexadecimal.fromInt(c.toInt).get)
+      case CharLiteral(c) => FixedSizeBitVectors.BitVectorLit(Hexadecimal.fromInt(c.toInt))
       case BooleanLiteral(v) => Core.BoolConst(v)
       case StringLiteral(s) => SString(s)
       case Let(b,d,e) =>
@@ -558,7 +558,7 @@ trait SMTLIBTarget {
     }
 
     interpreter.eval(cmd) match {
-      case ErrorResponse(msg) =>
+      case err@ErrorResponse(msg) if !interrupted =>
         reporter.fatalError("Unnexpected error from smt-"+targetName+" solver: "+msg)
       case res => res
     }