yinyang
yinyang copied to clipboard
testsmt
A fuzzing framework for SMT solvers
yinyang (version 0.3.0 installed via pip) consumes ~40G of memory when running with the provided `semantic-fusion-seeds/QF_SLIA` seeds. Using more seeds will increase memory consumption (with the QF_SLIA logic from SMT-LIB...
This mostly means to make the type-checker capable of dealing with SMT-LIB files of all logics. It is already implemented but not yet robust enough.
Commit: d8174eb The parser currently rejects formulas such as the one below. ``` (declare-fun bv () (_ BitVec 10)) (declare-fun a () Bool) (assert (not (and (= ((_ extract 5...
Actions: - devise parallel run script make sure some logs are generated so errors can be diagnosed quickly; add it to `scripts` - provide 1-2 sentence documentation on how to...
make Typefuzz more robust as it fails on several benchmarks Related issues: #31 , #33, #34
This makes the typechecker fail (but z3 and cvc4 are happy with it): ```smt (declare-fun x () Int) (assert (=> (= x 3) (forall ((x Int)) (let ((?y x)) (=...
Some regex constants, i.e., re.none, re.all, and re.allchar, from the config/generalization.txt need some special treatment as they are constants. At the moment, when they are used, extra '(' and ')'...
The rule for "(par (A) (id A A))" might be enabled too infrequently as there are many other rules in the config rule. Not sure what would be the best...
Make option fuzzing for cvc4 to be more general (not only boolean flags) and abide by their fuzzing guidelines