From 1e76e46c2ed0833e776b261520c6f95f2d77a413 Mon Sep 17 00:00:00 2001
From: Marco Antognini <antognini.marco@gmail.com>
Date: Wed, 14 Dec 2016 16:19:29 +0100
Subject: [PATCH] Move some tests around

 - Aliasing3 is disabled because it make verification crash (see #289)
 - Aliasing4 is disabled because it make verification produce incorrect counter-example (see #287)
 - Inheritance9 is disabled because it make xlang crash (see #288)
 - UsingConcreteCLasses is enabled because verification is easy
---
 .../regression/genc/{valid => unverified}/Aliasing3.scala       | 0
 .../regression/genc/{valid => unverified}/Aliasing4.scala       | 0
 .../regression/genc/{valid => unverified}/Inheritance9.scala    | 0
 .../regression/genc/{valid => unverified}/LinearSearch.scala    | 0
 .../genc/{unverified => valid}/UsingConcreteClasses.scala       | 2 +-
 5 files changed, 1 insertion(+), 1 deletion(-)
 rename src/test/resources/regression/genc/{valid => unverified}/Aliasing3.scala (100%)
 rename src/test/resources/regression/genc/{valid => unverified}/Aliasing4.scala (100%)
 rename src/test/resources/regression/genc/{valid => unverified}/Inheritance9.scala (100%)
 rename src/test/resources/regression/genc/{valid => unverified}/LinearSearch.scala (100%)
 rename src/test/resources/regression/genc/{unverified => valid}/UsingConcreteClasses.scala (93%)

diff --git a/src/test/resources/regression/genc/valid/Aliasing3.scala b/src/test/resources/regression/genc/unverified/Aliasing3.scala
similarity index 100%
rename from src/test/resources/regression/genc/valid/Aliasing3.scala
rename to src/test/resources/regression/genc/unverified/Aliasing3.scala
diff --git a/src/test/resources/regression/genc/valid/Aliasing4.scala b/src/test/resources/regression/genc/unverified/Aliasing4.scala
similarity index 100%
rename from src/test/resources/regression/genc/valid/Aliasing4.scala
rename to src/test/resources/regression/genc/unverified/Aliasing4.scala
diff --git a/src/test/resources/regression/genc/valid/Inheritance9.scala b/src/test/resources/regression/genc/unverified/Inheritance9.scala
similarity index 100%
rename from src/test/resources/regression/genc/valid/Inheritance9.scala
rename to src/test/resources/regression/genc/unverified/Inheritance9.scala
diff --git a/src/test/resources/regression/genc/valid/LinearSearch.scala b/src/test/resources/regression/genc/unverified/LinearSearch.scala
similarity index 100%
rename from src/test/resources/regression/genc/valid/LinearSearch.scala
rename to src/test/resources/regression/genc/unverified/LinearSearch.scala
diff --git a/src/test/resources/regression/genc/unverified/UsingConcreteClasses.scala b/src/test/resources/regression/genc/valid/UsingConcreteClasses.scala
similarity index 93%
rename from src/test/resources/regression/genc/unverified/UsingConcreteClasses.scala
rename to src/test/resources/regression/genc/valid/UsingConcreteClasses.scala
index 8725a6e20..434c01d3f 100644
--- a/src/test/resources/regression/genc/unverified/UsingConcreteClasses.scala
+++ b/src/test/resources/regression/genc/valid/UsingConcreteClasses.scala
@@ -13,7 +13,7 @@ object UsingConcreteClasses {
 
     if (child.opt.v == 42) 0
     else 1
-  }
+  } ensuring { _ == 0 }
 
   @extern
   def main(args: Array[String]): Unit = _main()