Benchmark to check QF_BV extensions

[Tjark Weber]

Dear QF_BV implementors,

I crafted a small benchmark (currently available at [1]) to check that
the extensions defined in the QF_BV logic are implemented according to
their definitions (as given in [2]).

The benchmark was motivated by a bug that I discovered in an older
version of Z3 related to bit-vector division by 0. This benchmark would
have exposed the bug (and, more generally, many incorrect QF_BV
implementations).

Pascal suggested that I advertise it here, so that you get a chance to
discover non-conforming implementations now, rather than after the next
SMT-LIB release. I hope you will find the benchmark useful.

Best,
Tjark

[1]
https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks-tmp/benchmarks-pending/-/blob/829057eedc74702127d288841e87a71e873c15f1/TODO/QF_BV/2020-Weber/extensions.smt2
[2] http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV









När du har kontakt med oss på Uppsala universitet med e-post så innebär det att vi behandlar dina personuppgifter. För att läsa mer om hur vi gör det kan du läsa här: http://www.uu.se/om-uu/dataskydd-personuppgifter/

E-mailing Uppsala University means that we will process your personal data. For more information on how this is performed, please read here: http://www.uu.se/en/about-uu/data-protection-policy