From 2fe24a49808ac223c84066bb8374f8890fa48758 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Fri, 20 Feb 2015 14:01:36 +0100
Subject: [PATCH] fix bug while reading int literal from z3 models
---
.../solvers/z3/Z3ModelReconstruction.scala | 5 +++-
.../verification/purescala/invalid/Acc.scala | 24 +++++++++++++++++++
.../verification/purescala/valid/Acc.scala | 24 +++++++++++++++++++
3 files changed, 52 insertions(+), 1 deletion(-)
create mode 100644 src/test/resources/regression/verification/purescala/invalid/Acc.scala
create mode 100644 src/test/resources/regression/verification/purescala/valid/Acc.scala
diff --git a/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala b/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala
index 1bdb9fe6a..bb290cd89 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 000000000..2edd23ab7
--- /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 000000000..681f75059
--- /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
+ }
+
+}
--
GitLab