From ce4bf15e9dc545a8176fc73be14c0b27f98c486d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <mikael.mayer@epfl.ch>
Date: Mon, 14 Mar 2016 14:59:50 +0100
Subject: [PATCH] Bug fix: Z3 string ADT with type parameters.

---
 src/main/scala/leon/solvers/z3/Z3StringConversion.scala | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/main/scala/leon/solvers/z3/Z3StringConversion.scala b/src/main/scala/leon/solvers/z3/Z3StringConversion.scala
index b644f687a..75e7cc902 100644
--- a/src/main/scala/leon/solvers/z3/Z3StringConversion.scala
+++ b/src/main/scala/leon/solvers/z3/Z3StringConversion.scala
@@ -156,8 +156,8 @@ trait Z3StringConverters  {
     def convertExpr(expr: Expr)(implicit bindings: Map[Identifier, Expr]): Expr
     object TypeConverted {
       def unapply(t: TypeTree): Option[TypeTree] = Some(t match {
-        case cct@CaseClassType(ccd, args) => CaseClassType(convertClassDef(ccd).asInstanceOf[CaseClassDef], args)
-        case act@AbstractClassType(acd, args) => AbstractClassType(convertClassDef(acd).asInstanceOf[AbstractClassDef], args)
+        case cct@CaseClassType(ccd, args) => CaseClassType(convertClassDef(ccd).asInstanceOf[CaseClassDef], args map convertType)
+        case act@AbstractClassType(acd, args) => AbstractClassType(convertClassDef(acd).asInstanceOf[AbstractClassDef], args map convertType)
         case NAryType(es, builder) => 
           builder(es map convertType)
       })
@@ -280,7 +280,7 @@ trait Z3StringConverters  {
     def isTypeToConvert(tpe: TypeTree): Boolean = 
       TypeOps.exists(StringType == _)(tpe)
     def convertType(tpe: TypeTree): TypeTree = tpe match {
-      case StringType => StringList.typed
+      case StringType => StringListTyped
       case TypeConverted(t) => t
     }
     def convertPattern(e: Pattern): Pattern = e match {
@@ -344,7 +344,7 @@ trait Z3StringConverters  {
     def isTypeToConvert(tpe: TypeTree): Boolean = 
       TypeOps.exists(t => TypeOps.isSubtypeOf(t, StringListTyped))(tpe)
     def convertType(tpe: TypeTree): TypeTree = tpe match {
-      case StringList | StringCons | StringNil => StringType
+      case StringListTyped | StringConsTyped | StringNilTyped => StringType
       case TypeConverted(t) => t
     }
     def convertPattern(e: Pattern): Pattern = e match {
-- 
GitLab