fix bug while reading int literal from z3 models

src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala

@@ -23,7 +23,10 @@ trait Z3ModelReconstruction {
     variables.getZ3(id.toVariable).flatMap { z3ID =>
       expectedType match {
         case BooleanType => model.evalAs[Boolean](z3ID).map(BooleanLiteral(_))
-        case Int32Type => model.evalAs[Int](z3ID).map(IntLiteral(_))
+        case Int32Type =>
+          model.evalAs[Int](z3ID).map(IntLiteral(_)).orElse{
+            model.eval(z3ID).flatMap(t => softFromZ3Formula(model, t))
+          }
         case IntegerType => model.evalAs[Int](z3ID).map(InfiniteIntegerLiteral(_))
         case other => model.eval(z3ID) match {
           case None => None

src/test/resources/regression/verification/purescala/invalid/Acc.scala

+import leon.annotation._
+import leon.lang._
+
+object Acc {
+
+  case class Acc(checking : Int, savings : Int)
+
+  def putAside(x: Int, a: Acc): Acc = {
+    require (x > 0 && notRed(a) && a.checking >= x)
+      Acc(a.checking - x, a.savings + x)
+  } ensuring {
+    r => notRed(r) && sameTotal(a, r)
+  }
+
+
+  def sameTotal(a1: Acc, a2: Acc): Boolean = {
+    a1.checking + a1.savings == a2.checking + a2.savings
+  }
+
+  def notRed(a: Acc) : Boolean = {
+    a.checking >= 0 && a.savings >= 0
+  }
+
+}

src/test/resources/regression/verification/purescala/valid/Acc.scala

+import leon.annotation._
+import leon.lang._
+
+object Acc {
+
+  case class Acc(checking : BigInt, savings : BigInt)
+
+  def putAside(x: BigInt, a: Acc): Acc = {
+    require (x > 0 && notRed(a) && a.checking >= x)
+      Acc(a.checking - x, a.savings + x)
+  } ensuring {
+    r => notRed(r) && sameTotal(a, r)
+  }
+
+
+  def sameTotal(a1: Acc, a2: Acc): Boolean = {
+    a1.checking + a1.savings == a2.checking + a2.savings
+  }
+
+  def notRed(a: Acc) : Boolean = {
+    a.checking >= 0 && a.savings >= 0
+  }
+
+}