diff --git a/project/Build.scala b/project/Build.scala
index 34aa3701901a43424a7b2b2d15e318800cc76e22..7d50352f7740e5a326996f02dd51a31ce127fd6c 100644
--- a/project/Build.scala
+++ b/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")
   }
 }
diff --git a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala b/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
index 56f7f4af4caf561d324c3a5144cbeeca9d064290..8f4d216f7197cc99296ffadf42672f057ccf6653 100644
--- a/src/main/scala/leon/solvers/combinators/UnrollingSolver.scala
+++ b/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
   }
 }
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index 51ac7672602daac2a787687befa49b8c4add8ac2..5c0276201141d5bd54303564a51fae4e80e6b1c1 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/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
 
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index c31506240b3233c981a9fabe570a7d83140993c2..53264c59c1f1b43b8a556d2811df9b3e9a5f6fc2 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/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
     }