Problem with SMT and for loops

[rmn30]

prop_sail_bug in the following produces a 'Failed to replay counterexample' error when used with sail -smt -smt_auto.

default Order dec
$include <prelude.sail>

val sum_n : nat -> nat
function sum_n(n)= {
  var s : nat = 0;
  foreach(i from 1 to n by 1 in inc) 
    s = s + i;
  s
}

$counterexample
function prop_sail_no_bug() -> bool = {
    sum_n(10) == 55
}

$counterexample
function prop_sail_bug() -> bool = {
    sum_n(11) == 66
}

Amusingly the SMT problems for these two properties consist of assert false and assert true! I guess this is because Sail unrolls the loop up to 10 times then gives up? I guess this is a known limitation but I am just noting it here as it caused me some confusion on #1562 and was the last thing I wanted to understand before marking #1573 ready for review.