Hi,
I think I might have found a problem with the AASTORE for symbolic arrays.
When executed on a concrete array with a symbolic index, the path condition is not saved in the current choice generator.
(I don't have much experience with SPF, please let me know if I'm wrong :) )
Hi, I think I might have found a problem with the AASTORE for symbolic arrays. When executed on a concrete array with a symbolic index, the path condition is not saved in the current choice generator.
(I don't have much experience with SPF, please let me know if I'm wrong :) )
Best, Donato