You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
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:
or
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.The text was updated successfully, but these errors were encountered: