diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index e7224a9506d1029cd919545e85275868d2b2e6a8..92f6bf354e9593c8b5b008e495de2277a57054c2 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -578,12 +578,17 @@ trait AbstractZ3Solver extends Solver {
         }
         case Z3NumeralIntAST(None) => {
           val ts = t.toString
+          reporter.ifDebug(printer => printer(ts))(DebugSectionSynthesis)
           if(ts.length > 4 && ts.substring(0, 2) == "bv" && ts.substring(ts.length - 4) == "[32]") {
             val integer = ts.substring(2, ts.length - 4)
             tpe match {
-              case Int32Type => IntLiteral(integer.toInt)
+              case Int32Type => 
+                if(integer == "2147483648") IntLiteral(-1) else
+                IntLiteral(integer.toInt)
               case CharType  => CharLiteral(integer.toInt.toChar)
-              case IntegerType => InfiniteIntegerLiteral(BigInt(integer.toInt))
+              case IntegerType => 
+                if(integer == "2147483648") InfiniteIntegerLiteral(BigInt(-1)) else
+                InfiniteIntegerLiteral(BigInt(integer))
               case _ =>
                 reporter.fatalError("Unexpected target type for BV value: " + tpe.asString)
             }