diff --git a/doc/cprover-manual/cbmc-tutorial.md b/doc/cprover-manual/cbmc-tutorial.md
index 7da86c649aa..e2a6cd5a970 100644
--- a/doc/cprover-manual/cbmc-tutorial.md
+++ b/doc/cprover-manual/cbmc-tutorial.md
@@ -145,6 +145,8 @@ int sum() {
   sum=0;
   for(i=0; i<10; i++)
     sum+=array[i];
+
+  return sum;
 }
 ```
 
@@ -216,6 +218,7 @@ is an example of a program with a user-specified property:
 
 ```C
 _Bool nondet_bool();
+unsigned int nondet_unsigned_int();
 _Bool LOCK = 0;
 
 _Bool lock()
@@ -239,7 +242,7 @@ void unlock()
 int main()
 {
   unsigned got_lock = 0;
-  int times;
+  unsigned times = nondet_unsigned_int();
 
   while(times > 0)
   {