diff --git a/src/test/resources/regression/genc/invalid/BadInheritance2.scala b/src/test/resources/regression/genc/valid/Inheritance7.scala similarity index 67% rename from src/test/resources/regression/genc/invalid/BadInheritance2.scala rename to src/test/resources/regression/genc/valid/Inheritance7.scala index 61bb1f219..c2e8e5f14 100644 --- a/src/test/resources/regression/genc/invalid/BadInheritance2.scala +++ b/src/test/resources/regression/genc/valid/Inheritance7.scala @@ -3,10 +3,10 @@ import leon.annotation.extern import leon.lang._ -object BadInheritance2 { +object Inheritance7 { abstract class Base { - def get: Int // Defining abstract method is not supported + def get: Int // Defining abstract method IS supported } case class Derived1(x: Int) extends Base { @@ -17,8 +17,11 @@ object BadInheritance2 { override def get: Int = 1 } + def test1 = Derived1(42).get // == 0 + def test2 = Derived2(58).get - 1 // == 0 + def _main() = { - 0 + test1 + test2 } ensuring { _ == 0 } @extern diff --git a/src/test/resources/regression/genc/invalid/BadInheritance1.scala b/src/test/resources/regression/genc/valid/Inheritance8.scala similarity index 63% rename from src/test/resources/regression/genc/invalid/BadInheritance1.scala rename to src/test/resources/regression/genc/valid/Inheritance8.scala index 4f59f2729..0337c1a33 100644 --- a/src/test/resources/regression/genc/invalid/BadInheritance1.scala +++ b/src/test/resources/regression/genc/valid/Inheritance8.scala @@ -3,7 +3,7 @@ import leon.annotation.extern import leon.lang._ -object BadInheritance1 { +object Inheritance8 { abstract class Base { def get: Int = 1 @@ -12,11 +12,14 @@ object BadInheritance1 { case class Derived1(x: Int) extends Base case class Derived2(x: Int) extends Base { - override def get: Int = 0 // Overriding a method is not supported + override def get: Int = 0 // Overriding a method IS supported } + def test1 = Derived1(42).get - 1 // == 0 + def test2 = Derived2(58).get // == 0 + def _main() = { - 0 + test1 + test2 } ensuring { _ == 0 } @extern