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.

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
 

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

+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
+}