diff --git a/src/main/scala/leon/FairZ3Solver.scala b/src/main/scala/leon/FairZ3Solver.scala index 51330a3e37232eb761f74ac594363bd93990c69d..1c3f1c8ec6afa77526e62cc036a4fb1df0f93b77 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)())