—Satisfiability Modulo Theory (SMT) solvers play a crucial role in various domains and applications. Therefore, ensuring their correctness and robustness becomes increasingly vital. Fuzzing is an efficient and effective method for validating the quality of SMT solvers, utilizing inputs that consist of solving formulas and configuration options. However, existing fuzzing methods focus solely on generating formulas or simply combining options and formulas, neglecting the complex interactions between options. Yet, randomly combining multiple options can lead to a combinatorial explosion and result in numerous invalid inputs. To overcome these limitations, we propose OptionFuzz, a fuzzer that optimizes option exploration by identifying relationships between solver options, reducing invalid inputs and mitigating combinatorial explosion. OptionFuzz identifies option relationships using large language models (LLMs), which analyze official documentation of options. These identified relationships are transformed to a relation graph, enabling efficient traversal to derive related option combinations and generate high-quality fuzz inputs. To evaluate OptionFuzz’s effectiveness, we conduct comprehensive evaluations on two state-of-the-art SMT solvers, Z3 and CVC5. OptionFuzz demonstrates its effectiveness by accurately extracting option relationships with an accuracy of 95.23% and a recall rate of 90.10%. Leveraging these relationships, OptionFuzz reduces the number of options combinations to be tested by 70.11%. Notably, OptionFuzz has detected 34 unique bugs, 20 of which have been fixed by developers, and 5 have been assigned CVE IDs due to their severity.