[Question] Can the input set be partitioned into multiple subsets?

[neiling]

I'm relatively new to bounded model checking, so please bear with me if this question seems basic.

Can the input set be partitioned into multiple subsets for the proof? For instance, if I have a sum function that I want to prove over the input set {1,2,…,10000}, is it feasible to also conduct the proof over the subsets {{1,2,…,1000}{1001,…,2000},...,{9001,…,10000}}?

Will the conclusions regarding memory safety, integer overflows, and other properties remain consistent?

I'm curious because I've noticed that the runtime and memory usage are considerably reduced when verifying over these subsets.

// Are sum_subsets_harness and sum_superset_harness equivalent?

uint64_t calc_sum(const uint64_t n) {
  uint64_t sum = 0;
  for (uint64_t k = 1; k <= n; ++k) {
    sum += k;
  }
  return sum;
}

// cbmc sum.c --unwinding-assertions --unwind 1000 --function sum_subsets_harness
void sum_subsets_harness(void) {
  const uint64_t n;
  uint64_t sum;
  for (uint64_t i = 1; i <= 10; ++i) {
    __CPROVER_assume(n >= (1 * i) && n < (1000 * i));
    sum = calc_sum(n);
    __CPROVER_assert(sum = (n * (n + 1)) / 2, "");
  }
}

// cbmc sum.c --unwinding-assertions --unwind 10000 --function sum_superset_harness
void sum_superset_harness(void) {
  const uint64_t n;
  uint64_t sum;
  __CPROVER_assume(n >= 1 && n < 10000);
  sum = calc_sum(n);
  __CPROVER_assert(sum = (n * (n + 1)) / 2, "");
}