CPAchecker validates wrong witness using predicate analysis for no-overflow

The following witness:

- entry_type: "invariant_set"
  metadata:
    format_version: "2.0"
    uuid: "cba90611-7aaa-3e70-a3ce-826233d02f9f"
    creation_time: "2024-07-15T17:35:56+02:00"
    producer:
      name: "CPAchecker"
      version: "3.1-svn"
      configuration: "kInduction"
    task:
      input_files:
        - "../paper/paper/figures/examples/correctness-witnesses/example-safe.c"
      input_file_hashes:
        "../paper/paper/figures/examples/correctness-witnesses/example-safe.c": "b1d326615fa7bc45446a3449062206d651e14b5d7b5d45c21fde096fe70a4790"
      specification: "CHECK( init(main()), LTL(G ! call(reach_error())) )"
      data_model: "ILP32"
      language: "C"
  content:
    - invariant:
        type: "loop_invariant"
        location:
          file_name: "../paper/paper/figures/examples/correctness-witnesses/example-safe.c"
          line: 23
          column: 3
          function: "main"
        value: "0"
        format: "c_expression"

is being correctly validated for the program ../sv-benchmarks/c/loops/trex02-1.c, see below:

extern void abort(void);
extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
void reach_error() { __assert_fail("0", "trex02-1.c", 3, "reach_error"); }

void __VERIFIER_assert(int cond) {
  if (!(cond)) {
    ERROR: {reach_error();abort();}
  }
  return;
}
_Bool __VERIFIER_nondet_bool();
int __VERIFIER_nondet_int();

//x is an input variable
int x;

void foo() {
  x--;
}

int main() {
  x=__VERIFIER_nondet_int();
  while (x > 0) {
    _Bool c = __VERIFIER_nondet_bool();
    if(c) foo();
    else foo();
  }
  __VERIFIER_assert(x<=0);
}

even though the invariant is clearly false i.e. 0.

The command line used is: bin/cpachecker --witnessValidation --spec ../sv-benchmarks/c/properties/no-overflow.prp -w witness-2.0.yml ../sv-benchmarks/c/loops/trex02-1.c