From 82c86cdb370296a29aded9a8a147db7755b00e7d Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Mon, 30 Mar 2015 15:58:13 +0200
Subject: [PATCH] Fix synthesis test suite to not rely on ADTInduction
---
src/test/scala/leon/test/synthesis/SynthesisSuite.scala | 8 ++++----
1 file changed, 4 insertions(+), 4 deletions(-)
diff --git a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
index 9abd14c6e..6978a3fa8 100644
--- a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
+++ b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
@@ -299,20 +299,20 @@ object SortedList {
}
""") {
case "concat" =>
- Decomp("ADT Induction on 'in1'", List(
+ Decomp("ADT Split on 'in1'", List(
Close("CEGIS"),
Close("CEGIS")
))
case "insert" =>
- Decomp("ADT Induction on 'in1'", List(
+ Decomp("ADT Split on 'in1'", List(
Close("CEGIS"),
Close("CEGIS")
))
case "insertSorted" =>
Decomp("Assert isSorted(in1)", List(
- Decomp("ADT Induction on 'in1'", List(
+ Decomp("ADT Split on 'in1'", List(
Decomp("Ineq. Split on 'head*' and 'v*'", List(
Close("CEGIS"),
Decomp("Equivalent Inputs *", List(
@@ -356,7 +356,7 @@ object ChurchNumerals {
}
""") {
case "add" =>
- Decomp("ADT Induction on 'y'", List(
+ Decomp("ADT Split on 'y'", List(
Close("CEGIS"),
Close("CEGIS")
))
--
GitLab