From ed286908045c68b945f4c92820fbde52aa711c36 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Tue, 30 Aug 2016 14:02:22 +0200
Subject: [PATCH] Fixed small typing bug in InductiveUnrollingSuite
---
.../scala/inox/solvers/unrolling/InductiveUnrollingSuite.scala | 2 +-
src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala | 1 -
2 files changed, 1 insertion(+), 2 deletions(-)
diff --git a/src/it/scala/inox/solvers/unrolling/InductiveUnrollingSuite.scala b/src/it/scala/inox/solvers/unrolling/InductiveUnrollingSuite.scala
index 753145736..a6a47106d 100644
--- a/src/it/scala/inox/solvers/unrolling/InductiveUnrollingSuite.scala
+++ b/src/it/scala/inox/solvers/unrolling/InductiveUnrollingSuite.scala
@@ -38,7 +38,7 @@ class InductiveUnrollingSuite extends SolvingTestSuite {
val append = mkFunDef(appendID)("A") { case Seq(aT) => (
Seq("l1" :: T(listID)(aT), "l2" :: T(listID)(aT)), T(listID)(aT), { case Seq(l1, l2) =>
if_ (l1.isInstOf(T(consID)(aT))) {
- let("c" :: T(listID)(aT), l1.asInstOf(T(consID)(aT))) { c =>
+ let("c" :: T(consID)(aT), l1.asInstOf(T(consID)(aT))) { c =>
T(consID)(aT)(c.getField(head), E(appendID)(aT)(c.getField(tail), l2))
}
} else_ {
diff --git a/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala b/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala
index d9e5836dd..8d519087e 100644
--- a/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/DatatypeTemplates.scala
@@ -259,7 +259,6 @@ trait DatatypeTemplates { self: Templates =>
}
def unroll: Clauses = if (typeInfos.isEmpty) Seq.empty else {
- println("unrolling datatypes")
val blockers = typeInfos.filter(_._2._1 <= currentGeneration).toSeq.map(_._1)
val newClauses = new scala.collection.mutable.ListBuffer[Encoded]
--
GitLab