Large language models (LLMs) have recently demonstrated strong capabilities in code understanding and generation. However, existing LLM-based vulnerability detection approaches often suffer from hallucinations and a lack of formal constraint reasoning, which limits the reliability of their predictions. In contrast, traditional symbolic execution provides logically sound and highly trustworthy analysis but struggles with path explosion and insufficient semantic modeling in complex programs. To leverage the strengths of both paradigms, we propose SAVD, a vulnerability detection framework that integrates assertion-guided slicing with LLM-assisted semantic reasoning. SAVD first extracts assertion-relevant execution paths through dependence analysis to focus on semantically meaningful program segments. It then employs LLMs to generate logic constraints that describe conditions under which assertions may fail, enabling more precise reachability reasoning. Finally, a verifier-in-the-loop mechanism iteratively refines these constraints using counterexample feedback, improving both accuracy and robustness. Experiments across multiple benchmark datasets show that SAVD improves the accuracy of assertion-relevant vulnerability detection by 29.74% over baseline approaches, demonstrating its effectiveness in bridging semantic reasoning and formal verification for reliable automated vulnerability detection.