How to disable formula slicing?

[Yoel Kim]

Dear CPAchecker team,

I have noticed that when the following code is translated into the corresponding SMT formula, formula slicing removes the formula for 'c_i = c[i]':

for(i=1;i<N;i++) {

    c_i = c[i];

    __VERIFIER_assert(c[i] == 0);

  }

The resulting formula is as follows:

(`not` (`and` (`and` (`not` (`<=_int` N@2 main::i@5)) (`=_int` (`ite_int` (`=_int` (`read_int_int` *int@1 (`+_int` __ADDRESS_OF_main::c@ (`*_int` 4 main::i@5))) 0) 1 0) __VERIFIER_assert::cond@2)) (`=_int` __VERIFIER_assert::cond@2 0)))

However, I need to retain the formula for 'c_i = c[i]', for my own refinement process.

Is there an option to disable formula slicing?

Best Regards,

Yoel

[Philipp Wendler]

Dear Yoel,

Am 12.02.25 um 10:48 schrieb Yoel Kim:

> Dear CPAchecker team,
>
> I have noticed that when the following code is translated into the
> corresponding SMT formula, formula slicing removes the formula for 'c_i =
> c[i]':

For clarification: We don't do any formula slicing, which I would
understand as removing parts of a formula after determining that they
are unnecessary. But we do simplify the program in various steps of
CPAchecker and remove irrelevant parts, and skip generating formulas for
even more irrelevant parts, so the effect is similar.

For ignoring irrelevant (never read) variables and struct fields there
are the following two options (default value is true):

cpa.predicate.ignoreIrrelevantFields
cpa.predicate.ignoreIrrelevantVariables

The latter should be what you need.

Greetings
Philipp
--
Philipp Wendler
Software and Computational Systems Lab
LMU Munich, Germany
Oettingenstr. 67 Raum F008 - Tel.: 089/2180-9181