From 1d1d624e4bd54670e31900922f1ce6eeef7b8b5b Mon Sep 17 00:00:00 2001
From: "Emmanouil (Manos) Koukoutos" <emmanouil.koukoutos@epfl.ch>
Date: Mon, 10 Nov 2014 18:33:03 +0100
Subject: [PATCH] bestRealType when extracting builder for FiniteMaps
---
src/main/scala/leon/purescala/Extractors.scala | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index 8803ae47d..419170251 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -113,8 +113,8 @@ object Extractors {
case (Seq(), Seq()) => expr.getType
case _ =>
MapType(
- leastUpperBound(keys.map(_.getType)).get,
- leastUpperBound(values.map(_.getType)).get
+ bestRealType(leastUpperBound(keys.map (_.getType)).get),
+ bestRealType(leastUpperBound(values.map(_.getType)).get)
)
}
FiniteMap(keys.zip(values)).setType(tpe)
--
GitLab