From e538b2676795d688b8765adecbabfc0f02093220 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Tue, 17 Apr 2012 13:40:38 +0200
Subject: [PATCH] Fix problem with lazy call to typeToSort
---
src/main/scala/leon/FairZ3Solver.scala | 1 +
1 file changed, 1 insertion(+)
diff --git a/src/main/scala/leon/FairZ3Solver.scala b/src/main/scala/leon/FairZ3Solver.scala
index 51330a3e3..1c3f1c8ec 100644
--- a/src/main/scala/leon/FairZ3Solver.scala
+++ b/src/main/scala/leon/FairZ3Solver.scala
@@ -978,6 +978,7 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
case errorType => scala.sys.error("Unexpected type for singleton map: " + (ex, errorType))
}
case e @ EmptyMap(fromType, toType) => {
+ typeToSort(e.getType) //had to add this here because the mapRangeNoneConstructors was not yet constructed...
val fromSort = typeToSort(fromType)
val toSort = typeToSort(toType)
z3.mkConstArray(fromSort, mapRangeNoneConstructors(toType)())
--
GitLab