From a7b80a139add683ce3d75debb3f5924d18b421e0 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Mon, 20 Apr 2015 15:15:56 +0200
Subject: [PATCH] No guarantee that defined map entries are not None
---
src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala | 5 +++--
1 file changed, 3 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index 20c8c5ae0..8a38fd562 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -164,8 +164,9 @@ trait SMTLIBTarget {
// We expect a RawArrayValue with keys in from and values in Option[to],
// with default value == None
require(from == r.keyTpe && r.default == OptionManager.mkLeonNone(to))
- val elems = r.elems.mapValues {
- case CaseClass(leonSome, Seq(x)) => x
+ val elems = r.elems.flatMap {
+ case (k, CaseClass(leonSome, Seq(x))) => Some(k -> x)
+ case (k, _) => None
}.toSeq
finiteMap(elems, from, to)
--
GitLab