From dbc4e63008d2e2275f6824040c45e479c017a66a Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Thu, 16 Apr 2015 15:42:47 +0200
Subject: [PATCH] Use PrettyPrinter and not ScalaPrinter for printing c-ex
---
.../scala/leon/verification/VerificationCondition.scala | 6 +++++-
1 file changed, 5 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/verification/VerificationCondition.scala b/src/main/scala/leon/verification/VerificationCondition.scala
index 75618fbba..147417cee 100644
--- a/src/main/scala/leon/verification/VerificationCondition.scala
+++ b/src/main/scala/leon/verification/VerificationCondition.scala
@@ -4,6 +4,7 @@ package leon.verification
import leon.purescala.Expressions._
import leon.purescala.Definitions._
+import leon.purescala.PrettyPrinter
import leon.purescala.Common._
import leon.utils.Positioned
@@ -52,8 +53,11 @@ case class VCResult(status: VCStatus, solvedWith: Option[Solver], timeMs: Option
reporter.error(" => INVALID")
reporter.error("Found counter-example:")
+ // We use PrettyPrinter explicitly and not ScalaPrinter: printing very
+ // large arrays faithfully in ScalaPrinter is hard, while PrettyPrinter
+ // is free to simplify
val strings = cex.toSeq.sortBy(_._1.name).map {
- case (id, v) => (id.asString(context), v.asString(context))
+ case (id, v) => (id.asString(context), PrettyPrinter(v))
}
if (strings.nonEmpty) {
--
GitLab