From 93ccaa93ed7819217c8dfa4eff6be95a7ba4f462 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Thu, 17 Mar 2016 18:21:41 +0100
Subject: [PATCH] Improve some messages
---
src/main/scala/leon/synthesis/Solution.scala | 2 +-
src/main/scala/leon/synthesis/SourceInfo.scala | 2 +-
src/main/scala/leon/synthesis/Synthesizer.scala | 2 ++
3 files changed, 4 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/synthesis/Solution.scala b/src/main/scala/leon/synthesis/Solution.scala
index fd7d3fb6a..bddbcae12 100644
--- a/src/main/scala/leon/synthesis/Solution.scala
+++ b/src/main/scala/leon/synthesis/Solution.scala
@@ -96,6 +96,6 @@ object Solution {
def UNSAT(implicit p: Problem): Solution = {
val tpe = tupleTypeWrap(p.xs.map(_.getType))
- Solution(BooleanLiteral(false), Set(), Error(tpe, "Path condition is UNSAT!"))
+ Solution(BooleanLiteral(false), Set(), Error(tpe, "Spec is UNSAT for this path!"))
}
}
diff --git a/src/main/scala/leon/synthesis/SourceInfo.scala b/src/main/scala/leon/synthesis/SourceInfo.scala
index 666c589c3..cf6063da0 100644
--- a/src/main/scala/leon/synthesis/SourceInfo.scala
+++ b/src/main/scala/leon/synthesis/SourceInfo.scala
@@ -39,7 +39,7 @@ object SourceInfo {
}
if (results.isEmpty) {
- ctx.reporter.warning("No 'choose' found. Maybe the functions you chose do not exist?")
+ ctx.reporter.warning("No 'choose' found. Maybe the functions you indicated do not exist?")
}
results.sortBy(_.source.getPos)
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 23d79c1e7..50f2da1af 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -55,6 +55,8 @@ class Synthesizer(val context : LeonContext,
val s = getSearch
+ reporter.info(ASCIIHelpers.title(s"Synthesizing '${ci.fd.id}'"))
+
val t = context.timers.synthesis.search.start()
val sols = s.search(sctx)
--
GitLab