diff --git a/testcases/smalltest/BallBeam.scala b/testcases/fm2019/BallBeam.scala
similarity index 100%
rename from testcases/smalltest/BallBeam.scala
rename to testcases/fm2019/BallBeam.scala
diff --git a/testcases/testsmt/BatchProcessor.scala b/testcases/fm2019/BatchProcessor.scala
similarity index 100%
rename from testcases/testsmt/BatchProcessor.scala
rename to testcases/fm2019/BatchProcessor.scala
diff --git a/testcases/testsmt/BatchReactor.scala b/testcases/fm2019/BatchReactor.scala
similarity index 100%
rename from testcases/testsmt/BatchReactor.scala
rename to testcases/fm2019/BatchReactor.scala
diff --git a/testcases/smalltest/Bicycle.scala b/testcases/fm2019/Bicycle.scala
similarity index 100%
rename from testcases/smalltest/Bicycle.scala
rename to testcases/fm2019/Bicycle.scala
diff --git a/testcases/smalltest/Bsplines.scala b/testcases/fm2019/Bsplines.scala
similarity index 100%
rename from testcases/smalltest/Bsplines.scala
rename to testcases/fm2019/Bsplines.scala
diff --git a/testcases/testsmt/DCMotor.scala b/testcases/fm2019/DCMotor.scala
similarity index 100%
rename from testcases/testsmt/DCMotor.scala
rename to testcases/fm2019/DCMotor.scala
diff --git a/testcases/testsmt/Doppler.scala b/testcases/fm2019/Doppler.scala
similarity index 100%
rename from testcases/testsmt/Doppler.scala
rename to testcases/fm2019/Doppler.scala
diff --git a/testcases/testsmt/DopplerFMA.scala b/testcases/fm2019/DopplerFMA.scala
similarity index 87%
rename from testcases/testsmt/DopplerFMA.scala
rename to testcases/fm2019/DopplerFMA.scala
index 2f37288f73e8a91e9351ccc2832871437c93c30d..5f3c58878f0fa6fa44ef25350a2c8700fe390fb3 100644
--- a/testcases/testsmt/DopplerFMA.scala
+++ b/testcases/fm2019/DopplerFMA.scala
@@ -7,7 +7,7 @@ import Real._
 object DopplerFMA {
 
   def doppler(u: Real, v: Real, T: Real): Real = {
-    require(-100.0 <= u && u <= 100 && 20 <= v && v <= 20000 && -30 <= T && T <= 50)
+    require(-100.0 <= u && u <= 100 && 20 <= v && v <= 20000 && -30 <= T && T <= 50 && u + T <= 100)
 
     val t1 = fma(0.6, T, 331.4)
     (- (t1) *v) / ((t1 + u)*(t1 + u))
diff --git a/testcases/smalltest/Floudas.scala b/testcases/fm2019/Floudas.scala
similarity index 100%
rename from testcases/smalltest/Floudas.scala
rename to testcases/fm2019/Floudas.scala
diff --git a/testcases/testsmt/Himmilbeau.scala b/testcases/fm2019/Himmilbeau.scala
similarity index 100%
rename from testcases/testsmt/Himmilbeau.scala
rename to testcases/fm2019/Himmilbeau.scala
diff --git a/testcases/smalltest/InvertedPendulum.scala b/testcases/fm2019/InvertedPendulum.scala
similarity index 100%
rename from testcases/smalltest/InvertedPendulum.scala
rename to testcases/fm2019/InvertedPendulum.scala
diff --git a/testcases/fm2019/JetEngine.scala b/testcases/fm2019/JetEngine.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f80fe68203c2e994512ed3401301a601d3c9b16e
--- /dev/null
+++ b/testcases/fm2019/JetEngine.scala
@@ -0,0 +1,22 @@
+
+
+import daisy.lang._
+import Real._
+
+
+object JetEngine {
+
+
+  def jetEngine(x1: Real, x2: Real): Real = {
+    require(-5 <= x1 && x1 <= 5 && -20 <= x2 && x2 <= 5)
+
+    val t = (3*x1*x1 + 2*x2 - x1)
+
+    x1 + ((2*x1*(t/(x1*x1 + 1))*
+    (t/(x1*x1 + 1) - 3) + x1*x1*(4*(t/(x1*x1 + 1))-6))*
+    (x1*x1 + 1) + 3*x1*x1*(t/(x1*x1 + 1)) + x1*x1*x1 + x1 +
+    3*((3*x1*x1 + 2*x2 -x1)/(x1*x1 + 1)))
+  }
+
+
+}
\ No newline at end of file
diff --git a/testcases/smalltest/Kepler.scala b/testcases/fm2019/Kepler.scala
similarity index 100%
rename from testcases/smalltest/Kepler.scala
rename to testcases/fm2019/Kepler.scala
diff --git a/testcases/testsmt/RigidBody.scala b/testcases/fm2019/RigidBody.scala
similarity index 100%
rename from testcases/testsmt/RigidBody.scala
rename to testcases/fm2019/RigidBody.scala
diff --git a/testcases/smalltest/Science.scala b/testcases/fm2019/Science.scala
similarity index 100%
rename from testcases/smalltest/Science.scala
rename to testcases/fm2019/Science.scala
diff --git a/testcases/smalltest/Traincar1.scala b/testcases/fm2019/Traincar1.scala
similarity index 100%
rename from testcases/smalltest/Traincar1.scala
rename to testcases/fm2019/Traincar1.scala
diff --git a/testcases/testsmt/Traincar2.scala b/testcases/fm2019/Traincar2.scala
similarity index 100%
rename from testcases/testsmt/Traincar2.scala
rename to testcases/fm2019/Traincar2.scala
diff --git a/testcases/testsmt/Traincar3.scala b/testcases/fm2019/Traincar3.scala
similarity index 100%
rename from testcases/testsmt/Traincar3.scala
rename to testcases/fm2019/Traincar3.scala
diff --git a/testcases/testsmt/Traincar4.scala b/testcases/fm2019/Traincar4.scala
similarity index 100%
rename from testcases/testsmt/Traincar4.scala
rename to testcases/fm2019/Traincar4.scala
diff --git a/testcases/testsmt/Turbine.scala b/testcases/fm2019/Turbine.scala
similarity index 100%
rename from testcases/testsmt/Turbine.scala
rename to testcases/fm2019/Turbine.scala
diff --git a/testcases/testsmt/BallBeam.scala b/testcases/testsmt/BallBeam.scala
deleted file mode 100644
index c15817f702cf8c6e7ca242b79ae2c8604364d00f..0000000000000000000000000000000000000000
--- a/testcases/testsmt/BallBeam.scala
+++ /dev/null
@@ -1,15 +0,0 @@
-import daisy.lang._
-import Real._
-
-
-object BallBeam {
-
-  // s1 <1, 16, 14>, s2, s3, s4: <1, 16, 15>
-  def ballbeam(s1: Real, s2: Real, s3: Real, s4: Real) = {
-    require(0 <= s1 && s1 <= 1 && -0.5 <= s2 && s2 <= 0.5 && 0 <= s3 && s3 <= 0.5 && 0 <= s4 && s4 <= 0.5)
-    (-1828.6) * s1 + (-1028.6) * s2 + (-2008.0) * s3 + (-104.0) * s4
-  }
-
-
-
-}
diff --git a/testcases/testsmt/Bicycle.scala b/testcases/testsmt/Bicycle.scala
deleted file mode 100644
index d06361e7afb7873bad14af4e3bb52808e9a4867f..0000000000000000000000000000000000000000
--- a/testcases/testsmt/Bicycle.scala
+++ /dev/null
@@ -1,24 +0,0 @@
-import daisy.lang._
-import Real._
-
-
-object Bicycle {
-
-  // s1, s2, s3, y1: <1, 16, 14>, [-1, 1]
-  def out1(s1: Real, s2: Real) = {
-    require(-1 <= s1 && s1 <= 1 && -1 <= s2 && s2 <= 1)
-    (-3.025300) * s1 + (-12.608900) * s2
-  }
-
-  def state1(s1: Real, s2: Real, y1: Real) = {
-    require(-1 <= s1 && s1 <= 1 && -1 <= s2 && s2 <= 1 && -1 <= y1 && y1 <= 1)
-    (0.961270) * s1 + (-0.095962) * s2 + (0.013200) * y1
-  }
-
-  def state2(s1: Real, s2: Real, y1: Real) = {
-    require(-1 <= s1 && s1 <= 1 && -1 <= s2 && s2 <= 1 && -1 <= y1 && y1 <= 1)
-    (-0.058217) * s1 + (0.727430) * s2 + (0.102100) * y1
-  }
-
-
-}
\ No newline at end of file
diff --git a/testcases/testsmt/Bsplines.scala b/testcases/testsmt/Bsplines.scala
deleted file mode 100644
index f988d087b16a4433154d7abb9d293ba58a3311d2..0000000000000000000000000000000000000000
--- a/testcases/testsmt/Bsplines.scala
+++ /dev/null
@@ -1,36 +0,0 @@
-
-import daisy.lang._
-import Real._
-
-/**
-  Equation and initial ranges from:
-  L. Zhang, Y. Zhang, and W. Zhou. Tradeoff between Approximation Accuracy and
-  Complexity for Range Analysis using Affine Arithmetic.
-*/
-object Bsplines {
-
-  def bspline0(u: Real): Real = {
-    require(0 <= u && u <= 1)
-    (1 - u) * (1 - u) * (1 - u) / 6.0
-  } ensuring (res => 0 <= res && res <= 0.17 && res +/- 1e-15)
-  // proven in paper: [-0.05, 0.17]
-
-  def bspline1(u: Real): Real = {
-    require(0 <= u && u <= 1)
-    (3 * u*u*u - 6 * u*u + 4) / 6.0
-  } ensuring (res => 0.16 <= res && res <= 0.7 && res +/- 1e-15)
-  // in paper [-0.05, 0.98]
-
-  def bspline2(u: Real): Real = {
-    require(0 <= u && u <= 1)
-    (-3 * u*u*u  + 3*u*u + 3*u + 1) / 6.0
-  } ensuring (res => 0.16 <= res && res <= 0.7 && res +/- 1e-15)
-  // in paper [-0.02, 0.89]
-
-  def bspline3(u: Real): Real = {
-    require(0 <= u && u <= 1)
-    -u*u*u / 6.0
-  } ensuring (res => -0.17 <= res && res <= 0.0 && res +/- 1e-15)
-  // in paper [-0.17, 0.05]
-
-}
diff --git a/testcases/testsmt/Floudas.scala b/testcases/testsmt/Floudas.scala
deleted file mode 100644
index ef2893660b81276999b4c709624817b702a10364..0000000000000000000000000000000000000000
--- a/testcases/testsmt/Floudas.scala
+++ /dev/null
@@ -1,88 +0,0 @@
-
-
-import daisy.lang._
-import Real._
-
-/*
-  Real2Float
-
-  Optimization problems
-  A Collection of Test Problems for
-  Constrained Global Optimization Algorithms,
-  Floudas, Pardalos 1990
-
-*/
-object Floudas {
-
-
-
-  def floudas26(x1: Real, x2: Real, x3: Real, x4: Real, x5: Real, x6: Real,
-    x7: Real, x8: Real, x9: Real, x10: Real): Real = {
-    require(0 <= x1 && x1 <= 1 && 0 <= x2 && x2 <= 1 && 0 <= x3 && x3 <= 1 && 0 <= x4 && x4 <= 1 &&
-      0 <= x5 && x5 <= 1 && 0 <= x6 && x6 <= 1 && 0 <= x7 && x7 <= 1 && 0 <= x8 && x8 <= 1 &&
-      0 <= x9 && x9 <= 1 && 0 <= x10 && x10 <= 1 &&
-      2 * x1 +6*x2 +1*x3 +0*x4 +3*x5 + 3*x6 +2*x7 +6*x8 +2*x9+2*x10 - 4  >= 0 &&
-      22-(6*x1 -5*x2 +8*x3 -3*x4 +0*x5+1*x6 +3*x7 +8*x8 +9*x9-3*x10)>= 0 &&
-      -(5*x1 +6*x2 +5*x3 +3*x4 +8*x5 -8*x6 +9*x7 +2*x8 +0*x9-9*x10) - 6 >= 0 &&
-      -(9*x1 +5*x2 +0*x3 -9*x4 +1*x5 -8*x6 +3*x7 -9*x8 -9*x9-3*x10) - 23 >= 0 &&
-      -(-(8*x1) +7*x2 -4*x3 -5*x4 -9*x5 +1*x6 -7*x7 -1*x8 +3*x9-2*x10) - 12 >= 0)
-
-    48*x1 + 42*x2 + 48*x3 + 45*x4 + 44*x5 + 41*x6 + 47*x7 + 42*x8 + 45*x9 + 46*x10 -
-      50*(x1*x1 + x2*x2 + x3*x3 + x4*x4 + x5*x5 + x6*x6 + x7*x7 + x8*x8 + x9*x9 + x10*x10)
-
-  }// 5.15e-13
-
-  def floudas33(x1: Real, x2: Real, x3: Real, x4: Real, x5: Real, x6: Real): Real = {
-    require(0 <= x1 && x1 <= 6 && 0 <= x2 && x2 <= 6 && 1 <= x3 && x3 <= 5 &&
-      0 <= x4 && x4 <= 6 && 1 <= x5 && x5 <= 5 && 0 <= x6 && x6 <= 10 &&
-      (x3 -3)*(x3 -3) + x4 - 4 >= 0 &&
-      (x5 -3)*(x5 -3) + x6 - 4 >= 0 &&
-      2 - x1 + 3 * x2 >= 0 &&
-      2 + x1 - x2 >= 0 &&
-      6 - x1 - x2 >= 0 &&
-      x1 + x2 - 2 >= 0)
-
-    - (25 * (x1 -2)*(x1 -2)) - (x2 -2)* (x2 -2) - (x3 -1)*(x3 -1) -
-      (x4 -4)*(x4 -4) - (x5 - 1)*(x5 - 1) - (x6 - 4)* (x6 - 4)
-  } //5.81e–13
-
-  def floudas34(x1: Real, x2: Real, x3: Real): Real = {
-    require(0 <= x1 && x1 <= 2 && 0 <= x2 && x2 <= 2 && 0 <= x3 && x3 <= 3 &&
-      4 - x1 - x2 - x3 >= 0 &&
-      6 - 3 * x2 - x3 >= 0 &&
-      2*x1 - 0.75 - 2*x3 + 4*x1*x1 - 4*x1*x2 + 4*x1*x3 + 2*x2*x2 - 2*x2*x3 + 2*x3*x3 >= 0)
-
-    -2 * x1 + x2 - x3
-
-  } //2.67e - 15
-
-  def floudas46(x1: Real, x2: Real): Real = {
-    require(0 <= x1 && x1 <= 3 && 0 <= x2 && x2 <= 4 &&
-      2 * x1*x1*x1*x1 - 8 * x1*x1*x1 + 8 * x1* x1 - x2 >= 0 &&
-      4 * x1*x1*x1*x1 - 32 * x1*x1*x1 + 88 * x1*x1 - 96*x1 + 36 - x2 >= 0)
-
-    -x1 - x2
-  } //1.38e–15
-
-  def floudas47(x1: Real, x2: Real): Real = {
-    require(0 <= x1 && x1 <= 2 && 0 <= x2 && x2 <= 3 &&
-      -2 * x1*x1*x1*x1 + 2 - x2 >= 0)
-
-    -12*x1 -7*x2 +x2 *x2
-
-  } //1.01e–14
-
-
-  // from FPTaylor github
-  def floudas1(x1: Real, x2: Real, x3: Real, x4: Real, x5: Real, x6: Real): Real = {
-    require(0 <= x1 && x1 <= 6 && 0 <= x2 && x2 <= 6 && 1 <= x3 && x3 <= 5 &&
-      0 <= x4 && x4 <= 6 && 1 <= x5 && x5 <= 5 && 0 <= x6 && x6 <= 10 &&
-      (x3 - 3) * (x3 - 3) + x4 - 4 >= 0 && (x5 - 3) * (x5 - 3) + x6 - 4 >= 0 &&
-      2 - x1 + 3 * x2 >= 0 &&  2 + x1 - x2 >= 0 &&  6 - x1 - x2 >= 0 && x1 + x2 - 2 >= 0)
-
-    -25 * ((x1 - 2) * (x1 - 2)) - ((x2 - 2) * (x2 - 2)) - ((x3 - 1) * (x3 - 1)) -
-      ((x4 - 4) * (x4 - 4)) - ((x5 - 1) * (x5 - 1)) - ((x6 - 4) * (x6 - 4))
-  }
-
-}
-
diff --git a/testcases/testsmt/InvertedPendulum.scala b/testcases/testsmt/InvertedPendulum.scala
deleted file mode 100644
index f66b9117e2bf69e987c44144a3cca42eae2fc47a..0000000000000000000000000000000000000000
--- a/testcases/testsmt/InvertedPendulum.scala
+++ /dev/null
@@ -1,16 +0,0 @@
-import daisy.lang._
-import Real._
-
-
-object InvertedPendulum {
-
-  // s1: <1, 16, 9>  s2: <1, 16, 11>   s3,s4: <1, 16, 15>
-  def out(s1: Real, s2: Real, s3: Real, s4: Real) = {
-    require(-50 <= s1 && s1 <= 50 && -10 <= s2 && s2 <= 10 && -0.785 <= s3 && s3 <= 0.785 && -0.785 <= s4 && s4 <= 0.785)
-
-    1.0000 * s1 + 1.6567 * s2 + (-18.6854) * s3 + (-3.4594) * s4
-  }
-
-
-
-}
diff --git a/testcases/testsmt/Kepler.scala b/testcases/testsmt/Kepler.scala
deleted file mode 100644
index 809983986c7d04d5fb992515bf848c66001792bd..0000000000000000000000000000000000000000
--- a/testcases/testsmt/Kepler.scala
+++ /dev/null
@@ -1,47 +0,0 @@
-
-import daisy.lang._
-import Real._
-
-/*
-  These benchmarks were used by the Real2Float tool,
-  and come from the proof of the Kepler conjecture
-  Introduction to the flyspec project, T.C. Hales, Dagstuhl 2006
-*/
-object Kepler {
-
-  //15 operations
-  def kepler0(x1: Real, x2: Real, x3: Real, x4: Real, x5: Real, x6: Real): Real = {
-    require(4 <= x1 && x1 <= 6.36 && 4 <= x2 && x2 <= 6.36 && 4 <= x3 && x3 <= 6.36 &&
-      4 <= x4 && x4 <= 6.36 && 4 <= x5 && x5 <= 6.36 && 4 <= x6 && x6 <= 6.36)
-
-    val t = ((-1 * x1) + x2 + x3 - x4 + x5 + x6)
-    x2 * x5 + x3 * x6 - x2 * x3 - x5 * x6 + x1 * t
-
-  } // 1.15e-15
-
-  //24 operations
-  def kepler1(x1: Real, x2: Real, x3: Real, x4: Real): Real = {
-    require(4 <= x1 && x1 <= 6.36 && 4 <= x2 && x2 <= 6.36 && 4 <= x3 && x3 <= 6.36 &&
-      4 <= x4 && x4 <= 6.36)
-
-    val t = ((-1 * x1) + x2 + x3 - x4)
-
-    x1 * x4 * t + x2 * (x1 - x2 + x3 + x4) + x3 * (x1 + x2 - x3 + x4) -
-      x2 * x3 * x4 - x1 * x3 - x1 * x2 - x4
-
-  } // 4.50e–13
-
-  //36 operations
-  def kepler2(x1: Real, x2: Real, x3: Real, x4: Real, x5: Real, x6: Real): Real = {
-    require(4 <= x1 && x1 <= 6.36 && 4 <= x2 && x2 <= 6.36 && 4 <= x3 && x3 <= 6.36 &&
-      4 <= x4 && x4 <= 6.36 && 4 <= x5 && x5 <= 6.36 && 4 <= x6 && x6 <= 6.36)
-
-      val t = ((-1 * x1) + x2 + x3 - x4 + x5 + x6)
-      val t2 = (x1 - x2 + x3 + x4 - x5 + x6)
-
-      x1 * x4 * t + x2 * x5 * t2 +
-        x3* x6 * (x1 + x2 - x3 + x4 + x5 - x6) - x2 * x3 * x4 -
-          x1* x3* x5 - x1 * x2 * x6 - x4 * x5 * x6
-
-  } //2.08e–12
-}
diff --git a/testcases/testsmt/Science.scala b/testcases/testsmt/Science.scala
deleted file mode 100644
index 32f4b0e7ad65fd1e04d3f6d6da70d49030d695ff..0000000000000000000000000000000000000000
--- a/testcases/testsmt/Science.scala
+++ /dev/null
@@ -1,33 +0,0 @@
-
-
-import daisy.lang._
-import Real._
-
-
-
-object Science {
-
-  def verhulst(r: Real, K: Real, x: Real): Real = {
-    require(r >= 4.0 && r <= 4.0 && K >= 1.11 && K <= 1.11 && 0.1 <= x && x <= 0.3)
-
-    (r*x) / (1 + (x/K))
-
-  }
-
-  def predatorPrey(r: Real, K: Real, x: Real): Real = {
-    require(r >= 4.0 && r <= 4.0 && K >= 1.11 && K <= 1.11 && 0.1 <= x && x <= 0.3)
-
-    (r*x*x) / (1 + (x/K)*(x/K))
-
-  }
-
-  def carbonGas(T: Real, a: Real, b: Real, N: Real, p: Real, V: Real): Real = {
-    require(T >= 300 && T <= 300 && a >= 0.401 && a <= 0.401 && b >= 42.7e-6 && b <= 42.7e-6 && N >= 1000 && N <= 1000 &&
-    p >= 3.5e7 && p <= 3.5e7 && 0.1 < V && V < 0.5)
-
-    val k: Real = 1.3806503e-23
-    (p + a * (N / V) * (N / V)) * (V - N * b) - k * N * T
-
-  }
-
-}
\ No newline at end of file
diff --git a/testcases/testsmt/Traincar1.scala b/testcases/testsmt/Traincar1.scala
deleted file mode 100644
index a7c8817e408804c039b32b6477aed6d69b12d2fc..0000000000000000000000000000000000000000
--- a/testcases/testsmt/Traincar1.scala
+++ /dev/null
@@ -1,35 +0,0 @@
-
-import daisy.lang._
-import Real._
-
-object Traincar1 {
-
-  // y1, y2: <1, 30, 16>    s1, s2, s3: <1, 30, 25>
-  def out1(s0: Real, s1: Real, s2: Real) = {
-    require(0 <= s0 && s0 <= 4.6 && 0 <= s1 && s1 <= 10 && 0 <= s2 && s2 <= 10)
-    (-3.795323e2) * s0 + (-5.443608e2) * s1 + 92.729 * s2 + 4.5165916241610748e3
-  }
-
-  def state1(s0: Real, s1: Real, s2: Real, y0: Real, y1: Real) = {
-    require(0 <= s0 && s0 <= 4.6 && 0 <= s1 && s1 <= 10 && 0 <= s2 && s2 <= 10 &&
-      0 <= y0 && y0 <= 10 && 0 <= y1 && y1 <= 10)
-    (9.9992292212695999e-01)*s0+ (6.7987387059578006e-02)*s1+ (-5.7849982690687002e-02)*s2 +
-      (-6.7093068270769995e-02)*y0 + (5.6868444245656999e-02)*y1+ (1.93109421e-07)*4.5165916241610748e+03
-  }
-
-  def state2(s0: Real, s1: Real, s2: Real, y0: Real, y1: Real) = {
-    require(0 <= s0 && s0 <= 4.6 && 0 <= s1 && s1 <= 10 && 0 <= s2 && s2 <= 10 &&
-      0 <= y0 && y0 <= 10 && 0 <= y1 && y1 <= 10)
-    (-2.1755689728790001e-03)*s0+ (9.8343791204296505e-01)*s1+ (2.6908497812900001e-03)*s2 +
-      (1.3497550507479000e-02)*y0 + (-2.1628302791680000e-03)*y1+ (5.615999103e-06)*4.5165916241610748e+03
-  }
-
-  def state3(s0: Real, s1: Real, s2: Real, y0: Real, y1: Real) = {
-    require(0 <= s0 && s0 <= 4.6 && 0 <= s1 && s1 <= 10 && 0 <= s2 && s2 <= 10 &&
-      0 <= y0 && y0 <= 10 && 0 <= y1 && y1 <= 10)
-    (7.5141305955000001e-05)*s0+ (2.4840831806619999e-03)*s1+ (9.9188004018882503e-01)*s2 + (-2.4770170720600001e-03)*y0 +
-     (8.1097048460159991e-03)*y1+ (7.060315e-09)*4.5165916241610748e+03
-  }
-
-
-}
\ No newline at end of file