diff --git a/project/Build.scala b/project/Build.scala
index 70c01e8e7ebb819bb3db49e5331b41d570de7d76..6d2daf1527803945de3a4f810f544ef5b738f079 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",     "0fec9f97f4220fa94b1f3f305f2e8b76a3cd1539")
-    lazy val scalaSmtLib = project("git://github.com/regb/scala-smtlib.git", "e721cf606f73c6ba41f7622c141a1eefef2c712d")
+    lazy val scalaSmtLib = project("git://github.com/regb/scala-smtlib.git", "8b37b5e95cd87093734ee342b484b1786c8c0bfe")
   }
 }
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index 0c69b047b7190194f32bfd74b962c8b2583728df..98a129ce277af80f6a04721c868f6820ba42680f 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -515,6 +515,7 @@ trait SMTLIBTarget {
     case (Core.True(), BooleanType)  => BooleanLiteral(true)
     case (Core.False(), BooleanType)  => BooleanLiteral(false)
 
+    case (FixedSizeBitVectors.BitVectorConstant(n, 32), Int32Type) => IntLiteral(n.toInt)
     case (SHexadecimal(hexa), Int32Type) => IntLiteral(hexa.toInt)
 
     case (SimpleSymbol(s), _: ClassType) if constructors.containsB(s) =>
@@ -553,6 +554,7 @@ trait SMTLIBTarget {
             FiniteArray(definedElements, Some(default), IntLiteral(size)).setType(at)
 
           } else {
+            println("size is: " + size)
             val entries = for (i <- 0 to size-1) yield elems.getOrElse(IntLiteral(i), default)
 
             FiniteArray(entries).setType(at)
diff --git a/src/main/scala/leon/utils/TypingPhase.scala b/src/main/scala/leon/utils/TypingPhase.scala
index 57f5c314ee1e5b7e9bad0752ccabba15d81553db..61eb37b36c0f41f65af5dfffd5febe47f9860628 100644
--- a/src/main/scala/leon/utils/TypingPhase.scala
+++ b/src/main/scala/leon/utils/TypingPhase.scala
@@ -35,6 +35,7 @@ object TypingPhase extends LeonPhase[Program, Program] {
       fd.precondition = {
         val argTypesPreconditions = fd.params.flatMap(arg => arg.tpe match {
           case cct : CaseClassType if cct.parent.isDefined => Seq(CaseClassInstanceOf(cct, arg.id.toVariable))
+          case (at : ArrayType) => Seq(GreaterEquals(ArrayLength(arg.id.toVariable), IntLiteral(0)))
           case _ => Seq()
         })
         argTypesPreconditions match {
diff --git a/src/test/resources/regression/verification/purescala/invalid/Array3.scala b/src/test/resources/regression/verification/purescala/invalid/Array3.scala
index 3145fb07fc6c0c697f6b373646a1baf78fb28c43..b7be061e3444ecfbb3ac44760cd15e2ac8c65e76 100644
--- a/src/test/resources/regression/verification/purescala/invalid/Array3.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/Array3.scala
@@ -5,6 +5,7 @@ import leon.lang._
 object Test {
 
   def find(c: Array[Int], i: Int): Int = {
+    require(i >= 0)
     if(c(i) == i)
       42
     else