Merge fixes and example extensions from master.

examples/sudokuchecker.code

@@ -59,7 +59,7 @@ counter = 0 // globally counts duplicate entries in boxes, rows and columns
 
   counter = counter + checkEquality(a11,a12,b11,b12)
   counter = counter + checkEquality(a21,a22,b21,b22)
-  counter = counter + checkEquality(c11,c21,d11,d12)
+  counter = counter + checkEquality(c11,c12,d11,d12)
   counter = counter + checkEquality(c21,c22,d21,d22)
 
 // check column correctness

examples/waldo.code

@@ -0,0 +1,25 @@
+// Where's Waldo is a puzzle where the goal is to find Waldo in the picture of a crowd
+// In this example, the crowd is a series of numbers, ideally* all prime but one, and Waldo is a non-prime number
+// * we don't enforce only one number being non-prime, so there could be multiple Waldos
+
+def isWaldo(a):
+  // make sure that p and q are both non zero
+  // we can't check inequalities, so let's create binary
+  // variables
+  p1 = if p == 1 then 0 else 1 fi // "p != 1"
+  q1 = if q == 1 then 0 else 1 fi // "q != 1"
+  q1 * p1 == 1 // "p1 and q1"
+
+  // we know how to factor a
+  a == p * q
+
+  return 1
+
+// define all
+def main(a0, a1, a2, a3):
+  // prover provides the index of Waldo
+  waldo = if index == 0 then a0 else 0 fi 
+  waldo = waldo + if index == 1 then a1 else 0 fi 
+  waldo = waldo + if index == 2 then a2 else 0 fi 
+  waldo = waldo + if index == 3 then a3 else 0 fi
+  return isWaldo(waldo)