Putting the general versions of variables into the precision instead of the instance versions makes Theta not be able to verify some tasks, while allowing some previously unverified tasks to be verified.
General versions of variables are put into the precision if both reverseLookup and additionalLookup are used in changeVars, while instances are used if reverseLookup is omitted.
For recursive tasks:
Fibonacci02.c, fibo_10-2.c, fibo_2calls_10-1.c, fibo_2calls_6-1.c, fibo_2calls_8-1.c, fibo_7-1.c can only be verified with general vars, not with instances,
Ackermann02.c, Addition02.c, BallRajamani-SPIN2000-Fig1.c can only be verified with instances, not with general vars.
Explicit abstraction performs better with general vars (49 vs. 39), while predicate abstraction solves significantly more tasks with instances (15 vs. 44).
Putting the general versions of variables into the precision instead of the instance versions makes Theta not be able to verify some tasks, while allowing some previously unverified tasks to be verified.
https://github.com/ftsrg/theta/blob/22257ee2f1c091346760c800f9ded00f4681f473/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaPrecRefiner.kt#L45-L57
General versions of variables are put into the precision if both
reverseLookupandadditionalLookupare used inchangeVars, while instances are used ifreverseLookupis omitted.For recursive tasks:
Fibonacci02.c,fibo_10-2.c,fibo_2calls_10-1.c,fibo_2calls_6-1.c,fibo_2calls_8-1.c,fibo_7-1.ccan only be verified with general vars, not with instances,Ackermann02.c,Addition02.c,BallRajamani-SPIN2000-Fig1.ccan only be verified with instances, not with general vars.For multithreaded tasks, general vars are preferred, as there were over 200 tasks that Theta can only solve with general vars and not with instances (see https://github.com/ftsrg/theta/pull/244#issuecomment-1822224299).
This behavior does not seem to be by-design and should be investigated.