(Also posted on the Reddit thread)
I think the example is broken.
To see why, notice that we are dealing with field elements, not integers. Field elements are integers modulo p. In the Ethereum case, p = 21888242871839275222246405745257275088696311157297823662689037894645226208583. We can make a fake proof that a nontrivial x * y = z by supplying any witnesses x and y such that x * y = p * k + z for some integer k; the field math "wraps around". For example, I can show that 5 is "non-prime" via x = 7 and y = 18761351033005093047639776353077664361739695277683848853733461052553051035929, which equals 6 * p + 5 in regular arithmetic, but equals 5 in field arithmetic because of how it wraps around.
To solve this, I think you need to have an inequality check that x and y are both less than sqrt(p) (or, better yet, less than z). So unfortunately the number of constraints will be ~1600 after all.
Author: Vitalik Buterin