diff --git a/testcases/xlang/MaxSum.scala b/testcases/xlang/MaxSum.scala
index 3d414f39716f6342eb17e526de03201e39913910..f4d056ab9106d939fadc658c2c21bebb70662c3b 100644
--- a/testcases/xlang/MaxSum.scala
+++ b/testcases/xlang/MaxSum.scala
@@ -35,4 +35,27 @@ object MaxSum {
     rec(0)
   }
 
+  def summ(to : Int): Int = ({
+    require(to >= 0)
+    var i = 0
+    var s = 0
+    (while (i < to) {
+      s = s + i
+      i = i + 1
+    }) invariant (s >= 0 && i >= 0 && s == i*(i-1)/2 && i <= to)
+    s
+  }) ensuring(res => res >= 0 && res == to*(to-1)/2)
+
+
+  def sumsq(to : Int): Int = ({
+    require(to >= 0)
+    var i = 0
+    var s = 0
+    (while (i < to) {
+      s = s + i*i
+      i = i + 1
+    }) invariant (s >= 0 && i >= 0 && s == (i-1)*i*(2*i-1)/6 && i <= to)
+    s
+  }) ensuring(res => res >= 0 && res == (to-1)*to*(2*to-1)/6)
+
 }