Over-subsumption due to pre-solving in subsumption check

[domainexpert]

Consider the following program. The assertion violation is not reported due to over-subsumption.

/*
 * This example exhibits the situation where some path conditions that
 * are needed in subsumption check gets missing from the interpolant
 * of the subsumed states. The second issue is that this also shows an
 * over-simplification of formula at subsumption check resulting in
 * successful subsumption that should have failed.
 *
 * Copyright 2017 National University of Singapore
 */

#ifdef LLBMC
#include <llbmc.h>
#else
#include <klee/klee.h>
#endif

int main() {
  int wcet,q;
  int a,b,c;
  char p;

#ifdef LLBMC
  a = __llbmc_nondef_int();
  b = __llbmc_nondef_int();
  c = __llbmc_nondef_int();
  wcet = __llbmc_nondef_int();
  p = __llbmc_nondef_char();

  if (p) {
    __llbmc_assume(wcet == 1);
  } else {
    __llbmc_assume(wcet == 0);
  }
#else
  klee_make_symbolic(&a, sizeof(int), "a");
  klee_make_symbolic(&b, sizeof(int), "b");
  klee_make_symbolic(&c, sizeof(int), "c");
  klee_make_symbolic(&wcet, sizeof(int), "wcet");
  klee_make_symbolic(&p, sizeof(char), "p");

  if (p) {
    klee_assume(wcet == 1);
  } else {
    klee_assume(wcet == 0);
  }
#endif
  q = 5;

  if (a >= 0){
    wcet +=5;        // PP 9
     q +=3;
#ifdef LLBMC
     __llbmc_assert(wcet <= 5);
#else
     klee_assert(wcet <= 5);
#endif
  }else{
    wcet+=5;         // PP 2
     q +=4;
  }

  if (b != 1){
     wcet+=2;
     q +=5;
  }else{
     wcet+=2;
     q +=6;
  }

  if (c >= 0){
     wcet+=2;
     q +=5;
  }else{
     wcet+=2;
     q +=6;
  }

#ifdef LLBMC
  __llbmc_assert(wcet < 10);
#else
  klee_assert(wcet < 10);
#endif
} 

This can be seen from -debug-subsumption=3 log.

KLEE: Subsumption check for Node #14, Program Point 41552752
KLEE: Before simplification:
antecedent:
        !(0 = p[0])
        (1 = wcet[3].wcet[2].wcet[1].wcet[0])
        !(0 \<= a[3].a[2].a[1].a[0])
consequent:
        (exists (__shadow__wcet) ((0 = __shadow__wcet[3].__shadow__wcet[2].__shadow__wcet[1].__shadow__wcet[0]) & ((5 + __shadow__wcet[3].__shadow__wcet[2].__shadow__wcet[1].__shadow__wcet[0]) = (5 + wcet[3].wcet[2].wcet[1].wcet[0]))))

KLEE: Existentials not empty
KLEE: Querying for subsumption check:
antecedent:
        !(0 = p[0])
        (1 = wcet[3].wcet[2].wcet[1].wcet[0])
        !(0 \<= a[3].a[2].a[1].a[0])
consequent:
        (exists (__shadow__wcet) ((5 + __shadow__wcet[3].__shadow__wcet[2].__shadow__wcet[1].__shadow__wcet[0]) = (5 + wcet[3].wcet[2].wcet[1].wcet[0])))

KLEE: #14=>#3: Check success as solver decided validity

After the simplification, the constraint _shadow__wcet == 0 disappeared, making subsumption holds.

[domainexpert]

Resolved via #322.