search

testsmt / yinyang

A fuzzing framework for SMT solvers
https://testsmt.github.io/
MIT License
185 stars 23 forks source link

Cannot detect soundness issue when (get-model) is in the mutant. #18

Closed muchang closed 3 years ago

muchang commented 3 years ago

When there is a (get-mode) in the seeds, the mutant will also bring a (get-model) after mutation. If we use this mutant to test SMT solvers, the solvers would report:

unsat
(error "line 13 column 10: model is not available")

or 

sat
(error "Cannot get model when produce-models options is off.")

Since they contain error, such outputs will be ignored by yinyang even though this mutant triggers a soundness bug. We could get rid of (get-model) in our mutants.