From 12896ea56ab2821e743973c265c6f486b2d3a5f7 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Mon, 26 Aug 2013 13:46:35 +0200
Subject: [PATCH] Replacing empty finite sets should keep type information
---
src/main/scala/leon/purescala/Extractors.scala | 12 +++++++++++-
1 file changed, 11 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index 8837ee937..5c2571719 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -88,7 +88,17 @@ object Extractors {
case CaseClass(cd, args) => Some((args, CaseClass(cd, _)))
case And(args) => Some((args, And.apply))
case Or(args) => Some((args, Or.apply))
- case FiniteSet(args) => Some((args, FiniteSet))
+ case FiniteSet(args) =>
+ Some((args,
+ { newargs =>
+ if (newargs.isEmpty) {
+ FiniteSet(Seq()).setType(expr.getType)
+ } else {
+ FiniteSet(newargs)
+ }
+ }
+ ))
+
case FiniteMap(args) => {
val subArgs = args.flatMap{case (k, v) => Seq(k, v)}
val builder: (Seq[Expr]) => Expr = (as: Seq[Expr]) => {
--
GitLab