From 20d2dd6e2eae76b6135e9e2582ca865dd1d75e89 Mon Sep 17 00:00:00 2001
From: Philippe Suter <philippe.suter@gmail.com>
Date: Sun, 13 Jan 2013 22:52:13 +0100
Subject: [PATCH] `max` is better for fairness
---
src/main/scala/leon/solvers/z3/FairZ3Solver.scala | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index 466e1c0ae..42f60df91 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -271,7 +271,7 @@ class FairZ3Solver(context : LeonContext)
// 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 min exGen
+ val minGen = gen max exGen
blockersInfo(id) = ((minGen, origGen, z3ast, fis++exFis))
case None =>
--
GitLab