Incorrect handling of constant variables

This witness (witness.graphml) contains a safe and inductive invariant for the program (sw_sym_ex.c).

However, LIV (at commit cf736e45) computes a wrong answer when checking the inductivity of the invariant.

liv$ bin/liv --no-cache-update --cache-dir lib/cvt_cache/ \
    --verifier actors/cbmc.yml --verifierversion default \
    --allow-missing-invariant --all-possible-invariant-locations --fuzzy-invariant-locations 1 \
    --witness witness.graphml --property path/to/unreach-call.prp --data-model LP64 sw_sym_ex.c
Generated 3 programs
Using verifier "cbmc-default" from actors/cbmc.yml which claims to be tool version "CBMC 5.43.0 (cbmc-5.43.0-18-gb83f0e1cc3)"
Verification result of output/program_1.c: true
Verification result of output/program_2.c: false(unreach-call)
Verification result of output/program_3.c: true
Overall result: false

Some constant variables are declared at the beginning of main of sw_sym_ex.c:

  // snippet of sw_sym_ex.c
  typedef unsigned char SORT_1;  // BV with 8 bits
  const SORT_1 mask_SORT_1 = (SORT_1)-1 >> (sizeof(SORT_1) * 8 - 8);
  const SORT_1 msb_SORT_1 = (SORT_1)1 << (8 - 1);
  typedef unsigned char SORT_5;  // BV with 1 bits
  const SORT_5 mask_SORT_5 = (SORT_5)-1 >> (sizeof(SORT_5) * 8 - 1);
  const SORT_5 msb_SORT_5 = (SORT_5)1 << (1 - 1);
  const SORT_5 var_7 = 0;
  const SORT_5 var_13 = 1;
  const SORT_1 var_33 = 0;
  const SORT_1 var_42 = 4;
  const SORT_1 var_54 = 5;
  const SORT_1 var_193 = 3;
  const SORT_1 var_199 = 2;

When generating program_2.c, LIV incorrectly havocked these constant variables:

  // snippet of program_2.c
  typedef unsigned char SORT_1;
  const SORT_1 mask_SORT_1 = __VERIFIER_nondet_char();
  const SORT_1 msb_SORT_1 = __VERIFIER_nondet_char();
  typedef unsigned char SORT_5;
  const SORT_5 mask_SORT_5 = __VERIFIER_nondet_char();
  const SORT_5 msb_SORT_5 = __VERIFIER_nondet_char();
  const SORT_5 var_7 = __VERIFIER_nondet_char();
  const SORT_5 var_13 = __VERIFIER_nondet_char();
  const SORT_1 var_33 = __VERIFIER_nondet_char();
  const SORT_1 var_42 = __VERIFIER_nondet_char();
  const SORT_1 var_54 = __VERIFIER_nondet_char();
  const SORT_1 var_193 = __VERIFIER_nondet_char();
  const SORT_1 var_199 = __VERIFIER_nondet_char();

As some constraints in the invariant depend on the constant variables, such havocking alters the satisfiability of the query. (The correct answer should be true, but now it becomes false.)

In fact, if program_2.c is modified to preserve these constant values program_2_mod.c), then the inductivity check succeeds (confirmed by CBMC)