From 778cc7ca331ffd610ba98d021b12ba9b4cc0e3cc Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Mon, 31 Oct 2016 10:18:25 +0100
Subject: [PATCH] More precise types
---
.../scala/inox/solvers/unrolling/QuantificationTemplates.scala | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala b/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
index 5c1d651e8..fa43474ea 100644
--- a/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
+++ b/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala
@@ -168,7 +168,7 @@ trait QuantificationTemplates { self: Templates =>
val inst: Variable = Variable(FreshIdentifier("inst", true), BooleanType)
val insts = inst -> encodeSymbol(inst)
val extraClause = mkImplies(pathVar._2, mkEquals(insts._2, pT))
- (Some(inst), Negative(insts), Seq(extraClause), Map.empty)
+ (Some(inst), Negative(insts), Seq(extraClause), Map.empty[Variable, Encoded])
case None =>
val q: Variable = Variable(FreshIdentifier("q", true), BooleanType)
--
GitLab