A Sentient program in response to https://twitter.com/jamestanton/status/874962919963885568

search.snt

# A Sentient program in response to this tweet:
# https://twitter.com/jamestanton/status/874962919963885568
#
# Run it with:
# for i in {1..100}; do ruby search.rb $i > search.snt && sentient -c -o -r -n 0 -m lingeling search.snt; done

n = Integer(ARGV.first)

program = <<-SNT
array#{n}<int5> numbers;

invariant numbers.all?(function (n) {
  return n.between?(0, 9);
});

s = numbers.sum;

t = #{n.times.map { |i| "numbers[#{i}] * #{10 ** (n - i - 1)}" }.join(" + ") };

invariant #{(["s"] * n).join(" * ")} == t;

expose t, numbers;
SNT

puts program