From 11e6dc97c12dcb29c93214956728a5051ef8a6ed Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Fri, 20 Sep 2013 17:43:58 +0200
Subject: [PATCH] Fix potential infinite loop with unlocking of reused blockers
Unlocking reused, already-unlocked blockers would result in a no-op
while still keeping this blocker into the list of blockers to address.
This patch makes sure that reused, unlocked blockers are excluded from
the worklist.
---
.../leon/solvers/z3/FairZ3SolverFactory.scala | 30 +++++++++----------
.../verification/purescala/valid/Nat.scala | 24 +++++++++++++++
2 files changed, 39 insertions(+), 15 deletions(-)
create mode 100644 src/test/resources/regression/verification/purescala/valid/Nat.scala
diff --git a/src/main/scala/leon/solvers/z3/FairZ3SolverFactory.scala b/src/main/scala/leon/solvers/z3/FairZ3SolverFactory.scala
index b4d187894..7f50b3e1c 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3SolverFactory.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3SolverFactory.scala
@@ -228,18 +228,20 @@ class FairZ3SolverFactory(val context : LeonContext, val program: Program)
}
private def registerBlocker(gen: Int, id: Z3AST, fis: Set[Z3FunctionInvocation]) {
- val z3ast = z3.mkNot(id)
- blockersInfo.get(id) match {
- case Some((exGen, origGen, _, exFis)) =>
- // PS: when recycling `b`s, this assertion becomes dangerous.
- // It's better to simply take the min of the generations.
- // assert(exGen == gen, "Mixing the same id "+id+" with various generations "+ exGen+" and "+gen)
-
- val minGen = gen max exGen
-
- blockersInfo(id) = ((minGen, origGen, z3ast, fis++exFis))
- case None =>
- blockersInfo(id) = ((gen, gen, z3ast, fis))
+ if (!wasUnlocked(id)) {
+ val z3ast = z3.mkNot(id)
+ blockersInfo.get(id) match {
+ case Some((exGen, origGen, _, exFis)) =>
+ // PS: when recycling `b`s, this assertion becomes dangerous.
+ // It's better to simply take the max of the generations.
+ // assert(exGen == gen, "Mixing the same id "+id+" with various generations "+ exGen+" and "+gen)
+
+ val maxGen = gen max exGen
+
+ blockersInfo(id) = ((maxGen, origGen, z3ast, fis++exFis))
+ case None =>
+ blockersInfo(id) = ((gen, gen, z3ast, fis))
+ }
}
}
@@ -293,13 +295,11 @@ class FairZ3SolverFactory(val context : LeonContext, val program: Program)
def unlock(id: Z3AST) : Seq[Z3AST] = {
assert(blockersInfo contains id)
-
- if(unlockedSet(id)) return Seq.empty
+ assert(!wasUnlocked(id))
val (gen, origGen, _, fis) = blockersInfo(id)
blockersInfo -= id
- val twice = wasUnlocked(id)
var newClauses : Seq[Z3AST] = Seq.empty
diff --git a/src/test/resources/regression/verification/purescala/valid/Nat.scala b/src/test/resources/regression/verification/purescala/valid/Nat.scala
new file mode 100644
index 000000000..c78693b66
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/Nat.scala
@@ -0,0 +1,24 @@
+import leon.Annotations._
+import leon.Utils._
+
+object Nat {
+ sealed abstract class Nat
+ case class Zero() extends Nat
+ case class Succ(num: Nat) extends Nat
+
+ def plus(a: Nat, b: Nat): Nat = a match {
+ case Zero() => b
+ case Succ(a1) => Succ(plus(a1, b))
+ }
+
+ def nat2Int(n: Nat): Int = n match {
+ case Zero() => 0
+ case Succ(n1) => 1 + nat2Int(n1)
+ }
+
+ def int2Nat(n: Int): Nat = if (n == 0) Zero() else Succ(int2Nat(n-1))
+
+ def sum_lemma(): Boolean = {
+ 3 == nat2Int(plus(int2Nat(1), int2Nat(2)))
+ }.holds
+}
--
GitLab