From 73837fd738ff625a803a35819e103b622d32b7f4 Mon Sep 17 00:00:00 2001
From: Viktor Kuncak <vkuncak@gmail.com>
Date: Sun, 13 Feb 2011 01:12:52 +0000
Subject: [PATCH] counterexamples
---
testcases/IntSynth.scala | 14 ++++++++++++++
1 file changed, 14 insertions(+)
create mode 100644 testcases/IntSynth.scala
diff --git a/testcases/IntSynth.scala b/testcases/IntSynth.scala
new file mode 100644
index 000000000..f3a6a8ac6
--- /dev/null
+++ b/testcases/IntSynth.scala
@@ -0,0 +1,14 @@
+import scala.collection.immutable.Set
+import funcheck.Annotations._
+import funcheck.Utils._
+
+object IntSynth {
+ def spec(time : Int, m : Int, s : Int) : Boolean = {
+ require(0 <= time)
+ time == 60 * m + s &&
+ 0 <= m && 0 <= s && s < 60
+ }
+ def f200(m : Int, s : Int) : Boolean = {
+ !spec(200, m, s)
+ } holds
+}
--
GitLab