Does flasification force ESBMC to produce more guarded copies of the loop bodies?

[kunjsong01]

Since both --incremental-bmc and --falsification are strategies based on loop unwinding, I'm trying to use the test case below to figure out what's behind the scenes.

#include <assert.h>
int main() {
  int x=10;
  while(x>0) x--; // All states are reached when k=11 is provided. 
  assert(x==0);
  return 0;
}

Using ./esbmc main.c --max-k-step 9 --falsification and ./esbmc-new main.c --max-k-step 9 --incremental, ESBMC would give VERIFICATION UNKNOWN, which is expected because 9<11.

Using ./esbmc main.c --max-k-step 15 --incremental-bmc, ESBMC would unroll the loop up to k=11 and give VERIFICATION SUCCESSFUL, which is also expected because --incremental-bmc cares about unwinding assertions and checks whether the loop is fully unrolled.

Using ./esbmc main.c --max-k-step 15 --falsification, ESBMC unrolls the loop up to k=15 but gives VERIFICATION UNKNOWN --- why?
My understanding is that --falsification replaces all unwinding assertions with unwinding assumptions and forces ESBMC to generate more guarded copies of the loop bodies in such a way that the loop execution is "pushed" forward. So shouldn't the final value of x be a negative which in turns fails the property (i.e. assertion(x==0);)?

Is this the expected behaviour? or possibly implies an issue?

[kunjsong01]

ESBMC version: 06663d7

[lucasccordeiro]

That's correct, @kunjsong01.

The falsification strategy searches for counterexamples only, i.e., if there is a property violation within k steps, it should produce "VERIFICATION FAILED"; otherwise, it will generate "VERIFICATION UNKNOWN".