From f9b46be6fdbad3dce125fd0cac61b3d5e0ca473c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Thu, 7 Jun 2012 15:21:36 +0200
Subject: [PATCH] comment on the copy from FunctionTemplate
---
src/main/scala/leon/FairZ3Solver.scala | 2 ++
1 file changed, 2 insertions(+)
diff --git a/src/main/scala/leon/FairZ3Solver.scala b/src/main/scala/leon/FairZ3Solver.scala
index 1b68d6c46..4bfe5c048 100644
--- a/src/main/scala/leon/FairZ3Solver.scala
+++ b/src/main/scala/leon/FairZ3Solver.scala
@@ -1379,6 +1379,8 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
}
}
+ //this is mostly copied from FunctionTemplate. This is sort of a quick hack to the problem
+ //of the initial unrolling
def initialUnrolling0(formula: Expr): (Seq[Expr], Seq[(Identifier,Boolean)]) = {
var guardedExprs : Map[(Identifier,Boolean),Seq[Expr]] = Map.empty
--
GitLab