From 3da86095dc6dbb2169fc8286a2d09926378c6de9 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 18 Mar 2016 17:20:35 +0100
Subject: [PATCH] solutionToProgram should use Choose spec as postcondition
---
src/main/scala/leon/synthesis/Synthesizer.scala | 5 +++++
1 file changed, 5 insertions(+)
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 467ed7376..70b8c88e1 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -174,6 +174,11 @@ class Synthesizer(val context : LeonContext,
case fd if fd eq ci.fd =>
val nfd = fd.duplicate()
nfd.fullBody = replace(Map(ci.source -> solutionExpr), nfd.fullBody)
+ (fd.body, fd.postcondition) match {
+ case (Some(Choose(pred)), None) =>
+ nfd.postcondition = Some(pred)
+ case _ =>
+ }
Some(nfd)
case _ => None
})
--
GitLab