From 00b0139d8289fc6c00b1be95a49eb27e3b3cb932 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 9 Oct 2015 14:52:15 +0200
Subject: [PATCH] Change this tests to not trigger CVC4 bug, un-ignore them
---
.../regression/verification/purescala/invalid/Nested15.scala | 2 +-
.../regression/verification/purescala/valid/Nested15.scala | 2 +-
.../regression/verification/PureScalaVerificationSuite.scala | 5 -----
3 files changed, 2 insertions(+), 7 deletions(-)
diff --git a/src/test/resources/regression/verification/purescala/invalid/Nested15.scala b/src/test/resources/regression/verification/purescala/invalid/Nested15.scala
index 228afa9fa..61ac54c4e 100644
--- a/src/test/resources/regression/verification/purescala/invalid/Nested15.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/Nested15.scala
@@ -10,7 +10,7 @@ object Nested15 {
def rec3(k: C) = k :: rec1[C](l)
rec3(l.head).size + j + n.size + i.size
}
- rec2(List(true, true, false), 2)
+ rec2(List(1,2,3), 2)
} ensuring(_ == i.size + 9) // Should be 2* size
}
diff --git a/src/test/resources/regression/verification/purescala/valid/Nested15.scala b/src/test/resources/regression/verification/purescala/valid/Nested15.scala
index a81c77e67..5fd3650d6 100644
--- a/src/test/resources/regression/verification/purescala/valid/Nested15.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Nested15.scala
@@ -10,7 +10,7 @@ object Nested15 {
def rec3(k: C) = k :: rec1[C](l)
rec3(l.head).size + j + n.size + i.size
}
- rec2(List(true, true, false), 2)
+ rec2(List(1, 2, 3), 2)
} ensuring(_ == 2 * i.size + 9)
}
diff --git a/src/test/scala/leon/regression/verification/PureScalaVerificationSuite.scala b/src/test/scala/leon/regression/verification/PureScalaVerificationSuite.scala
index d72e74f26..b1ee19996 100644
--- a/src/test/scala/leon/regression/verification/PureScalaVerificationSuite.scala
+++ b/src/test/scala/leon/regression/verification/PureScalaVerificationSuite.scala
@@ -16,11 +16,6 @@ class PureScalaVerificationSuite extends VerificationSuite {
val pipeFront = xlang.NoXLangFeaturesChecking
val pipeBack = AnalysisPhase
- override val ignored = Seq(
- "verification/purescala/valid/Nested15.scala",
- "verification/purescala/invalid/Nested15.scala"
- )
-
val optionVariants: List[List[String]] = {
val isZ3Available = try {
Z3Interpreter.buildDefault.free()
--
GitLab