--- /dev/null
+niter = range(500)
+nvar = range(7)
+
+for a in niter:
+ for b in nvar:
+ print '(define a_{}_{}::int)'.format(a, b)
+
+for a in nvar:
+ print '(assert (= a_0_{} {}))'.format(a, a+1)
+
+for a in niter[1:]:
+ for b in nvar[1:-1]:
+ print '(assert (= a_{0}_{1} (+ a_{2}_{3} a_{2}_{4})))'.format(
+ a, b, a-1, b-1, b+1)
+
+for a in niter[1:]:
+ print '(assert (= a_{}_0 a_{}_0))'.format(a-1, a)
+ print '(assert (= a_{}_6 a_{}_6))'.format(a-1, a)
+
+
+print '(assert (or',
+for a in niter:
+ for b1 in nvar:
+ for b2 in nvar:
+ if b1 != b2:
+ print '(and (>= a_{0}_{1} 50) (= a_{0}_{2} a_{0}_{1}))'.format(
+ a, b1, b2),
+print '))'
+
+print '(check)'
+print '(show-model)'