Constraint independent and caching

[Tianhai Liu]

Hi,

I understand the techniques constraint independent and caching described
in KLEE paper, then I want to see how it works in KLEE, so I used KLEE to
analyze a small code. while I could not understand the generation.

When KLEE runs on the function as below: klee -use-query-log=all:smt2
-use-query-log=all:pc -use-query-log=solver:smt2 -use-query-log=solver:pc
-write-pcs -write-smt2s -write-cov -search=dfs constraint_independent.o

int constraint_independent(int x, int y) {
int c = 0;
if (x == 0) c = x++; // B1
else c = x--; // B2

if (y < 0) c = y++; // B3
else c = y--; // B4

return c;
}

Before optimization, I can see the KLEE generate Path conditions in the
order that (from file "all-queries.smt2"):
query0: [B2]
query1: [B2,B4]
query2: [B2,B4,True]
query3: [B2,B3,True]
query4: [B1,B3]
query5: [B1,B3,True]
query6: [B1,B4,True]

after optimizations, I presume the queries to the solver would be like :
query0: [B2] // wrt. query0.
query1: [B4] // wrt. query2. B1/B2 and B3/B4 are independent
query2: [B3] // wrt. query3
query3: [B1] // wrt. query4
query4: [B3] // wrt. query5
query5: [B4] // wrt. query6

while the actual queries to the solver is (from file
"solver-queries.smt2"):
query0: [True]
query1: [B2]
query2: [B3]
query3: [B2,B3,True]

Is my presumption correct if only considering the constraint independent
and caching? If not, do I need some options to disable other
optimizations? Btw, is there some reason to introduce the "True" for some
PCs? I appreciate any suggestion and help highly.

Best regards,
Tianhai