diff --git a/src/test/resources/regression/verification/purescala/invalid/Nested15.scala b/src/test/resources/regression/verification/purescala/invalid/Nested15.scala index 228afa9fa6a217258aacbb2604817808f2b43abc..61ac54c4e924885c671544d6b5438db5e0183f31 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 a81c77e67042ac24586fdbe2a45818dcad49ea23..5fd3650d62211bfafe18fc2f32c6da3c64f5a158 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 d72e74f2633e3713839622e95582d1f06f399383..b1ee199960b8ec9732f52b5d6b98ba1198e8fd51 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()