From daf7431bed97a2c924517a1777d0e0e1f4ee739a Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Mon, 11 Feb 2013 13:46:57 +0100
Subject: [PATCH] Include the precondition of the outer function in the path to
chooses
---
src/main/scala/leon/synthesis/ChooseInfo.scala | 4 +++-
1 file changed, 3 insertions(+), 1 deletion(-)
diff --git a/src/main/scala/leon/synthesis/ChooseInfo.scala b/src/main/scala/leon/synthesis/ChooseInfo.scala
index adfec0f17..3ea6081ab 100644
--- a/src/main/scala/leon/synthesis/ChooseInfo.scala
+++ b/src/main/scala/leon/synthesis/ChooseInfo.scala
@@ -24,7 +24,9 @@ object ChooseInfo {
// Look for choose()
for (f <- prog.definedFunctions.sortBy(_.id.toString) if f.body.isDefined) {
- for ((ch, path) <- new ChooseCollectorWithPaths().traverse(f.body.get)) {
+ val actualBody = And(f.precondition.getOrElse(BooleanLiteral(true)), f.body.get)
+
+ for ((ch, path) <- new ChooseCollectorWithPaths().traverse(actualBody)) {
results = ChooseInfo(ctx, prog, f, path, ch, options) :: results
}
}
--
GitLab