1 files changed, 23 insertions, 0 deletions
diff --git a/Test/dafny0/Computations.dfy b/Test/dafny0/Computations.dfy
index 8050aded..83b2a571 100644
--- a/Test/dafny0/Computations.dfy
+++ b/Test/dafny0/Computations.dfy
@@ -184,3 +184,26 @@ ghost method test_fib3(k: nat, m: nat)
   var y := 12;
   assert y <= k && k < y + m && m == 1 ==> fib(k)==144;
 }
+
+module NeedsAllLiteralsAxiom {
+  // The following test shows that there exist an example that
+  // benefits from the all-literals axiom.  (It's not clear how
+  // important such an example is, nor is it clear what the cost
+  // of including the all-literals axiom is.)
+
+  function trick(n: nat, m: nat): nat
+    decreases n;  // note that m is not included
+  {
+    if n < m || m==0 then n else trick(n-m, m) + m
+  }
+
+  lemma lemma_trick(n: nat, m: nat)
+    ensures trick(n, m) == n;
+  {
+  }
+
+  lemma calc_trick(n: nat, m: nat)
+    ensures trick(100, 10) == 100;
+  {
+  }
+}