From a170be6fcb35ab23995f8b24ba235c02fc9335c1 Mon Sep 17 00:00:00 2001
From: Viktor Kuncak <viktor.kuncak@epfl.ch>
Date: Tue, 28 Apr 2015 22:33:56 -0700
Subject: [PATCH] Minor cleanup what is commented and what not.
---
testcases/web/demos/001_Tutorial-Max.scala | 13 ++++++-------
1 file changed, 6 insertions(+), 7 deletions(-)
diff --git a/testcases/web/demos/001_Tutorial-Max.scala b/testcases/web/demos/001_Tutorial-Max.scala
index c013d1b9f..75ac1a0b6 100644
--- a/testcases/web/demos/001_Tutorial-Max.scala
+++ b/testcases/web/demos/001_Tutorial-Max.scala
@@ -2,18 +2,17 @@ import leon.lang._
import leon.lang.synthesis._
import leon.annotation._
object Max {
-/*
def max(x: Int, y: Int): Int = {
val d = x - y
if (d > 0) x
else y
- } ensuring(res =>
- x <= res && y <= res && (res == x || res == y))
-*/
+ }
+ // ensuring(res => (res == x || res == y))
+ // x <= res && y <= res
- //def test1 = max(10, 5)
- //def test2 = max(-5, 5)
- //def test3 = max(-5, -7)
+ def test1 = max(10, 5)
+ def test2 = max(-5, 5)
+ def test3 = max(-5, -7)
//def test4 = max(-1639624704, 1879048192)
--
GitLab