parsing bit vector constants from cvc4

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")
   }
 }

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)

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 {

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