阴阳 SMT求解器的模糊器。 给定一组种子SMT公式,阴阳会生成突变体公式以对SMT求解器进行压力测试。 yinyang可用于增强SMT求解器的稳定性。 它已经在两个最先进的SMT求解器Z3和CVC4中发现了1,000多个错误。 安装 要求: python 3.6+ antlr4 python运行时 git clone https://github.com/testsmt/yinyang.git pip3 install antlr4-python3-runtime==4.8 用法 获得SMT-LIB 2基准。 编辑scripts/SMT-LIB-clone.sh以选择测试逻辑。 运行