We study the decision problem for the existential fragment of the theory of power structures. We prove complexity results that parallel the decidability results of Feferman-Vaught for the theories of product structures thereby showing that the construction of Hintikka formulae is not necessary in the quantifier-free case. We show that the result stays true when the theory of the indices is enriched with a finiteness or an order predicate. We prove that the resulting logical fragment gives quantifier-free logics suitable for verification. We conclude by applying the developed techniques to the existential fragment of the theory of non-linear integer arithmetic and the theory of arrays.