@article{Reynolds_2016,
    doi = {10.1007/s10817-016-9372-6},
    url = {https://doi.org/10.1007%2Fs10817-016-9372-6},
    year = {2016},
    month = {may},
    publisher = {Springer Science and Business Media {LLC}},
    volume = {58},
    number = {3},
    pages = {341--362},
    author = {Andrew Reynolds and Jasmin Christian Blanchette},
    title = {A Decision Procedure for (Co)datatypes in {SMT} Solvers},
    journal = {Journal of Automated Reasoning}
}

@article{Reynolds_2016, doi = {10.1007/s10817-016-9372-6}, url = {https://doi.org/10.1007%2Fs10817-016-9372-6}, year = {2016}, month = {may}, publisher = {Springer Science and Business Media {LLC}}, volume = {58}, number = {3}, pages = {341--362}, author = {Andrew Reynolds and Jasmin Christian Blanchette}, title = {A Decision Procedure for (Co)datatypes in {SMT} Solvers}, journal = {Journal of Automated Reasoning} }