Zesti: Making a particular instruction as sensitive

[Sandeep Dasgupta]

Hello Sir,

Currently I am working on Zesti to solve a problem which is similar to
one described below.

I have a static analysis which could figure out what all things a could
get assigned in the following code segment.

if(...) {
a = 1;
} else {
if(...) {
a = 2;
} else {
a = 3;
}
}

Now the static analyzer will put the following test and expect the
symbolic engine to explore all possible paths
that can assign to a and make the following condition true. If there is
a bug in the analyzer and hence cannot interpret the
disjuncts correctly then the abort will get hit.

*if(a == 1 || a == 2 || a == 3) {*
// I am OK
} else {
abort;
}

Here my goal is to make the bolded statement sensitive so that zesti can
explore all the alternative paths reaching that statement.
The challenge is there could be many similar conditional statement and i
have to deliberately make the bolded one as sensitive. Can you suggest
me ways of doing that.