From f173c8986b7055abaf90a144fe0f1ed2ca69fff0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <a-mikmay@microsoft.com>
Date: Tue, 22 Dec 2015 14:35:11 +0100
Subject: [PATCH] Correct bug generating endless loops for false-guarded test
cases.
---
.../scala/leon/synthesis/ExamplesFinder.scala | 6 +++--
testcases/stringrender/DoubleListRender.scala | 24 ++++++++++++++++---
2 files changed, 25 insertions(+), 5 deletions(-)
diff --git a/src/main/scala/leon/synthesis/ExamplesFinder.scala b/src/main/scala/leon/synthesis/ExamplesFinder.scala
index 744029ee3..3cc97f4f5 100644
--- a/src/main/scala/leon/synthesis/ExamplesFinder.scala
+++ b/src/main/scala/leon/synthesis/ExamplesFinder.scala
@@ -199,8 +199,10 @@ class ExamplesFinder(ctx0: LeonContext, program: Program) {
case None =>
true
}
-
- (for {
+
+ if(cs.optGuard == Some(BooleanLiteral(false))) {
+ Nil
+ } else (for {
inst <- instantiations.toSeq
inR = replaceFromIDs(inst, pattExpr)
outR = replaceFromIDs(inst, doSubstitute(ieMap, cs.rhs))
diff --git a/testcases/stringrender/DoubleListRender.scala b/testcases/stringrender/DoubleListRender.scala
index ed28a264b..284760380 100644
--- a/testcases/stringrender/DoubleListRender.scala
+++ b/testcases/stringrender/DoubleListRender.scala
@@ -24,12 +24,30 @@ object DoubleListRender {
a == b || a == c || b == c
} holds
- def AtoString(a : A): String = {
+ def mutual_lists(a : A): String = {
???
} ensuring {
(res : String) => (a, res) passes {
- case B(BB(N(), BB(B(NN(), B(NN(), N())), NN())), N()) =>
- "[([], [(), ()])]"
+ case N() =>
+ "[]"
+ case B(NN(), N()) =>
+ "[()]"
+ case B(NN(), B(NN(), N())) =>
+ "[(), ()]"
+ case B(BB(N(), NN()), N()) =>
+ "[([])]"
+ case B(NN(), B(NN(), B(NN(), N()))) =>
+ "[(), (), ()]"
+ case B(BB(N(), BB(N(), NN())), N()) =>
+ "[([], [])]"
+ case B(NN(), B(BB(N(), NN()), N())) =>
+ "[(), ([])]"
+ case B(BB(N(), NN()), B(NN(), N())) =>
+ "[([]), ()]"
+ case B(BB(B(NN(), N()), NN()), N()) =>
+ "[([()])]"
+ case B(BB(N(), BB(N(), BB(N(), NN()))), N()) =>
+ "[([], [], [])]"
}
}
}
\ No newline at end of file
--
GitLab