From 119a0f8c36c36cafaa95e1cf253bbecfea6fbdb0 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Fri, 19 Jun 2015 17:53:34 +0200
Subject: [PATCH] Inject the synthesized function only once, instead of once
per compilation unit.
---
src/main/scala/leon/synthesis/Synthesizer.scala | 9 +++++----
1 file changed, 5 insertions(+), 4 deletions(-)
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 4fa399f7a..de108afa9 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -74,7 +74,7 @@ class Synthesizer(val context : LeonContext,
val solverf = SolverFactory.default(context, npr).withTimeout(timeout)
- try {
+ try {
val vctx = VerificationContext(context, npr, solverf, context.reporter)
val vcs = generateVCs(vctx, Some(fds.map(_.id.name)))
val vcreport = checkVCs(vctx, vcs)
@@ -113,9 +113,10 @@ class Synthesizer(val context : LeonContext,
val newDefs = fd +: sol.defs.toList
- val npr = program.copy(units = program.units map { u =>
- u.copy(modules = ModuleDef(FreshIdentifier("synthesis"), newDefs.toSeq, false) +: u.modules )
- })
+ val newModule = ModuleDef(FreshIdentifier("synthesis"), newDefs.toSeq, false)
+ val newUnit = UnitDef(FreshIdentifier("synthesis"), Seq(newModule), Nil, Seq(), true)
+
+ val npr = program.copy(units = newUnit :: program.units)
(npr, newDefs)
}
--
GitLab