Control systems play a crucial role in various domains necessitating high reliability and proof of correct software operation. To address this, formal methods, such as deductive verification, are employed to ensure the correctness of safety-critical software mathematically. This process involves generating verification conditions from the program's axiomatic semantics and its requirements. Main disadvantage of manual verification condition generation is its labor-intensity and prone to human error, which leads to the development of automated verification condition generators. However, they produce excessive or overly complex verification conditions that do not accurately reflect the possible program's operational paths. To mitigate the second issue, domain-oriented languages like Reflex have been introduced, which adopt a process-oriented paradigm to streamline programming and simplify verification condition generation. Nevertheless, the inherent switch-case structure of Reflex can lead to an increase in the number of verification conditions, exacerbating the first issue and complicating the selection of relevant ones. This paper proposes a simple static analysis system designed to optimize the generation of verification conditions for Reflex programs, enhancing the efficiency of the verification process. It is based on attaching attributes to different statements. Then, throughout the verification condition generation these attributes are collected and checked to be compatible with previously collected. If attributes are incompatible then verification condition are discarded.