Missing subsumption with klee_assume

[domainexpert]

In Tracer-X run, the following example shows no subsumption, but there would are subsumptions when the call to klee_assume is replaced with x = 0;.

/*
 * Copyright 2017 National University of Singapore 
 */

#include <klee/klee.h>
#include <assert.h>

int inc(int x) { 
  return x + 1;
} 

int main() {
  char p1, p2;
  int x;

  klee_make_symbolic(&x, sizeof(x), "x");
  klee_make_symbolic(&p1, sizeof(p1), "p1");
  klee_make_symbolic(&p2, sizeof(p2), "p2");

  klee_assume(x == 0);

  if (p1) {
    x++;
  } else {
    x = inc(x);
  }

  if (p2) {
    x++;
  } else {
    x = inc(x);
  }

  klee_assert(x > 0);

  return 0;
} 

[domainexpert]

The following tree shows the subsumptions when the klee_assume() call is replaced with x = 0;.

[domainexpert]

The problem is because Z3 could not resolve the constraint with existential quantification.

KLEE: Querying for subsumption check:
antecedent:
        (0 = x[3].x[2].x[1].x[0])
        !(0 = p1[0])
        (0 = p2[0])
consequent:
        (exists (__shadow__x) ((1 + __shadow__x[3].__shadow__x[2].__shadow__x[1].__shadow__x[0]) = (1 + x[3].x[2].x[1].x[0])))

KLEE: #6=>#3: Check failure as solved did not decide validity of existentially-quantified query

[domainexpert]

Related to #220 and #280.

[domainexpert]

This issue seems to be due to an inconsistent result of Z3 when called from the command line and when the C API is used. I had Z3 dump the content of the solver as follows:

(declare-fun x0 () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun |1| () Bool)
(declare-fun p11 () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun |2| () Bool)
(declare-fun p22 () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun |3| () Bool)
(declare-fun __shadow__x () (Array (_ BitVec 32) (_ BitVec 8)))
(assert (let ((a!1 (concat (select x0 #x00000003)
                   (concat (select x0 #x00000002)
                           (concat (select x0 #x00000001)
                                   (select x0 #x00000000))))))
  (=> |1| (= #x00000000 a!1))))
(assert (=> |2| (not (= #x00 (select p11 #x00000000)))))
(assert (=> |3| (= #x00 (select p22 #x00000000))))
(assert (not (exists ((__shadow__x (Array (_ BitVec 32) (_ BitVec 8))))
       (let ((a!1 (concat (select __shadow__x #x00000003)
                          (concat (select __shadow__x #x00000002)
                                  (concat (select __shadow__x #x00000001)
                                          (select __shadow__x #x00000000)))))
             (a!2 (concat (select x0 #x00000003)
                          (concat (select x0 #x00000002)
                                  (concat (select x0 #x00000001)
                                          (select x0 #x00000000))))))
         (= (bvadd #x00000001 a!1) (bvadd #x00000001 a!2))))))

When (check-sat) added at the end, the command-line z3 tool reports unsat, however, the result of Z3_solver_check() call in Z3SolverImpl::internalRunSolver() is Z3_L_TRUE which means Z3 proved satisfiability.

[domainexpert]

The existence of

(declare-fun __shadow__x () (Array (_ BitVec 32) (_ BitVec 8)))

in the above is funny. Existentials should not have been declared as functions.

[domainexpert]

Resolved via #307.