From 28424994935965a280f4abb4640bb5c909ed5d5b Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Thu, 11 Dec 2014 17:10:38 +0100
Subject: [PATCH] Fix bug in forward trusting untrusted solutions
---
src/main/scala/leon/synthesis/Rules.scala | 7 +------
1 file changed, 1 insertion(+), 6 deletions(-)
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 330ba38c0..e93aa7089 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -173,12 +173,7 @@ trait RuleHelpers {
def subst(what: Tuple2[Identifier, Expr], in: Expr): Expr = replaceFromIDs(Map(what), in)
def substAll(what: Map[Identifier, Expr], in: Expr): Expr = replaceFromIDs(what, in)
- val forward: List[Solution] => Option[Solution] = {
- case List(s) =>
- Some(Solution(s.pre, s.defs, s.term))
- case _ =>
- None
- }
+ val forward: List[Solution] => Option[Solution] = { ss => ss.headOption }
def project(firstN: Int): List[Solution] => Option[Solution] = {
project(0 until firstN)
--
GitLab