diff --git a/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala b/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala
index 1bdb9fe6ad22b91357e9c3cfa46cf0a29515f079..bb290cd89f8ef808b7561120d4e0325c57a189e2 100644
--- a/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala
+++ b/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
diff --git a/src/test/resources/regression/verification/purescala/invalid/Acc.scala b/src/test/resources/regression/verification/purescala/invalid/Acc.scala
new file mode 100644
index 0000000000000000000000000000000000000000..2edd23ab78401f64fe7e6623cf3ace59d35007a7
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/invalid/Acc.scala
@@ -0,0 +1,24 @@
+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
+  }
+
+}
diff --git a/src/test/resources/regression/verification/purescala/valid/Acc.scala b/src/test/resources/regression/verification/purescala/valid/Acc.scala
new file mode 100644
index 0000000000000000000000000000000000000000..681f750598d908be4aa4ce50c5cfd18f1465c9ef
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/Acc.scala
@@ -0,0 +1,24 @@
+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
+  }
+
+}