diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala index f5b82b8f43480c8938a4368588f41db177936f91..44d4e90bfc6880d1683ddbcadc90f1e05afe793f 100644 --- a/src/main/scala/leon/purescala/PrettyPrinter.scala +++ b/src/main/scala/leon/purescala/PrettyPrinter.scala @@ -235,18 +235,18 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe isListLiteral(e) match { case Some((tpe, elems)) => val chars = elems.collect{case CharLiteral(ch) => ch} - if (chars.length == elems.length) { + if (chars.length == elems.length && tpe == CharType) { // String literal val str = chars mkString "" val q = '"' p"$q$str$q" - } - - val elemTps = leastUpperBound(elems.map(_.getType)) - if (elemTps == Some(tpe)) { - p"List($elems)" } else { - p"List[$tpe]($elems)" + val elemTps = leastUpperBound(elems.map(_.getType)) + if (elemTps == Some(tpe)) { + p"List($elems)" + } else { + p"List[$tpe]($elems)" + } } case None => @@ -268,7 +268,7 @@ class PrettyPrinter(opts: PrinterOptions, val sb: StringBuffer = new StringBuffe case BVUMinus(expr) => p"-$expr" case Equals(l,r) => optP { p"$l == $r" } case IntLiteral(v) => p"$v" - case InfiniteIntegerLiteral(v) => p"BigInt($v)" + case InfiniteIntegerLiteral(v) => p"$v" case CharLiteral(v) => p"$v" case BooleanLiteral(v) => p"$v" case UnitLiteral() => p"()" diff --git a/src/main/scala/leon/purescala/ScalaPrinter.scala b/src/main/scala/leon/purescala/ScalaPrinter.scala index f1d1911968c7c7c24e608ffeb2845e868efb4836..eeca5d984724bc784d3bdaef0d6ee79238bf0df8 100644 --- a/src/main/scala/leon/purescala/ScalaPrinter.scala +++ b/src/main/scala/leon/purescala/ScalaPrinter.scala @@ -52,6 +52,7 @@ class ScalaPrinter(opts: PrinterOptions, sb: StringBuffer = new StringBuffer) ex case SetDifference(l,r) => p"$l -- $r" case SetIntersection(l,r) => p"$l & $r" case SetCardinality(s) => p"$s.size" + case InfiniteIntegerLiteral(v) => p"BigInt($v)" case a@FiniteArray(elems, oDef, size) => { import ExprOps._