1 files changed, 47 insertions, 4 deletions
diff --git a/drnim/tests/tensures.nim b/drnim/tests/tensures.nim
index 1283b493b..f4e8f84e6 100644
--- a/drnim/tests/tensures.nim
+++ b/drnim/tests/tensures.nim
@@ -1,12 +1,19 @@
 discard """
-  nimout: '''tensures.nim(11, 10) Warning: BEGIN [User]
-tensures.nim(20, 5) Warning: cannot prove:
+  nimout: '''tensures.nim(18, 10) Warning: BEGIN [User]
+tensures.nim(27, 5) Warning: cannot prove:
 0 < n [IndexCheck]
-tensures.nim(30, 10) Warning: END [User]'''
+tensures.nim(47, 17) Warning: cannot prove: a < 4; counter example: y -> 2
+a`2 -> 4
+a`1 -> 3
+a -> 2 [IndexCheck]
+tensures.nim(69, 17) Warning: cannot prove: a < 4; counter example: y -> 2
+a`1 -> 4
+a -> 2 [IndexCheck]
+tensures.nim(73, 10) Warning: END [User]'''
   cmd: "drnim $file"
   action: "compile"
 """
-
+import std/logic
 {.push staticBoundChecks: defined(nimDrNim).}
 {.warning: "BEGIN".}
 
@@ -27,5 +34,41 @@ proc main =
 
 main()
 
+proc myinc(x: var int) {.ensures: x == old(x)+1.} =
+  inc x
+  {.assume: old(x)+1 == x.}
+
+proc mainB(y: int) =
+  var a = y
+  if a < 3:
+    myinc a
+    {.assert: a < 4.}
+    myinc a
+    {.assert: a < 4.} # now this is wrong!
+
+mainB(3)
+
+proc a(yy, z: int) {.requires: (yy - z) > 6.} = discard
+# 'requires' must be weaker (or equal)
+# 'ensures'  must be stronger (or equal)
+
+# a 'is weaker than' b iff  b -> a
+# a 'is stronger than' b iff a -> b
+# --> We can use Z3 to compute whether 'var x: T = q' is valid
+
+type
+  F = proc (yy, z3: int) {.requires: z3 < 5 and z3 > -5 and yy > 10.}
+
+var
+  x: F = a # valid?
+
+proc testAsgn(y: int) =
+  var a = y
+  if a < 3:
+    a = a + 2
+    {.assert: a < 4.}
+
+testAsgn(3)
+
 {.warning: "END".}
 {.pop.}