diff --git a/testcases/IntSynth.scala b/testcases/IntSynth.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f3a6a8ac6d3a615b44a94746fa9fe23d5ec006b3
--- /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
+}