diff --git a/src/main/scala/leon/FairZ3Solver.scala b/src/main/scala/leon/FairZ3Solver.scala index 1b68d6c467d4f85527825dbd1e724a98909ed26d..4bfe5c0484a48fc34b71b13fde7a08635cd0f5cc 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