Project Yin-Yang for SMT Solver Testing

Bug findings with Type-aware mutation

========= CVC4 =========

Soundness Bugs

Refutation Soundness

https://github.com/cvc5/cvc5/issues/6776 Fixed
https://github.com/cvc5/cvc5/issues/6681 Fixed
https://github.com/cvc5/cvc5/issues/6654 Confirmed
https://github.com/cvc5/cvc5/issues/6520 Fixed
https://github.com/CVC4/CVC4/issues/6142 Fixed
https://github.com/CVC4/CVC4/issues/6191 Fixed
https://github.com/CVC4/CVC4/issues/5940 Fixed

Solution Soundness

https://github.com/cvc5/cvc5/issues/6913 Fixed
https://github.com/cvc5/cvc5/issues/6604#issuecomment-847241234 Fixed
https://github.com/cvc5/cvc5/issues/6604#issue-898823692 Fixed
https://github.com/cvc5/cvc5/issues/6639#issue-906870227 Fixed
https://github.com/cvc5/cvc5/issues/6637#issuecomment-852452585 Dup
https://github.com/cvc5/cvc5/issues/6637#issue-906523476 Fixed
https://github.com/cvc5/cvc5/issues/6636 Fixed
https://github.com/cvc5/cvc5/issues/6635 Fixed
https://github.com/cvc5/cvc5/issues/6622 Fixed
https://github.com/cvc5/cvc5/issues/6567 Fixed
https://github.com/cvc5/cvc5/issues/6560 Fixed
https://github.com/cvc5/cvc5/issues/6483 Fixed
https://github.com/CVC4/CVC4/issues/6214#issuecomment-813495575 Fixed
https://github.com/CVC4/CVC4/issues/6214#issuecomment-812857277 Dup
https://github.com/CVC4/CVC4/issues/6214 Fixed
https://github.com/CVC4/CVC4/issues/6101 Fixed
https://github.com/CVC4/CVC4/issues/6075 Fixed
[CVC4/CVC4#5915](https://github.com/CVC4/CVC4/issues/5915) Fixed

Others

https://github.com/cvc5/cvc5/issues/7252#issue-1006824288 Confirmed
https://github.com/cvc5/cvc5/issues/6973 Confirmed
https://github.com/cvc5/cvc5/issues/6653#issuecomment-857073800 Confirmed
https://github.com/cvc5/cvc5/issues/6765#issuecomment-864151487 Confirmed
https://github.com/cvc5/cvc5/issues/6754 Fixed
https://github.com/cvc5/cvc5/issues/6765 Confirmed
https://github.com/cvc5/cvc5/issues/6766 Confirmed
https://github.com/cvc5/cvc5/issues/6653 Confirmed
https://github.com/cvc5/cvc5/issues/6653 Confirmed
https://github.com/cvc5/cvc5/issues/6604 Fixed
https://github.com/cvc5/cvc5/issues/6637#issuecomment-852928419 Dup
https://github.com/cvc5/cvc5/issues/6625 Fixed
https://github.com/cvc5/cvc5/issues/6620 Fixed
https://github.com/cvc5/cvc5/issues/6605 Confirmed
https://github.com/cvc5/cvc5/issues/6561#issuecomment-843546850 Fixed
https://github.com/cvc5/cvc5/issues/6545 Fixed
https://github.com/cvc5/cvc5/issues/6536 Fixed
https://github.com/CVC4/CVC4/issues/6057#issuecomment-814732785 Fixed
https://github.com/CVC4/CVC4/issues/6203#issuecomment-813501494 Fixed
https://github.com/cvc5/cvc5/issues/6214#issuecomment-812903986 Fixed
https://github.com/cvc5/cvc5/issues/6214#issuecomment-812858369 Dup
https://github.com/CVC4/CVC4/issues/6203#issuecomment-810860309 Fixed
https://github.com/CVC4/CVC4/issues/6203#issuecomment-810859231 Fixed
https://github.com/CVC4/CVC4/issues/6228#issuecomment-809130679 Dup
https://github.com/CVC4/CVC4/issues/6228 Fixed
https://github.com/CVC4/CVC4/issues/6203#issuecomment-809136033 Fixed
https://github.com/CVC4/CVC4/issues/6203 Fixed
https://github.com/CVC4/CVC4/issues/6192 Fixed
[CVC4/CVC4#6180](https://github.com/CVC4/CVC4/issues/6180) Confirmed
https://github.com/CVC4/CVC4/issues/6132 Fixed
https://github.com/CVC4/CVC4/issues/6057 Fixed
https://github.com/CVC4/CVC4/issues/6056 Fixed
https://github.com/CVC4/CVC4/issues/5943 Fixed
https://github.com/CVC4/CVC4/issues/5816 Fixed
https://github.com/CVC4/CVC4/issues/5815 Confirmed

========= Z3 =========

Soundness Bugs

Refutation Soundness

https://github.com/Z3Prover/z3/issues/5429#issuecomment-885793775 Fixed
https://github.com/Z3Prover/z3/issues/5429#issuecomment-885778234 Fixed
https://github.com/Z3Prover/z3/issues/5140#issuecomment-814310059 Fixed
https://github.com/Z3Prover/z3/issues/5140#issuecomment-846386635 Fixed
https://github.com/Z3Prover/z3/issues/5140#issuecomment-846446190 Fixed
https://github.com/Z3Prover/z3/issues/5140#issuecomment-846446946 Fixed
https://github.com/Z3Prover/z3/issues/5140#issuecomment-847352530 Fixed
https://github.com/Z3Prover/z3/issues/5140#issuecomment-851049176 Fixed
https://github.com/Z3Prover/z3/issues/5140#issuecomment-892583476 Fixed
https://github.com/Z3Prover/z3/issues/5467#issuecomment-895648140 Confirmed
https://github.com/Z3Prover/z3/issues/2650#issuecomment-854891402 Reported
https://github.com/Z3Prover/z3/issues/2650#issuecomment-852910615 Reported
https://github.com/Z3Prover/z3/issues/2650#issuecomment-852088518 Reported
https://github.com/Z3Prover/z3/issues/2650#issuecomment-851051592 Reported
https://github.com/Z3Prover/z3/issues/2650#issuecomment-830862350 Reported
https://github.com/Z3Prover/z3/issues/2650#issuecomment-829061143 Reported
https://github.com/Z3Prover/z3/issues/5467#issuecomment-895648011 Confirmed
https://github.com/Z3Prover/z3/issues/5140#issuecomment-868855897 Fixed
https://github.com/Z3Prover/z3/issues/2650#issuecomment-880092673 Reported
https://github.com/Z3Prover/z3/issues/5301 Dup
https://github.com/Z3Prover/z3/issues/5324#issuecomment-852984716 Fixed
https://github.com/Z3Prover/z3/issues/5324# Fixed
https://github.com/Z3Prover/z3/issues/5324#issuecomment-852907754 Fixed
https://github.com/Z3Prover/z3/issues/5324#issuecomment-852440597 Fixed
https://github.com/Z3Prover/z3/issues/5324#issue-908251210 Fixed
https://github.com/Z3Prover/z3/issues/5223 Fixed
https://github.com/Z3Prover/z3/issues/5223#issuecomment-828600799 Fixed
https://github.com/Z3Prover/z3/issues/5223#issuecomment-828599679 Fixed
https://github.com/Z3Prover/z3/issues/5223#issuecomment-828598613 Fixed
https://github.com/Z3Prover/z3/issues/5161 Dup
https://github.com/Z3Prover/z3/issues/5042#issuecomment-812978896 Dup
https://github.com/Z3Prover/z3/issues/5042#issuecomment-812848711 Dup
https://github.com/Z3Prover/z3/issues/5142 Fixed
https://github.com/Z3Prover/z3/issues/5141 Dup
https://github.com/Z3Prover/z3/issues/5127 Fixed
https://github.com/Z3Prover/z3/issues/5117 Fixed
https://github.com/Z3Prover/z3/issues/5112 Dup
https://github.com/Z3Prover/z3/issues/5111 Fixed
https://github.com/Z3Prover/z3/issues/5108 Fixed
https://github.com/Z3Prover/z3/issues/5086 Won't fix
https://github.com/Z3Prover/z3/issues/5083 Won't fix
[Z3Prover/Z3#5076](https://github.com/Z3Prover/z3/issues/5076) Dup
https://github.com/Z3Prover/z3/issues/5071 Fixed
https://github.com/Z3Prover/z3/issues/5061 Fixed
https://github.com/Z3Prover/z3/issues/5047#issuecomment-785797869 Fixed
https://github.com/Z3Prover/z3/issues/5042 Dup
https://github.com/Z3Prover/z3/issues/5037 Fixed
https://github.com/Z3Prover/z3/issues/4940#issuecomment-767074891 Fixed

Solution Soundness

https://github.com/Z3Prover/z3/issues/5532#issuecomment-912608064 Fixed
https://github.com/Z3Prover/z3/issues/5429#issuecomment-885803038 Fixed
https://github.com/Z3Prover/z3/issues/5429#issuecomment-885789614 Fixed
https://github.com/Z3Prover/z3/issues/5429#issuecomment-885777533 Fixed
https://github.com/Z3Prover/z3/issues/5140#issuecomment-814049048 Fixed
https://github.com/Z3Prover/z3/issues/5140#issuecomment-829064318 Fixed
https://github.com/Z3Prover/z3/issues/5140#issuecomment-852508190 Fixed
https://github.com/Z3Prover/z3/issues/5430#issue-951879804 Fixed
https://github.com/Z3Prover/z3/issues/5445#issuecomment-890539626 Fixed
https://github.com/Z3Prover/z3/issues/5445#issuecomment-890499828 Fixed
https://github.com/Z3Prover/z3/issues/2650#issuecomment-860191020 Reported
https://github.com/Z3Prover/z3/issues/2650#issuecomment-832190983 Reported
https://github.com/Z3Prover/z3/issues/5140#issuecomment-868853515 Fixed
https://github.com/Z3Prover/z3/issues/5140#issuecomment-863925613 Won't fix
https://github.com/Z3Prover/z3/issues/5324# Fixed
https://github.com/Z3Prover/z3/issues/5324#issuecomment-852095144 Fixed
https://github.com/Z3Prover/z3/issues/5096 Fixed
[Z3Prover/Z3#5074](https://github.com/Z3Prover/z3/issues/5074) Fixed

Others

https://github.com/Z3Prover/z3/issues/5467#issuecomment-917397337 Reported
https://github.com/Z3Prover/z3/issues/5467#issuecomment-917381062 Reported
https://github.com/Z3Prover/z3/issues/5532#issuecomment-915380467 Fixed
https://github.com/Z3Prover/z3/issues/5532#issuecomment-915379582 Fixed
https://github.com/Z3Prover/z3/issues/5532#issuecomment-913215224 Fixed
https://github.com/Z3Prover/z3/issues/5532#issuecomment-913145229 Fixed
https://github.com/Z3Prover/z3/issues/5532#issuecomment-913144953 Fixed
https://github.com/Z3Prover/z3/issues/5532#issuecomment-913144733 Fixed
https://github.com/Z3Prover/z3/issues/5532#issuecomment-912989432 Fixed
https://github.com/Z3Prover/z3/issues/5532#issuecomment-912985600 Fixed
https://github.com/Z3Prover/z3/issues/5532#issuecomment-912985068 Fixed
https://github.com/Z3Prover/z3/issues/5532#issuecomment-912984265 Fixed
https://github.com/Z3Prover/z3/issues/5532#issuecomment-912982870 Fixed
https://github.com/Z3Prover/z3/issues/5532#issuecomment-912976396 Fixed
https://github.com/Z3Prover/z3/issues/5532#issuecomment-912819668 Fixed
https://github.com/Z3Prover/z3/issues/5532#issuecomment-912818844 Fixed
https://github.com/Z3Prover/z3/issues/5532#issuecomment-912741415 Fixed
https://github.com/Z3Prover/z3/issues/5532#issuecomment-912607447 Fixed
https://github.com/Z3Prover/z3/issues/5532#issuecomment-912605220 Fixed
https://github.com/Z3Prover/z3/issues/5532#issuecomment-912603798 Fixed
https://github.com/Z3Prover/z3/issues/5429#issuecomment-885805425 Fixed
https://github.com/Z3Prover/z3/issues/5429#issuecomment-885779646 Fixed
https://github.com/Z3Prover/z3/issues/5140#issuecomment-813327655 Fixed
https://github.com/Z3Prover/z3/issues/5140#issuecomment-830863108 Fixed
https://github.com/Z3Prover/z3/issues/5140#issuecomment-846593329 Fixed
https://github.com/Z3Prover/z3/issues/5140#issuecomment-856095103 Fixed
https://github.com/Z3Prover/z3/issues/5454#issuecomment-894511709 Fixed
https://github.com/Z3Prover/z3/issues/5454#issuecomment-894510946 Fixed
https://github.com/Z3Prover/z3/issues/5445# Fixed
https://github.com/Z3Prover/z3/issues/5445#issuecomment-890408110 Fixed
https://github.com/Z3Prover/z3/issues/5445#issuecomment-890407656 Fixed
https://github.com/Z3Prover/z3/issues/5445#issuecomment-890407656 Fixed
https://github.com/Z3Prover/z3/issues/5445#issuecomment-890405218 Fixed
https://github.com/Z3Prover/z3/issues/5445 Fixed
https://github.com/Z3Prover/z3/issues/5345 Reported
https://github.com/Z3Prover/z3/issues/5140#issuecomment-894508476 Fixed
https://github.com/Z3Prover/z3/issues/5140#issuecomment-886614637 Fixed
https://github.com/Z3Prover/z3/issues/5140#issuecomment-868854765 Fixed
https://github.com/Z3Prover/z3/issues/5140#issuecomment-864426711 Fixed
https://github.com/Z3Prover/z3/issues/5140#issuecomment-864401805 Fixed
https://github.com/Z3Prover/z3/issues/5140#issuecomment-864395349 Fixed
https://github.com/Z3Prover/z3/issues/5140#issuecomment-864147989 Fixed
https://github.com/Z3Prover/z3/issues/5237 Fixed
https://github.com/Z3Prover/z3/issues/5244 Won't fix
https://github.com/Z3Prover/z3/issues/5296 Fixed
https://github.com/Z3Prover/z3/issues/5345 Reported
https://github.com/Z3Prover/z3/issues/5140#issuecomment-858409317 Fixed
https://github.com/Z3Prover/z3/issues/5238 Fixed
https://github.com/Z3Prover/z3/issues/5238 Fixed
https://github.com/Z3Prover/z3/issues/5260 Fixed
https://github.com/Z3Prover/z3/issues/5260 Fixed
https://github.com/Z3Prover/z3/issues/5260 Fixed
https://github.com/Z3Prover/z3/issues/5260 Fixed
https://github.com/Z3Prover/z3/issues/5294 Fixed
https://github.com/Z3Prover/z3/issues/5296 Fixed
https://github.com/Z3Prover/z3/issues/5297 Fixed
https://github.com/Z3Prover/z3/issues/5300 Fixed
https://github.com/Z3Prover/z3/issues/5302 Won't fix
https://github.com/Z3Prover/z3/issues/5319 Won't fix
https://github.com/Z3Prover/z3/issues/5324#issuecomment-852433761 Fixed
https://github.com/Z3Prover/z3/issues/5324#issuecomment-852430150 Fixed
https://github.com/Z3Prover/z3/issues/5324#issuecomment-852426666 Fixed
https://github.com/Z3Prover/z3/issues/5324#issuecomment-852349362 Fixed
https://github.com/Z3Prover/z3/issues/5324#issuecomment-852338173 Fixed
https://github.com/Z3Prover/z3/issues/5324#issuecomment-852305173 Fixed
https://github.com/Z3Prover/z3/issues/5324#issuecomment-852303723 Fixed
https://github.com/Z3Prover/z3/issues/5324#issuecomment-852303153 Fixed
https://github.com/Z3Prover/z3/issues/5324#issuecomment-852302717 Fixed
https://github.com/Z3Prover/z3/issues/5324#issuecomment-852302306 Fixed
https://github.com/Z3Prover/z3/issues/5324#issuecomment-852301856 Fixed
https://github.com/Z3Prover/z3/issues/5324# Fixed
https://github.com/Z3Prover/z3/issues/5324#issuecomment-852096873 Fixed
https://github.com/Z3Prover/z3/issues/5324#issuecomment-852094449 Fixed
https://github.com/Z3Prover/z3/issues/5328 Fixed
https://github.com/Z3Prover/z3/issues/5223#issuecomment-829050898 Fixed
https://github.com/Z3Prover/z3/issues/5223 Fixed
https://github.com/Z3Prover/z3/issues/5223#issuecomment-829047981 Fixed
https://github.com/Z3Prover/z3/issues/5223#issuecomment-828728774 Fixed
https://github.com/Z3Prover/z3/issues/5223#issuecomment-828718973 Fixed
https://github.com/Z3Prover/z3/issues/5223#issuecomment-828685173 Fixed
https://github.com/Z3Prover/z3/issues/5223#issuecomment-828596433 Fixed
https://github.com/Z3Prover/z3/issues/5223#issuecomment-828596247 Fixed
https://github.com/Z3Prover/z3/issues/5223#issuecomment-828594023 Fixed
https://github.com/Z3Prover/z3/issues/5223#issuecomment-828591597 Fixed
https://github.com/Z3Prover/z3/issues/5223#issue-870126261 Fixed
https://github.com/Z3Prover/z3/issues/5224 Fixed
https://github.com/Z3Prover/z3/issues/5153 Fixed
https://github.com/Z3Prover/z3/issues/5140#issuecomment-813489218 Fixed
https://github.com/Z3Prover/z3/issues/5140#issuecomment-813487609 Fixed
https://github.com/Z3Prover/z3/issues/5140 Fixed
https://github.com/Z3Prover/z3/issues/5140#issuecomment-812854854 Fixed
https://github.com/Z3Prover/z3/issues/5140 Fixed
https://github.com/Z3Prover/z3/issues/5140#issuecomment-810849999 Fixed
https://github.com/Z3Prover/z3/issues/5140#issuecomment-810206643 Fixed
https://github.com/Z3Prover/z3/issues/5140 Fixed
https://github.com/Z3Prover/z3/issues/5136 Fixed
https://github.com/Z3Prover/z3/issues/5134#issuecomment-809471830 Fixed
https://github.com/Z3Prover/z3/issues/5134#issuecomment-809239927 Dup
https://github.com/Z3Prover/z3/issues/5134 Fixed
https://github.com/Z3Prover/z3/issues/5124 Won't fix
https://github.com/Z3Prover/z3/issues/5122 Won't fix
https://github.com/Z3Prover/z3/issues/5121 Fixed
https://github.com/Z3Prover/z3/issues/5087 Won't fix
https://github.com/Z3Prover/z3/issues/5080 Fixed
https://github.com/Z3Prover/z3/issues/5047 Fixed
https://github.com/Z3Prover/z3/issues/5035 Fixed
https://github.com/Z3Prover/z3/issues/4940#issuecomment-767075970 Fixed