文件名称：阴阳：SMT求解器的模糊器
文件大小：2.05MB
文件格式：ZIP
更新时间：2024-02-26 18:47:38
testing fuzzing z3 smt smt-solver
阴阳 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以选择测试逻辑。 运行