about summary refs log tree commit diff
diff options
context:
space:
mode:
-rw-r--r--LICENSES/GPL-2.0-or-later.txt117
-rw-r--r--LICENSES/LGPL-2.1-or-later.txt176
-rw-r--r--README.md7
-rw-r--r--REUSE.toml41
-rw-r--r--loftix/deduction.scm86
-rw-r--r--loftix/emulation.scm156
-rw-r--r--loftix/fuzzing.scm201
-rw-r--r--loftix/patching.scm7
-rw-r--r--patches/e9patch-check.patch3
-rw-r--r--patches/fuzzolic-python-package.patch39
-rw-r--r--patches/fuzzolic-relax-perf-test.patch13
-rw-r--r--patches/fuzzolic-showmap.patch69
-rw-r--r--patches/fuzzolic-solver-install.patch10
-rw-r--r--patches/fuzzolic-solver-unbundle.patch598
-rw-r--r--patches/fuzzolic-test-fix-runner.patch326
-rw-r--r--patches/fuzzolic-test-skip-nondeterministic.patch23
-rw-r--r--patches/fuzzolic-timeout-solver.patch22
-rw-r--r--patches/fuzzolic-unbundle.patch108
-rw-r--r--patches/fuzzolic-utils-make.patch34
-rw-r--r--patches/fuzzy-sat-install.patch65
-rw-r--r--patches/fuzzy-sat-unbundle.patch346
-rw-r--r--patches/qemu-for-fuzzolic-static-global.patch24
-rw-r--r--patches/qemu-for-fuzzolic-test-opts-range-beyond.patch97
23 files changed, 2559 insertions, 9 deletions
diff --git a/LICENSES/GPL-2.0-or-later.txt b/LICENSES/GPL-2.0-or-later.txt
new file mode 100644
index 0000000..17cb286
--- /dev/null
+++ b/LICENSES/GPL-2.0-or-later.txt
@@ -0,0 +1,117 @@
+GNU GENERAL PUBLIC LICENSE
+Version 2, June 1991
+
+Copyright (C) 1989, 1991 Free Software Foundation, Inc.
+51 Franklin Street, Fifth Floor, Boston, MA  02110-1301, USA
+
+Everyone is permitted to copy and distribute verbatim copies of this license document, but changing it is not allowed.
+
+Preamble
+
+The licenses for most software are designed to take away your freedom to share and change it. By contrast, the GNU General Public License is intended to guarantee your freedom to share and change free software--to make sure the software is free for all its users. This General Public License applies to most of the Free Software Foundation's software and to any other program whose authors commit to using it. (Some other Free Software Foundation software is covered by the GNU Lesser General Public License instead.) You can apply it to your programs, too.
+
+When we speak of free software, we are referring to freedom, not price. Our General Public Licenses are designed to make sure that you have the freedom to distribute copies of free software (and charge for this service if you wish), that you receive source code or can get it if you want it, that you can change the software or use pieces of it in new free programs; and that you know you can do these things.
+
+To protect your rights, we need to make restrictions that forbid anyone to deny you these rights or to ask you to surrender the rights. These restrictions translate to certain responsibilities for you if you distribute copies of the software, or if you modify it.
+
+For example, if you distribute copies of such a program, whether gratis or for a fee, you must give the recipients all the rights that you have. You must make sure that they, too, receive or can get the source code. And you must show them these terms so they know their rights.
+
+We protect your rights with two steps: (1) copyright the software, and (2) offer you this license which gives you legal permission to copy, distribute and/or modify the software.
+
+Also, for each author's protection and ours, we want to make certain that everyone understands that there is no warranty for this free software. If the software is modified by someone else and passed on, we want its recipients to know that what they have is not the original, so that any problems introduced by others will not reflect on the original authors' reputations.
+
+Finally, any free program is threatened constantly by software patents. We wish to avoid the danger that redistributors of a free program will individually obtain patent licenses, in effect making the program proprietary. To prevent this, we have made it clear that any patent must be licensed for everyone's free use or not licensed at all.
+
+The precise terms and conditions for copying, distribution and modification follow.
+
+TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION
+
+0. This License applies to any program or other work which contains a notice placed by the copyright holder saying it may be distributed under the terms of this General Public License. The "Program", below, refers to any such program or work, and a "work based on the Program" means either the Program or any derivative work under copyright law: that is to say, a work containing the Program or a portion of it, either verbatim or with modifications and/or translated into another language. (Hereinafter, translation is included without limitation in the term "modification".) Each licensee is addressed as "you".
+
+Activities other than copying, distribution and modification are not covered by this License; they are outside its scope. The act of running the Program is not restricted, and the output from the Program is covered only if its contents constitute a work based on the Program (independent of having been made by running the Program). Whether that is true depends on what the Program does.
+
+1. You may copy and distribute verbatim copies of the Program's source code as you receive it, in any medium, provided that you conspicuously and appropriately publish on each copy an appropriate copyright notice and disclaimer of warranty; keep intact all the notices that refer to this License and to the absence of any warranty; and give any other recipients of the Program a copy of this License along with the Program.
+
+You may charge a fee for the physical act of transferring a copy, and you may at your option offer warranty protection in exchange for a fee.
+
+2. You may modify your copy or copies of the Program or any portion of it, thus forming a work based on the Program, and copy and distribute such modifications or work under the terms of Section 1 above, provided that you also meet all of these conditions:
+
+     a) You must cause the modified files to carry prominent notices stating that you changed the files and the date of any change.
+
+     b) You must cause any work that you distribute or publish, that in whole or in part contains or is derived from the Program or any part thereof, to be licensed as a whole at no charge to all third parties under the terms of this License.
+
+     c) If the modified program normally reads commands interactively when run, you must cause it, when started running for such interactive use in the most ordinary way, to print or display an announcement including an appropriate copyright notice and a notice that there is no warranty (or else, saying that you provide a warranty) and that users may redistribute the program under these conditions, and telling the user how to view a copy of this License. (Exception: if the Program itself is interactive but does not normally print such an announcement, your work based on the Program is not required to print an announcement.)
+
+These requirements apply to the modified work as a whole. If identifiable sections of that work are not derived from the Program, and can be reasonably considered independent and separate works in themselves, then this License, and its terms, do not apply to those sections when you distribute them as separate works. But when you distribute the same sections as part of a whole which is a work based on the Program, the distribution of the whole must be on the terms of this License, whose permissions for other licensees extend to the entire whole, and thus to each and every part regardless of who wrote it.
+
+Thus, it is not the intent of this section to claim rights or contest your rights to work written entirely by you; rather, the intent is to exercise the right to control the distribution of derivative or collective works based on the Program.
+
+In addition, mere aggregation of another work not based on the Program with the Program (or with a work based on the Program) on a volume of a storage or distribution medium does not bring the other work under the scope of this License.
+
+3. You may copy and distribute the Program (or a work based on it, under Section 2) in object code or executable form under the terms of Sections 1 and 2 above provided that you also do one of the following:
+
+     a) Accompany it with the complete corresponding machine-readable source code, which must be distributed under the terms of Sections 1 and 2 above on a medium customarily used for software interchange; or,
+
+     b) Accompany it with a written offer, valid for at least three years, to give any third party, for a charge no more than your cost of physically performing source distribution, a complete machine-readable copy of the corresponding source code, to be distributed under the terms of Sections 1 and 2 above on a medium customarily used for software interchange; or,
+
+     c) Accompany it with the information you received as to the offer to distribute corresponding source code. (This alternative is allowed only for noncommercial distribution and only if you received the program in object code or executable form with such an offer, in accord with Subsection b above.)
+
+The source code for a work means the preferred form of the work for making modifications to it. For an executable work, complete source code means all the source code for all modules it contains, plus any associated interface definition files, plus the scripts used to control compilation and installation of the executable. However, as a special exception, the source code distributed need not include anything that is normally distributed (in either source or binary form) with the major components (compiler, kernel, and so on) of the operating system on which the executable runs, unless that component itself accompanies the executable.
+
+If distribution of executable or object code is made by offering access to copy from a designated place, then offering equivalent access to copy the source code from the same place counts as distribution of the source code, even though third parties are not compelled to copy the source along with the object code.
+
+4. You may not copy, modify, sublicense, or distribute the Program except as expressly provided under this License. Any attempt otherwise to copy, modify, sublicense or distribute the Program is void, and will automatically terminate your rights under this License. However, parties who have received copies, or rights, from you under this License will not have their licenses terminated so long as such parties remain in full compliance.
+
+5. You are not required to accept this License, since you have not signed it. However, nothing else grants you permission to modify or distribute the Program or its derivative works. These actions are prohibited by law if you do not accept this License. Therefore, by modifying or distributing the Program (or any work based on the Program), you indicate your acceptance of this License to do so, and all its terms and conditions for copying, distributing or modifying the Program or works based on it.
+
+6. Each time you redistribute the Program (or any work based on the Program), the recipient automatically receives a license from the original licensor to copy, distribute or modify the Program subject to these terms and conditions. You may not impose any further restrictions on the recipients' exercise of the rights granted herein. You are not responsible for enforcing compliance by third parties to this License.
+
+7. If, as a consequence of a court judgment or allegation of patent infringement or for any other reason (not limited to patent issues), conditions are imposed on you (whether by court order, agreement or otherwise) that contradict the conditions of this License, they do not excuse you from the conditions of this License. If you cannot distribute so as to satisfy simultaneously your obligations under this License and any other pertinent obligations, then as a consequence you may not distribute the Program at all. For example, if a patent license would not permit royalty-free redistribution of the Program by all those who receive copies directly or indirectly through you, then the only way you could satisfy both it and this License would be to refrain entirely from distribution of the Program.
+
+If any portion of this section is held invalid or unenforceable under any particular circumstance, the balance of the section is intended to apply and the section as a whole is intended to apply in other circumstances.
+
+It is not the purpose of this section to induce you to infringe any patents or other property right claims or to contest validity of any such claims; this section has the sole purpose of protecting the integrity of the free software distribution system, which is implemented by public license practices. Many people have made generous contributions to the wide range of software distributed through that system in reliance on consistent application of that system; it is up to the author/donor to decide if he or she is willing to distribute software through any other system and a licensee cannot impose that choice.
+
+This section is intended to make thoroughly clear what is believed to be a consequence of the rest of this License.
+
+8. If the distribution and/or use of the Program is restricted in certain countries either by patents or by copyrighted interfaces, the original copyright holder who places the Program under this License may add an explicit geographical distribution limitation excluding those countries, so that distribution is permitted only in or among countries not thus excluded. In such case, this License incorporates the limitation as if written in the body of this License.
+
+9. The Free Software Foundation may publish revised and/or new versions of the General Public License from time to time. Such new versions will be similar in spirit to the present version, but may differ in detail to address new problems or concerns.
+
+Each version is given a distinguishing version number. If the Program specifies a version number of this License which applies to it and "any later version", you have the option of following the terms and conditions either of that version or of any later version published by the Free Software Foundation. If the Program does not specify a version number of this License, you may choose any version ever published by the Free Software Foundation.
+
+10. If you wish to incorporate parts of the Program into other free programs whose distribution conditions are different, write to the author to ask for permission. For software which is copyrighted by the Free Software Foundation, write to the Free Software Foundation; we sometimes make exceptions for this. Our decision will be guided by the two goals of preserving the free status of all derivatives of our free software and of promoting the sharing and reuse of software generally.
+
+NO WARRANTY
+
+11. BECAUSE THE PROGRAM IS LICENSED FREE OF CHARGE, THERE IS NO WARRANTY FOR THE PROGRAM, TO THE EXTENT PERMITTED BY APPLICABLE LAW. EXCEPT WHEN OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND/OR OTHER PARTIES PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESSED OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE PROGRAM IS WITH YOU. SHOULD THE PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF ALL NECESSARY SERVICING, REPAIR OR CORRECTION.
+
+12. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY MODIFY AND/OR REDISTRIBUTE THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES, INCLUDING ANY GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER PROGRAMS), EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGES.
+
+END OF TERMS AND CONDITIONS
+
+How to Apply These Terms to Your New Programs
+
+If you develop a new program, and you want it to be of the greatest possible use to the public, the best way to achieve this is to make it free software which everyone can redistribute and change under these terms.
+
+To do so, attach the following notices to the program. It is safest to attach them to the start of each source file to most effectively convey the exclusion of warranty; and each file should have at least the "copyright" line and a pointer to where the full notice is found.
+
+     one line to give the program's name and an idea of what it does. Copyright (C) yyyy name of author
+
+     This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version.
+
+     This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details.
+
+     You should have received a copy of the GNU General Public License along with this program; if not, write to the Free Software Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301, USA. Also add information on how to contact you by electronic and paper mail.
+
+If the program is interactive, make it output a short notice like this when it starts in an interactive mode:
+
+     Gnomovision version 69, Copyright (C) year name of author Gnomovision comes with ABSOLUTELY NO WARRANTY; for details type `show w'. This is free software, and you are welcome to redistribute it under certain conditions; type `show c' for details.
+
+The hypothetical commands `show w' and `show c' should show the appropriate parts of the General Public License. Of course, the commands you use may be called something other than `show w' and `show c'; they could even be mouse-clicks or menu items--whatever suits your program.
+
+You should also get your employer (if you work as a programmer) or your school, if any, to sign a "copyright disclaimer" for the program, if necessary. Here is a sample; alter the names:
+
+     Yoyodyne, Inc., hereby disclaims all copyright interest in the program `Gnomovision' (which makes passes at compilers) written by James Hacker.
+
+signature of Ty Coon, 1 April 1989 Ty Coon, President of Vice
diff --git a/LICENSES/LGPL-2.1-or-later.txt b/LICENSES/LGPL-2.1-or-later.txt
new file mode 100644
index 0000000..c6487f4
--- /dev/null
+++ b/LICENSES/LGPL-2.1-or-later.txt
@@ -0,0 +1,176 @@
+GNU LESSER GENERAL PUBLIC LICENSE
+
+Version 2.1, February 1999
+
+Copyright (C) 1991, 1999 Free Software Foundation, Inc.
+51 Franklin Street, Fifth Floor, Boston, MA  02110-1301  USA
+
+Everyone is permitted to copy and distribute verbatim copies of this license document, but changing it is not allowed.
+
+[This is the first released version of the Lesser GPL.  It also counts as the successor of the GNU Library Public License, version 2, hence the version number 2.1.]
+
+Preamble
+
+The licenses for most software are designed to take away your freedom to share and change it. By contrast, the GNU General Public Licenses are intended to guarantee your freedom to share and change free software--to make sure the software is free for all its users.
+
+This license, the Lesser General Public License, applies to some specially designated software packages--typically libraries--of the Free Software Foundation and other authors who decide to use it. You can use it too, but we suggest you first think carefully about whether this license or the ordinary General Public License is the better strategy to use in any particular case, based on the explanations below.
+
+When we speak of free software, we are referring to freedom of use, not price. Our General Public Licenses are designed to make sure that you have the freedom to distribute copies of free software (and charge for this service if you wish); that you receive source code or can get it if you want it; that you can change the software and use pieces of it in new free programs; and that you are informed that you can do these things.
+
+To protect your rights, we need to make restrictions that forbid distributors to deny you these rights or to ask you to surrender these rights. These restrictions translate to certain responsibilities for you if you distribute copies of the library or if you modify it.
+
+For example, if you distribute copies of the library, whether gratis or for a fee, you must give the recipients all the rights that we gave you. You must make sure that they, too, receive or can get the source code. If you link other code with the library, you must provide complete object files to the recipients, so that they can relink them with the library after making changes to the library and recompiling it. And you must show them these terms so they know their rights.
+
+We protect your rights with a two-step method: (1) we copyright the library, and (2) we offer you this license, which gives you legal permission to copy, distribute and/or modify the library.
+
+To protect each distributor, we want to make it very clear that there is no warranty for the free library. Also, if the library is modified by someone else and passed on, the recipients should know that what they have is not the original version, so that the original author's reputation will not be affected by problems that might be introduced by others.
+
+Finally, software patents pose a constant threat to the existence of any free program. We wish to make sure that a company cannot effectively restrict the users of a free program by obtaining a restrictive license from a patent holder. Therefore, we insist that any patent license obtained for a version of the library must be consistent with the full freedom of use specified in this license.
+
+Most GNU software, including some libraries, is covered by the ordinary GNU General Public License. This license, the GNU Lesser General Public License, applies to certain designated libraries, and is quite different from the ordinary General Public License. We use this license for certain libraries in order to permit linking those libraries into non-free programs.
+
+When a program is linked with a library, whether statically or using a shared library, the combination of the two is legally speaking a combined work, a derivative of the original library. The ordinary General Public License therefore permits such linking only if the entire combination fits its criteria of freedom. The Lesser General Public License permits more lax criteria for linking other code with the library.
+
+We call this license the "Lesser" General Public License because it does Less to protect the user's freedom than the ordinary General Public License. It also provides other free software developers Less of an advantage over competing non-free programs. These disadvantages are the reason we use the ordinary General Public License for many libraries. However, the Lesser license provides advantages in certain special circumstances.
+
+For example, on rare occasions, there may be a special need to encourage the widest possible use of a certain library, so that it becomes a de-facto standard. To achieve this, non-free programs must be allowed to use the library. A more frequent case is that a free library does the same job as widely used non-free libraries. In this case, there is little to gain by limiting the free library to free software only, so we use the Lesser General Public License.
+
+In other cases, permission to use a particular library in non-free programs enables a greater number of people to use a large body of free software. For example, permission to use the GNU C Library in non-free programs enables many more people to use the whole GNU operating system, as well as its variant, the GNU/Linux operating system.
+
+Although the Lesser General Public License is Less protective of the users' freedom, it does ensure that the user of a program that is linked with the Library has the freedom and the wherewithal to run that program using a modified version of the Library.
+
+The precise terms and conditions for copying, distribution and modification follow. Pay close attention to the difference between a "work based on the library" and a "work that uses the library". The former contains code derived from the library, whereas the latter must be combined with the library in order to run.
+
+GNU LESSER GENERAL PUBLIC LICENSE
+TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION
+
+0. This License Agreement applies to any software library or other program which contains a notice placed by the copyright holder or other authorized party saying it may be distributed under the terms of this Lesser General Public License (also called "this License"). Each licensee is addressed as "you".
+
+A "library" means a collection of software functions and/or data prepared so as to be conveniently linked with application programs (which use some of those functions and data) to form executables.
+
+The "Library", below, refers to any such software library or work which has been distributed under these terms. A "work based on the Library" means either the Library or any derivative work under copyright law: that is to say, a work containing the Library or a portion of it, either verbatim or with modifications and/or translated straightforwardly into another language. (Hereinafter, translation is included without limitation in the term "modification".)
+
+"Source code" for a work means the preferred form of the work for making modifications to it. For a library, complete source code means all the source code for all modules it contains, plus any associated interface definition files, plus the scripts used to control compilation and installation of the library.
+
+Activities other than copying, distribution and modification are not covered by this License; they are outside its scope. The act of running a program using the Library is not restricted, and output from such a program is covered only if its contents constitute a work based on the Library (independent of the use of the Library in a tool for writing it). Whether that is true depends on what the Library does and what the program that uses the Library does.
+
+1. You may copy and distribute verbatim copies of the Library's complete source code as you receive it, in any medium, provided that you conspicuously and appropriately publish on each copy an appropriate copyright notice and disclaimer of warranty; keep intact all the notices that refer to this License and to the absence of any warranty; and distribute a copy of this License along with the Library.
+
+You may charge a fee for the physical act of transferring a copy, and you may at your option offer warranty protection in exchange for a fee.
+
+2. You may modify your copy or copies of the Library or any portion of it, thus forming a work based on the Library, and copy and distribute such modifications or work under the terms of Section 1 above, provided that you also meet all of these conditions:
+
+     a) The modified work must itself be a software library.
+
+     b) You must cause the files modified to carry prominent notices stating that you changed the files and the date of any change.
+
+     c) You must cause the whole of the work to be licensed at no charge to all third parties under the terms of this License.
+
+     d) If a facility in the modified Library refers to a function or a table of data to be supplied by an application program that uses the facility, other than as an argument passed when the facility is invoked, then you must make a good faith effort to ensure that, in the event an application does not supply such function or table, the facility still operates, and performs whatever part of its purpose remains meaningful.
+
+(For example, a function in a library to compute square roots has a purpose that is entirely well-defined independent of the application. Therefore, Subsection 2d requires that any application-supplied function or table used by this function must be optional: if the application does not supply it, the square root function must still compute square roots.)
+
+These requirements apply to the modified work as a whole. If identifiable sections of that work are not derived from the Library, and can be reasonably considered independent and separate works in themselves, then this License, and its terms, do not apply to those sections when you distribute them as separate works. But when you distribute the same sections as part of a whole which is a work based on the Library, the distribution of the whole must be on the terms of this License, whose permissions for other licensees extend to the entire whole, and thus to each and every part regardless of who wrote it.
+
+Thus, it is not the intent of this section to claim rights or contest your rights to work written entirely by you; rather, the intent is to exercise the right to control the distribution of derivative or collective works based on the Library.
+
+In addition, mere aggregation of another work not based on the Library with the Library (or with a work based on the Library) on a volume of a storage or distribution medium does not bring the other work under the scope of this License.
+
+3. You may opt to apply the terms of the ordinary GNU General Public License instead of this License to a given copy of the Library. To do this, you must alter all the notices that refer to this License, so that they refer to the ordinary GNU General Public License, version 2, instead of to this License. (If a newer version than version 2 of the ordinary GNU General Public License has appeared, then you can specify that version instead if you wish.) Do not make any other change in these notices.
+
+Once this change is made in a given copy, it is irreversible for that copy, so the ordinary GNU General Public License applies to all subsequent copies and derivative works made from that copy.
+
+This option is useful when you wish to copy part of the code of the Library into a program that is not a library.
+
+4. You may copy and distribute the Library (or a portion or derivative of it, under Section 2) in object code or executable form under the terms of Sections 1 and 2 above provided that you accompany it with the complete corresponding machine-readable source code, which must be distributed under the terms of Sections 1 and 2 above on a medium customarily used for software interchange.
+
+If distribution of object code is made by offering access to copy from a designated place, then offering equivalent access to copy the source code from the same place satisfies the requirement to distribute the source code, even though third parties are not compelled to copy the source along with the object code.
+
+5. A program that contains no derivative of any portion of the Library, but is designed to work with the Library by being compiled or linked with it, is called a "work that uses the Library". Such a work, in isolation, is not a derivative work of the Library, and therefore falls outside the scope of this License.
+
+However, linking a "work that uses the Library" with the Library creates an executable that is a derivative of the Library (because it contains portions of the Library), rather than a "work that uses the library". The executable is therefore covered by this License. Section 6 states terms for distribution of such executables.
+
+When a "work that uses the Library" uses material from a header file that is part of the Library, the object code for the work may be a derivative work of the Library even though the source code is not. Whether this is true is especially significant if the work can be linked without the Library, or if the work is itself a library. The threshold for this to be true is not precisely defined by law.
+
+If such an object file uses only numerical parameters, data structure layouts and accessors, and small macros and small inline functions (ten lines or less in length), then the use of the object file is unrestricted, regardless of whether it is legally a derivative work. (Executables containing this object code plus portions of the Library will still fall under Section 6.)
+
+Otherwise, if the work is a derivative of the Library, you may distribute the object code for the work under the terms of Section 6. Any executables containing that work also fall under Section 6, whether or not they are linked directly with the Library itself.
+
+6. As an exception to the Sections above, you may also combine or link a "work that uses the Library" with the Library to produce a work containing portions of the Library, and distribute that work under terms of your choice, provided that the terms permit modification of the work for the customer's own use and reverse engineering for debugging such modifications.
+
+You must give prominent notice with each copy of the work that the Library is used in it and that the Library and its use are covered by this License. You must supply a copy of this License. If the work during execution displays copyright notices, you must include the copyright notice for the Library among them, as well as a reference directing the user to the copy of this License. Also, you must do one of these things:
+
+     a) Accompany the work with the complete corresponding machine-readable source code for the Library including whatever changes were used in the work (which must be distributed under Sections 1 and 2 above); and, if the work is an executable linked with the Library, with the complete machine-readable "work that uses the Library", as object code and/or source code, so that the user can modify the Library and then relink to produce a modified executable containing the modified Library. (It is understood that the user who changes the contents of definitions files in the Library will not necessarily be able to recompile the application to use the modified definitions.)
+
+     b) Use a suitable shared library mechanism for linking with the Library. A suitable mechanism is one that (1) uses at run time a copy of the library already present on the user's computer system, rather than copying library functions into the executable, and (2) will operate properly with a modified version of the library, if the user installs one, as long as the modified version is interface-compatible with the version that the work was made with.
+
+     c) Accompany the work with a written offer, valid for at least three years, to give the same user the materials specified in Subsection 6a, above, for a charge no more than the cost of performing this distribution.
+
+     d) If distribution of the work is made by offering access to copy from a designated place, offer equivalent access to copy the above specified materials from the same place.
+
+     e) Verify that the user has already received a copy of these materials or that you have already sent this user a copy.
+
+For an executable, the required form of the "work that uses the Library" must include any data and utility programs needed for reproducing the executable from it. However, as a special exception, the materials to be distributed need not include anything that is normally distributed (in either source or binary form) with the major components (compiler, kernel, and so on) of the operating system on which the executable runs, unless that component itself accompanies the executable.
+
+It may happen that this requirement contradicts the license restrictions of other proprietary libraries that do not normally accompany the operating system. Such a contradiction means you cannot use both them and the Library together in an executable that you distribute.
+
+7. You may place library facilities that are a work based on the Library side-by-side in a single library together with other library facilities not covered by this License, and distribute such a combined library, provided that the separate distribution of the work based on the Library and of the other library facilities is otherwise permitted, and provided that you do these two things:
+
+     a) Accompany the combined library with a copy of the same work based on the Library, uncombined with any other library facilities. This must be distributed under the terms of the Sections above.
+
+     b) Give prominent notice with the combined library of the fact that part of it is a work based on the Library, and explaining where to find the accompanying uncombined form of the same work.
+
+8. You may not copy, modify, sublicense, link with, or distribute the Library except as expressly provided under this License. Any attempt otherwise to copy, modify, sublicense, link with, or distribute the Library is void, and will automatically terminate your rights under this License. However, parties who have received copies, or rights, from you under this License will not have their licenses terminated so long as such parties remain in full compliance.
+
+9. You are not required to accept this License, since you have not signed it. However, nothing else grants you permission to modify or distribute the Library or its derivative works. These actions are prohibited by law if you do not accept this License. Therefore, by modifying or distributing the Library (or any work based on the Library), you indicate your acceptance of this License to do so, and all its terms and conditions for copying, distributing or modifying the Library or works based on it.
+
+10. Each time you redistribute the Library (or any work based on the Library), the recipient automatically receives a license from the original licensor to copy, distribute, link with or modify the Library subject to these terms and conditions. You may not impose any further restrictions on the recipients' exercise of the rights granted herein. You are not responsible for enforcing compliance by third parties with this License.
+
+11. If, as a consequence of a court judgment or allegation of patent infringement or for any other reason (not limited to patent issues), conditions are imposed on you (whether by court order, agreement or otherwise) that contradict the conditions of this License, they do not excuse you from the conditions of this License. If you cannot distribute so as to satisfy simultaneously your obligations under this License and any other pertinent obligations, then as a consequence you may not distribute the Library at all. For example, if a patent license would not permit royalty-free redistribution of the Library by all those who receive copies directly or indirectly through you, then the only way you could satisfy both it and this License would be to refrain entirely from distribution of the Library.
+
+If any portion of this section is held invalid or unenforceable under any particular circumstance, the balance of the section is intended to apply, and the section as a whole is intended to apply in other circumstances.
+
+It is not the purpose of this section to induce you to infringe any patents or other property right claims or to contest validity of any such claims; this section has the sole purpose of protecting the integrity of the free software distribution system which is implemented by public license practices. Many people have made generous contributions to the wide range of software distributed through that system in reliance on consistent application of that system; it is up to the author/donor to decide if he or she is willing to distribute software through any other system and a licensee cannot impose that choice.
+
+This section is intended to make thoroughly clear what is believed to be a consequence of the rest of this License.
+
+12. If the distribution and/or use of the Library is restricted in certain countries either by patents or by copyrighted interfaces, the original copyright holder who places the Library under this License may add an explicit geographical distribution limitation excluding those countries, so that distribution is permitted only in or among countries not thus excluded. In such case, this License incorporates the limitation as if written in the body of this License.
+
+13. The Free Software Foundation may publish revised and/or new versions of the Lesser General Public License from time to time. Such new versions will be similar in spirit to the present version, but may differ in detail to address new problems or concerns.
+
+Each version is given a distinguishing version number. If the Library specifies a version number of this License which applies to it and "any later version", you have the option of following the terms and conditions either of that version or of any later version published by the Free Software Foundation. If the Library does not specify a license version number, you may choose any version ever published by the Free Software Foundation.
+
+14. If you wish to incorporate parts of the Library into other free programs whose distribution conditions are incompatible with these, write to the author to ask for permission. For software which is copyrighted by the Free Software Foundation, write to the Free Software Foundation; we sometimes make exceptions for this. Our decision will be guided by the two goals of preserving the free status of all derivatives of our free software and of promoting the sharing and reuse of software generally.
+
+NO WARRANTY
+
+15. BECAUSE THE LIBRARY IS LICENSED FREE OF CHARGE, THERE IS NO WARRANTY FOR THE LIBRARY, TO THE EXTENT PERMITTED BY APPLICABLE LAW. EXCEPT WHEN OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND/OR OTHER PARTIES PROVIDE THE LIBRARY "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESSED OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE LIBRARY IS WITH YOU. SHOULD THE LIBRARY PROVE DEFECTIVE, YOU ASSUME THE COST OF ALL NECESSARY SERVICING, REPAIR OR CORRECTION.
+
+16. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY MODIFY AND/OR REDISTRIBUTE THE LIBRARY AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES, INCLUDING ANY GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OR INABILITY TO USE THE LIBRARY (INCLUDING BUT NOT LIMITED TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD PARTIES OR A FAILURE OF THE LIBRARY TO OPERATE WITH ANY OTHER SOFTWARE), EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGES.
+
+END OF TERMS AND CONDITIONS
+
+How to Apply These Terms to Your New Libraries
+
+If you develop a new library, and you want it to be of the greatest possible use to the public, we recommend making it free software that everyone can redistribute and change. You can do so by permitting redistribution under these terms (or, alternatively, under the terms of the ordinary General Public License).
+
+To apply these terms, attach the following notices to the library. It is safest to attach them to the start of each source file to most effectively convey the exclusion of warranty; and each file should have at least the "copyright" line and a pointer to where the full notice is found.
+
+     one line to give the library's name and an idea of what it does.
+     Copyright (C) year  name of author
+
+     This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 2.1 of the License, or (at your option) any later version.
+
+     This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU Lesser General Public License for more details.
+
+     You should have received a copy of the GNU Lesser General Public License along with this library; if not, write to the Free Software Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301  USA Also add information on how to contact you by electronic and paper mail.
+
+You should also get your employer (if you work as a programmer) or your school, if any, to sign a "copyright disclaimer" for the library, if necessary. Here is a sample; alter the names:
+
+Yoyodyne, Inc., hereby disclaims all copyright interest in
+the library `Frob' (a library for tweaking knobs) written
+by James Random Hacker.
+
+signature of Ty Coon, 1 April 1990
+Ty Coon, President of Vice
+That's all there is to it!
diff --git a/README.md b/README.md
index eb35d2e..6d36a61 100644
--- a/README.md
+++ b/README.md
@@ -26,6 +26,7 @@ Then run `guix pull`.
 
 - [afl-dyninst]: [Dyninst] integration for [AFL++]
 - [evocatio]: Bug analyzer for bug capability discovery
+- [fuzzolic]: Concolic fuzzer
 
 ### Patching
 
@@ -36,11 +37,17 @@ Then run `guix pull`.
 - [python-pacfix]: PAC-learning-based program synthesizer
 - [taosc]: Makeshift binary patch generator
 
+### Theorem Proving
+
+- [fuzzy-sat]: Approximate solver for concolic execution
+
 [Guix channel]: https://guix.gnu.org/manual/devel/en/html_node/Channels.html
 [afl-dyninst]: https://trong.loang.net/~cnx/afl-dyninst/about
 [Dyninst]: https://github.com/dyninst/dyninst
 [AFL++]: https://aflplus.plus
 [evocatio]: https://github.com/HexHive/Evocatio
+[fuzzolic]: https://season-lab.github.io/fuzzolic
 [e9patch]: https://github.com/GJDuck/e9patch
 [python-pacfix]: https://github.com/hsh814/pacfix-python
 [taosc]: https://trong.loang.net/~cnx/taosc/about
+[fuzzy-sat]: https://github.com/season-lab/fuzzy-sat
diff --git a/REUSE.toml b/REUSE.toml
index 99e95fe..f2e2c5d 100644
--- a/REUSE.toml
+++ b/REUSE.toml
@@ -8,18 +8,22 @@ SPDX-License-Identifier = 'CC0-1.0'
 [[annotations]]
 path = 'bugs/cve/2012/2806/cnode0006-heap-buffer-overflow-796.jpg'
 SPDX-FileCopyrightText = 'Chris Evans'
+SPDX-License-Identifier = 'CC0-1.0'
 
 [[annotations]]
 path = 'bugs/cve/2012/5134/bad.xml'
-SPDX-FileCopyrightText = 'Jueri Aedla'
+SPDX-FileCopyrightText = 'Jüri Aedla'
+SPDX-License-Identifier = 'CC0-1.0'
 
 [[annotations]]
 path = 'bugs/cve/2013/7437/1.bmp'
 SPDX-FileCopyrightText = 'Murray McAllister'
+SPDX-License-Identifier = 'CC0-1.0'
 
 [[annotations]]
 path = 'bugs/cve/2013/7437/2.bmp'
 SPDX-FileCopyrightText = 'Stefan Cornelius'
+SPDX-License-Identifier = 'CC0-1.0'
 
 [[annotations]]
 path = 'bugs/cve/2014/8128/03_thumbnail.tiff'
@@ -35,6 +39,7 @@ SPDX-License-Identifier = 'CC0-1.0'
 [[annotations]]
 path = 'bugs/cve/2016/3186/crash.gif'
 SPDX-FileCopyrightText = 'Aladdin Mubaied'
+SPDX-License-Identifier = 'CC0-1.0'
 
 [[annotations]]
 path = 'bugs/cve/2016/5844/libarchive-signed-int-overflow.iso'
@@ -103,10 +108,12 @@ SPDX-License-Identifier = 'CC0-1.0'
 path = [ 'bugs/cve/2017/14745/crash_1',
          'bugs/cve/2017/15025/floatexception.elf' ]
 SPDX-FileCopyrightText = 'Junchao Luan'
+SPDX-License-Identifier = 'CC0-1.0'
 
 [[annotations]]
 path = 'bugs/cve/2017/15232/*.jpg'
 SPDX-FileCopyrightText = 'Zhao Liang'
+SPDX-License-Identifier = 'CC0-1.0'
 
 [[annotations]]
 path = 'bugs/cve/2018/8806/heap-use-after-free.swf'
@@ -121,6 +128,7 @@ SPDX-License-Identifier = 'CC0-1.0'
 [[annotations]]
 path = 'bugs/cve/2018/14498/*.bmp'
 SPDX-FileCopyrightText = 'Hongxu Chen'
+SPDX-License-Identifier = 'CC0-1.0'
 
 [[annotations]]
 path = 'bugs/cve/2018/19664/heap-buffer-overflow-2.jpg'
@@ -147,7 +155,19 @@ SPDX-License-Identifier = 'CC0-1.0'
 path = [ 'patches/afl++-*.patch',
          'patches/e9patch-*.patch',
          'patches/evocatio-*.patch',
-         'patches/jasper-no-define-int-types.patch' ]
+         'patches/fuzzy-sat-*.patch',
+         'patches/fuzzolic-install.patch',
+         'patches/fuzzolic-python-package.patch',
+         'patches/fuzzolic-relax-perf-test.patch',
+         'patches/fuzzolic-solver-install.patch',
+         'patches/fuzzolic-solver-unbundle.patch',
+         'patches/fuzzolic-test-driver-include-libc.patch',
+         'patches/fuzzolic-test-fix-runner.patch',
+         'patches/fuzzolic-test-skip-nondeterministic.patch',
+         'patches/fuzzolic-unbundle.patch',
+         'patches/fuzzolic-utils-make.patch',
+         'patches/jasper-no-define-int-types.patch',
+         'patches/qemu-for-fuzzolic-static-global.patch' ]
 SPDX-FileCopyrightText = 'Nguyễn Gia Phong'
 SPDX-License-Identifier = 'GPL-3.0-or-later'
 
@@ -163,12 +183,29 @@ SPDX-FileCopyrightText = 'Paul Eggert'
 SPDX-License-Identifier = 'GPL-3.0-or-later'
 
 [[annotations]]
+path = 'patches/fuzzolic-showmap.patch'
+SPDX-FileCopyrightText = 'Emilio Coppa'
+SPDX-License-Identifier = 'GPL-2.0-or-later'
+
+
+[[annotations]]
+path = 'patches/fuzzolic-timeout-solver.patch'
+SPDX-FileCopyrightText = 'Andrew Haberlandt'
+SPDX-License-Identifier = 'GPL-2.0-or-later'
+
+[[annotations]]
 # https://src.fedoraproject.org/rpms/ming/c/c6f24aedb4f66c5b3167b75bebc55b14fd6b5248
 path = 'patches/libming-parallel-make.patch'
 SPDX-FileCopyrightText = 'Dominik Mierzejewski'
 SPDX-License-Identifier = 'MIT'
 
 [[annotations]]
+# https://lists.nongnu.org/archive/html/qemu-devel/2019-09/msg05403.html
+path = 'patches/qemu-for-fuzzolic-test-opts-range-beyond.patch'
+SPDX-FileCopyrightText = 'Andrey Shinkevich'
+SPDX-License-Identifier = 'LGPL-2.1-or-later'
+
+[[annotations]]
 path = '**/README.md'
 SPDX-FileCopyrightText = 'None'
 SPDX-License-Identifier = 'CC0-1.0'
diff --git a/loftix/deduction.scm b/loftix/deduction.scm
new file mode 100644
index 0000000..dd84df2
--- /dev/null
+++ b/loftix/deduction.scm
@@ -0,0 +1,86 @@
+;;; Packages for theorem provers
+;;;
+;;; SPDX-FileCopyrightText: 2025 Nguyễn Gia Phong
+;;; SPDX-License-Identifier: GPL-3.0-or-later
+
+(define-module (loftix deduction)
+  #:use-module (gnu packages)
+  #:use-module (gnu packages check)
+  #:use-module (gnu packages digest)
+  #:use-module (gnu packages maths)
+  #:use-module (gnu packages pkg-config)
+  #:use-module (guix build-system cmake)
+  #:use-module (guix build-system pyproject)
+  #:use-module (guix download)
+  #:use-module (guix gexp)
+  #:use-module (guix git-download)
+  #:use-module ((guix licenses) #:prefix license:)
+  #:use-module (guix packages))
+
+(define-public z3-for-fuzzolic
+  (let* ((base z3)
+         (base-version "4.14.1")
+         (base-tag (string-append "z3-" base-version))
+         (revision "fuzzolic")
+         (commit "268d10d0d99083a18cde2d615e0f9de82d7b201d")
+         (upstream "https://github.com/Z3Prover/z3"))
+    (hidden-package
+     (package
+       (inherit base)
+       (name "z3-for-fuzzolic")
+       (version (git-version base-version revision commit))
+       (source
+        (origin
+          (inherit (package-source base))
+          (uri (git-reference (url upstream)
+                              (commit base-tag)))
+          (file-name (git-file-name name version))
+          (sha256
+           (base32 "1gdknrqnnigfh1h833ks3vbrp4j74mfg6188c0k4xbl5zv6h6fx5"))
+          (patches
+           (list
+             (origin
+               (method url-fetch)
+               (uri (string-append upstream "/compare/" base-tag
+                                   ".." commit ".diff"))
+               (sha256
+                (base32 "07fga2jn5830fz9snwbzz2mpm2qqfjchsb969rqs7pf5py0h93fp"))
+               (file-name (string-append name ".patch")))))))
+       (home-page "https://github.com/season-lab/z3")
+       (synopsis "Z3 for FUZZOLIC")))))
+
+(define-public fuzzy-sat
+  (let ((commit "99094f664abcc7cb8ff7d04eb894616b89a15efc"))
+    (package
+      (name "fuzzy-sat")
+      (version (git-version "0.1" "master" commit))
+      (home-page "https://github.com/season-lab/fuzzy-sat")
+      (source
+       (origin
+         (method git-fetch)
+         (uri (git-reference (url home-page)
+                            (commit commit)))
+         (file-name (git-file-name name version))
+         (sha256
+          (base32 "1wq2a5j73aigw64bhf4s2qgkda114vfpmwiy353m0f54f5fg6sh3"))
+         (patches (search-patches "patches/fuzzy-sat-unbundle.patch"
+                                  "patches/fuzzy-sat-install.patch"))))
+      (build-system cmake-build-system)
+      (arguments
+       '(#:phases (modify-phases %standard-phases
+                    (replace 'check
+                      (lambda* (#:key source tests? #:allow-other-keys)
+                        (when tests?
+                          (setenv "FUZZY_BIN" "tools/fuzzy-solver")
+                          (invoke "pytest" "-p" "no:cacheprovider" "-v"
+                                  (string-append source "/tests/run.py"))))))))
+      (native-inputs (list pkg-config python-pytest))
+      (inputs (list xxhash z3-for-fuzzolic))
+      (synopsis "Approximate solver for concolic execution")
+      (description "Fuzzy SAT is an approximate solver that borrows ideas
+from the fuzzing domain.  It is tailored to the symbolic expressions
+generated by concolic engines and can replace classic SMT solvers
+in this context.  By analyzing the expressions contained in symbolic queries,
+Fuzzy SAT performs informed mutations to possibly generate
+new valuable inputs.")
+      (license license:gpl2+))))
diff --git a/loftix/emulation.scm b/loftix/emulation.scm
new file mode 100644
index 0000000..e649bc5
--- /dev/null
+++ b/loftix/emulation.scm
@@ -0,0 +1,156 @@
+;;; Emulator packages
+;;;
+;;; SPDX-FileCopyrightText: 2016 Ludovic Courtès
+;;; SPDX-FileCopyrightText: 2019 Rutger Helling
+;;; SPDX-FileCopyrightText: 2025 Nguyễn Gia Phong
+;;; SPDX-License-Identifier: GPL-3.0-or-later
+
+(define-module (loftix emulation)
+  #:use-module (gnu packages)
+  #:use-module (gnu packages commencement)
+  #:use-module (gnu packages virtualization)
+  #:use-module (guix download)
+  #:use-module (guix gexp)
+  #:use-module (guix git-download)
+  #:use-module (guix packages)
+  #:use-module (guix utils))
+
+(define-public qemu-for-aflplusplus
+  (let ((base qemu-minimal)
+        (base-version "5.2.50")
+        (commit "c43dd6e0369cd5d2a2458f3bd7f4f58c8de53300")
+        (revision "master"))
+    (hidden-package
+     (package
+       (inherit base)
+       (synopsis "QEMU for AFL++")
+       (name "qemu-for-aflplusplus")
+       (version (git-version base-version revision commit))
+       (home-page "https://github.com/AFLplusplus/qemuafl")
+       (source
+        (origin
+          (method git-fetch)
+          (uri (git-reference (url home-page)
+                              (commit commit)
+                              (recursive? #t)))
+          (file-name (git-file-name name version))
+          (sha256
+           (base32 "1qhblmr3azmvzv15w4isxws8zm8jmxxmskmjhmwnn5899rr34p0g"))))
+       (arguments
+        (substitute-keyword-arguments (package-arguments base)
+          ((#:configure-flags _ #~'())
+           #~(list (string-append
+                    "--target-list="
+                    ;; AFL++ only supports using a single afl-qemu-trace,
+                    ;; so we only build qemu for the native target.
+                    (match #$(let-system system system)
+                      ("x86_64-linux"   "x86_64-linux-user")
+                      ("i686-linux"     "i386-linux-user")
+                      ("aarch64-linux"  "aarch64-linux-user")
+                      ("armhf-linux"    "arm-linux-user")
+                      ("mips64el-linux" "mips64el-linux-user")
+                      ("powerpc-linux"  "ppc-linux-user")))))
+          ((#:phases phases)
+           #~(modify-phases #$phases
+               (delete 'replace-firmwares)
+               (delete 'patch-embedded-shebangs)
+               (delete 'fix-optionrom-makefile)
+               (delete 'disable-unusable-tests)
+               (replace 'configure
+                 (lambda* (#:key inputs outputs configure-flags
+                           #:allow-other-keys)
+                   ;; The `configure' script doesn't understand some of the
+                   ;; GNU options.  Thus, add a new phase that's compatible.
+                   (let ((out (assoc-ref outputs "out")))
+                     (setenv "SHELL" (which "bash"))
+                     ;; The binaries need to be linked against -lrt.
+                     (setenv "LDFLAGS" "-lrt")
+                     (apply invoke
+                            `("./configure"
+                              ,(string-append "--cc=" (which "gcc"))
+                              ;; Some architectures insist on using HOST_CC
+                              ,(string-append "--host-cc=" (which "gcc"))
+                              "--disable-debug-info" ; save build space
+                              ,(string-append "--prefix=" out)
+                              ,(string-append "--sysconfdir=/etc")
+                              ,@configure-flags)))))
+               (add-after 'install 'install-qasan-header
+                 (lambda* (#:key outputs #:allow-other-keys)
+                   (install-file "qemuafl/qasan.h"
+                                 (string-append (assoc-ref outputs "out")
+                                                "/include"))))
+               (delete 'delete-firmwares)))))))))
+
+(define-public qemu-for-fuzzolic
+  (let ((base qemu-minimal)
+        (base-version "4.1.1")
+        (commit "a07b82d618b0ed16d7bf1822653a74821cf13dbd")
+        (revision "symbolic"))
+    (hidden-package
+     (package
+       (inherit base)
+       (synopsis "QEMU with symbolic tracer")
+       (name "qemu-for-fuzzolic")
+       (version (git-version base-version revision commit))
+       (home-page "https://github.com/season-lab/qemu")
+       (source
+        (origin
+          (method url-fetch)
+          (uri (string-append "https://download.qemu.org/qemu-"
+                              base-version ".tar.xz"))
+          (sha256
+           (base32 "1lm1jndfpc5sydwrxyiz5sms414zkcg9jdl0zx318qbjsayxnvzd"))
+          (patches
+           (cons
+             (origin
+               (method url-fetch)
+               (uri (string-append home-page "/compare/v" base-version
+                                   ".." commit ".diff"))
+               (sha256
+                (base32 "1cqp0h0glz4pvq10lr7k9z5g9wjl6svlm51rapf3mbsvb1qy3rl1"))
+               (file-name (string-append name ".patch")))
+             (search-patches
+              "patches/qemu-for-fuzzolic-test-opts-range-beyond.patch"
+              "patches/qemu-for-fuzzolic-static-global.patch")))))
+       (arguments
+        (substitute-keyword-arguments (package-arguments base)
+          ((#:configure-flags _ #~'())
+           #~'("--target-list=x86_64-linux-user"))
+          ((#:phases phases)
+           #~(modify-phases #$phases
+               (delete 'replace-firmwares)
+               (delete 'patch-embedded-shebangs)
+               (delete 'fix-optionrom-makefile)
+               (delete 'disable-unusable-tests)
+               (replace 'configure
+                 (lambda* (#:key inputs outputs (configure-flags '())
+                           #:allow-other-keys)
+                   ;; The `configure' script doesn't understand some of the
+                   ;; GNU options.  Thus, add a new phase that's compatible.
+                   (let ((out (assoc-ref outputs "out")))
+                     (setenv "SHELL" (which "bash"))
+                     ;; The binaries need to be linked against -lrt.
+                     (setenv "LDFLAGS" "-lrt")
+                     (apply invoke
+                       "./configure"
+                       (string-append "--cc=" (which "gcc"))
+                       ;; Some architectures insist on using HOST_CC
+                       (string-append "--host-cc=" (which "gcc"))
+                       "--disable-debug-info" ; save build space
+                       (string-append "--prefix=" out)
+                       (string-append "--sysconfdir=/etc")
+                       configure-flags))))
+               (add-after 'install 'install-symbolic-header
+                 (lambda* (#:key outputs #:allow-other-keys)
+                   (install-file
+                    "tcg/symbolic/symbolic-struct.h"
+                    (string-append (assoc-ref outputs "out")
+                                   "/include/qemu/tcg/symbolic"))))
+               (delete 'delete-firmwares)))))
+       (native-inputs
+        (modify-inputs (package-native-inputs base)
+          ;; gcc-toolchain still defaults to version 11 unless on hurd64,
+          ;; which fails to include linux/mount.h in glibc>=2.36's sys/mount.h,
+          ;; causing compilation failure due to redefinition:
+          ;; https://gcc.gnu.org/bugzilla/show_bug.cgi?id=91085
+          (prepend gcc-toolchain-14)))))))
diff --git a/loftix/fuzzing.scm b/loftix/fuzzing.scm
index 6ec3a35..fd05a61 100644
--- a/loftix/fuzzing.scm
+++ b/loftix/fuzzing.scm
@@ -1,22 +1,55 @@
 ;;; Packages for software fuzzing
 ;;;
-;;; SPDX-FileCopyrightText: 2024 Nguyễn Gia Phong
+;;; SPDX-FileCopyrightText: 2024-2025 Nguyễn Gia Phong
 ;;; SPDX-License-Identifier: GPL-3.0-or-later
 
 (define-module (loftix fuzzing)
   #:use-module (gnu packages)
+  #:use-module (gnu packages check)
   #:use-module (gnu packages gcc)
   #:use-module (gnu packages debug)
+  #:use-module (gnu packages digest)
+  #:use-module (gnu packages glib)
   #:use-module (gnu packages instrumentation)
   #:use-module (gnu packages man)
   #:use-module (gnu packages m4)
+  #:use-module (gnu packages pkg-config)
+  #:use-module (gnu packages python)
+  #:use-module (gnu packages python-build)
+  #:use-module (guix build-system cmake)
   #:use-module (guix build-system gnu)
+  #:use-module (guix build-system pyproject)
   #:use-module (guix download)
   #:use-module (guix gexp)
   #:use-module (guix git-download)
   #:use-module ((guix licenses) #:prefix license:)
   #:use-module (guix packages)
-  #:use-module (guix utils))
+  #:use-module (guix utils)
+  #:use-module (loftix deduction)
+  #:use-module (loftix emulation)
+  #:export (for-evocatio))
+
+(define-public afl++
+  (package
+    (inherit aflplusplus)
+    (name "afl++")
+    (arguments
+      (substitute-keyword-arguments (package-arguments aflplusplus)
+        ((#:phases phases)
+         #~(modify-phases #$phases
+             (add-after 'build 'build-qasan
+               (lambda* (#:key make-flags #:allow-other-keys)
+                 (apply invoke "make" "-C" "qemu_mode/libqasan" make-flags)))
+             ;; afl-qemu-trace is a symbolic link to QEMU's binary.
+             ;; Substituting its source code with AFL++'s output path
+             ;; would result in a dependency cycle.
+             (add-after 'install-qemu 'wrap-qemu
+               (lambda* (#:key outputs #:allow-other-keys)
+                 (let ((out (assoc-ref outputs "out")))
+                   (wrap-program (string-append out "/bin/afl-qemu-trace")
+                     `("AFL_PATH" = (,(string-append out "/lib/afl")))))))))))
+    (inputs (modify-inputs (package-inputs aflplusplus)
+              (replace "qemu" qemu-for-aflplusplus)))))
 
 (define-public afl-dyninst
   (package
@@ -123,3 +156,167 @@ of how an attacker can exploit a bug.
 Evocatio leverages a capability-guided fuzzer to efficiently uncover
 new bug capabilities (rather than only generating a single crashing test case
 for a given bug, as a traditional greybox fuzzer does)."))))
+
+(define (for-evocatio base)
+  (package
+    (inherit base)
+    (name (string-append (package-name base) "-for-evocatio"))
+    (arguments
+     (substitute-keyword-arguments (package-arguments base)
+       ((#:configure-flags flags #~'())
+        #~(cons (string-append "CC=" #$evocatio "/bin/afl-cc")
+                #$flags))
+       ((#:phases phases #~%standard-phases)
+        #~(modify-phases #$phases
+            (add-before 'configure 'set-env
+              (lambda _
+                (setenv "CC" #$(file-append evocatio "/bin/afl-cc"))
+                (setenv "AFL_USE_ASAN" "1")
+                (setenv "AFL_USE_UBSAN" "1")
+                (setenv "ASAN_OPTIONS" "detect_leaks=0")))))
+       ((#:tests? _ #f)
+        #f)))
+    (native-inputs
+      (modify-inputs (package-native-inputs base)
+        (append evocatio)))))
+
+(define-public fuzzolic-showmap
+  (hidden-package
+   (package
+     (inherit aflplusplus)
+     (name "fuzzolic-showmap")
+     (source (origin
+               (inherit (package-source aflplusplus))
+               (patches (search-patches "patches/fuzzolic-showmap.patch"))))
+     (arguments
+      (substitute-keyword-arguments (package-arguments aflplusplus)
+        ((#:phases phases #~%standard-phases)
+         #~(modify-phases #$phases
+             (replace 'install
+               (lambda* (#:key outputs #:allow-other-keys)
+                 (let* ((dir (string-append (assoc-ref outputs "out")
+                                            "/bin"))
+                        (file (string-append dir "/fuzzolic-showmap")))
+                   (mkdir-p dir)
+                   (copy-file "afl-showmap" file)))))))))))
+
+(define-public fuzzolic
+  (let* ((base-name "fuzzolic")
+         (commit "cf4285aa08d1751fdf6824bfaaf75895055dc495")
+         (revision "master")
+         (version (git-version "0" revision commit))
+         (base-source
+          (origin
+            (method git-fetch)
+            (uri (git-reference
+                  (url "https://github.com/season-lab/fuzzolic")
+                  (commit commit)))
+            (file-name (git-file-name base-name version))
+            (sha256
+             (base32
+              "0mi1jyc2p4ynbshscnyvgyxcy6hdaa3fw77j4c8bchw049kc4w3p"))))
+         (description "FUZZOLIC is a concolic executor based on QEMU.
+
+It can instrument binary programs at runtime in order to build
+symbolic expressions and queries.  To reduce the runtime overhead
+and improve accuracy of the queries, it devises three analysis modes
+that are dynamically enabled during the program execution based on
+the running context.
+
+Moreover, differently from other concolic executors,
+FUZZOLIC runs the solver component, which reasons over the symbolic queries
+generated when analyzing a program, inside another process to reduce
+execution interferences that may be caused by the solver
+and negatively affect the analyzed application.")
+         (home-page "https://season-lab.github.io/fuzzolic")
+         (solver
+          (package
+            (name (string-append base-name "-solver"))
+            (version version)
+            (source (origin
+                      (inherit base-source)
+                      (patches (search-patches
+                                "patches/fuzzolic-solver-unbundle.patch"
+                                "patches/fuzzolic-solver-install.patch"))))
+            (build-system cmake-build-system)
+            (arguments '(#:configure-flags '("-S" "../source/solver")
+                         #:tests? #f))
+            (native-inputs (list pkg-config))
+            (inputs (list fuzzy-sat
+                          glib
+                          qemu-for-fuzzolic
+                          xxhash
+                          z3-for-fuzzolic))
+            (synopsis "Fuzzy constraint solver for FUZZOLIC")
+            (description description)
+            (home-page home-page)
+            (license license:gpl2+)))
+         (utils
+          (package
+            (name (string-append base-name "-utils"))
+            (version version)
+            (source (origin
+                      (inherit base-source)
+                      (patches (search-patches
+                                "patches/fuzzolic-utils-make.patch"))))
+            (build-system gnu-build-system)
+            (arguments
+             (list #:make-flags #~(list (string-append "CC=" #$(cc-for-target))
+                                        (string-append "PREFIX=" #$output))
+                   #:phases #~(modify-phases %standard-phases
+                                (delete 'configure)
+                                (delete 'check))))
+            (inputs (list python))
+            (synopsis "Fuzzy constraint solver for FUZZOLIC")
+            (description description)
+            (home-page home-page)
+            (license license:gpl2+))))
+    (package
+      (name base-name)
+      (version version)
+      (source (origin
+                (inherit base-source)
+                (snippet #~(call-with-output-file "pyproject.toml"
+                             (lambda (port)
+                               (display (string-append "
+[build-system]
+requires = ['flit_core >=3.2']
+build-backend = 'flit_core.buildapi'
+
+[project]
+name = '" #$base-name "'
+version = '0'
+description = '''" #$description "
+'''
+
+[project.scripts]
+fuzzolic = 'fuzzolic.fuzzolic:main'
+fuzzolic-with-afl = 'fuzzolic.run_afl_fuzzolic:main'
+") port))))
+                (patches (search-patches
+                          "patches/fuzzolic-python-package.patch"
+                          "patches/fuzzolic-unbundle.patch"
+                          ;; https://github.com/season-lab/fuzzolic/pull/13
+                          "patches/fuzzolic-timeout-solver.patch"
+                          "patches/fuzzolic-relax-perf-test.patch"
+                          "patches/fuzzolic-test-fix-runner.patch"
+                          "patches/fuzzolic-test-skip-nondeterministic.patch"))))
+      (build-system pyproject-build-system)
+      (arguments
+       '(#:phases (modify-phases %standard-phases
+                    (replace 'check
+                      (lambda* (#:key tests? #:allow-other-keys)
+                        (when tests?
+                          (invoke "make" "-C" "tests")
+                          (invoke "pytest" "-vv" "tests/run.py" "--fuzzy")
+                          (invoke "pytest" "-vv" "tests/run.py")))))))
+      (native-inputs (list python-flit-core python-pytest))
+      (propagated-inputs (list aflplusplus
+                               fuzzolic-showmap
+                               qemu-for-fuzzolic
+                               solver
+                               utils))
+      (synopsis "Concolic fuzzer")
+      (description description)
+      (home-page home-page)
+      (license license:gpl2+))))
diff --git a/loftix/patching.scm b/loftix/patching.scm
index d638019..8b50e6e 100644
--- a/loftix/patching.scm
+++ b/loftix/patching.scm
@@ -20,11 +20,11 @@
   (package
     (name "e9patch")
     (version "1.0.0-rc10")
+    (home-page "https://github.com/GJDuck/e9patch")
     (source (origin
               (method git-fetch)
-              (uri (git-reference
-                   (url "https://github.com/GJDuck/e9patch")
-                   (commit (string-append "v" version))))
+              (uri (git-reference (url home-page)
+                                  (commit (string-append "v" version))))
               (sha256
                (base32
                 "1l2pjxgr2mckpffvj7hf0sjvv3678138afjb0wc3f6c2zrcpspf8"))
@@ -47,7 +47,6 @@
                                             "PREFIX=" #$output))))
     (native-inputs (list markdown xxd))
     (inputs (list elfutils zycore zydis zlib))
-    (home-page "https://github.com/GJDuck/e9patch")
     (synopsis "Static binary rewriting tool")
     (description
      "E9Patch is a static binary rewriting tool for x86-64 ELF binaries.
diff --git a/patches/e9patch-check.patch b/patches/e9patch-check.patch
index d060c9f..bf39bd2 100644
--- a/patches/e9patch-check.patch
+++ b/patches/e9patch-check.patch
@@ -162,7 +162,7 @@ new file mode 100755
 index 000000000000..d22009e99b72
 --- /dev/null
 +++ b/test/regtest/regtest
-@@ -0,0 +1,25 @@
+@@ -0,0 +1,26 @@
 +#!/bin/sh
 +fails=()
 +for exe in $*
@@ -176,6 +176,7 @@ index 000000000000..d22009e99b72
 +  then ./exec.sh ./$cmd 1>$out 2>&1
 +  else ./exec.sh ./$exe 1>$out 2>&1
 +  fi
++  sed -i 's/ (core dumped)$//' $out
 +
 +  diff -u $out $exp
 +  if test $? -ne 0
diff --git a/patches/fuzzolic-python-package.patch b/patches/fuzzolic-python-package.patch
new file mode 100644
index 0000000..8ef5559
--- /dev/null
+++ b/patches/fuzzolic-python-package.patch
@@ -0,0 +1,39 @@
+commit 5098598289744766508d7b390f19d61bad30f54c
+Author: Nguyễn Gia Phong <cnx@loang.net>
+Date:   2025-05-07 14:34:24 +0900
+
+    Turn fuzzolic/ into a Python package
+
+diff --git a/fuzzolic/executor.py b/fuzzolic/executor.py
+index 39c6aa6dddb9..f2639eb8da6a 100644
+--- a/fuzzolic/executor.py
++++ b/fuzzolic/executor.py
+@@ -17,8 +17,8 @@ import random
+ import ctypes
+ import resource
+ 
+-import minimizer_qsym
+-import minimizer
++from . import minimizer_qsym
++from . import minimizer
+ 
+ SCRIPT_DIR = os.path.dirname(os.path.realpath(__file__))
+ SOLVER_SMT_BIN = SCRIPT_DIR + '/../solver/solver-smt'
+diff --git a/fuzzolic/fuzzolic.py b/fuzzolic/fuzzolic.py
+index ed6aac5cf5ab..3b692fb4b59c 100755
+--- a/fuzzolic/fuzzolic.py
++++ b/fuzzolic/fuzzolic.py
+@@ -2,11 +2,12 @@
+ 
+ import os
+ import sys
+-import executor
+ import signal
+ import argparse
+ import shutil
+ 
++from . import executor
++
+ ABORTING_COUNT = 0
+ 
+ 
diff --git a/patches/fuzzolic-relax-perf-test.patch b/patches/fuzzolic-relax-perf-test.patch
new file mode 100644
index 0000000..f1de80a
--- /dev/null
+++ b/patches/fuzzolic-relax-perf-test.patch
@@ -0,0 +1,13 @@
+diff --git a/tests/run.py b/tests/run.py
+index 2144d96c7544..1d84a2999662 100755
+--- a/tests/run.py
++++ b/tests/run.py
+@@ -78,7 +78,7 @@ def run(test,
+     if perf_run:
+         slowdown = emulated_time / native_time
+         print("Slowdown: %s" % round(slowdown, 1))
+-        assert slowdown < 70
++        assert slowdown < 140
+ 
+     if expected_inputs > 0:
+         testcases = glob.glob(WORKDIR + "/tests/test_*.dat") 
diff --git a/patches/fuzzolic-showmap.patch b/patches/fuzzolic-showmap.patch
new file mode 100644
index 0000000..ec9d99e
--- /dev/null
+++ b/patches/fuzzolic-showmap.patch
@@ -0,0 +1,69 @@
+diff --git a/src/afl-showmap.c b/src/afl-showmap.c
+index 881ca2a63ffe..a3485b881b3e 100644
+--- a/src/afl-showmap.c
++++ b/src/afl-showmap.c
+@@ -410,15 +410,16 @@ void pre_afl_fsrv_write_to_testcase(afl_forkserver_t *fsrv, u8 *mem, u32 len) {
+ 
+ /* Execute target application. */
+ 
+-static void showmap_run_target_forkserver(afl_forkserver_t *fsrv, u8 *mem,
+-                                          u32 len) {
++static fsrv_run_result_t showmap_run_target_forkserver(afl_forkserver_t *fsrv,
++                                                       u8 *mem, u32 len) {
+ 
+   pre_afl_fsrv_write_to_testcase(fsrv, mem, len);
+ 
+   if (!quiet_mode) { SAYF("-- Program output begins --\n" cRST); }
+ 
+-  if (afl_fsrv_run_target(fsrv, fsrv->exec_tmout, &stop_soon) ==
+-      FSRV_RUN_ERROR) {
++  const fsrv_run_result_t result =
++      afl_fsrv_run_target(fsrv, fsrv->exec_tmout, &stop_soon);
++  if (result == FSRV_RUN_ERROR) {
+ 
+     FATAL("Error running target");
+ 
+@@ -477,6 +478,7 @@ static void showmap_run_target_forkserver(afl_forkserver_t *fsrv, u8 *mem,
+ 
+   }
+ 
++  return result;
+ }
+ 
+ /* Read initial file. */
+@@ -867,7 +869,11 @@ u32 execute_testcases(u8 *dir) {
+ 
+       }
+ 
+-      showmap_run_target_forkserver(fsrv, in_data, in_len);
++      if (showmap_run_target_forkserver(fsrv, in_data, in_len)
++          == FSRV_RUN_CRASH)
++        snprintf(outfile, sizeof(outfile), "%s/%s.crash", out_file, fn2);
++      else
++        snprintf(outfile, sizeof(outfile), "%s/%s", out_file, fn2);
+       ck_free(in_data);
+       ++done;
+ 
+@@ -1422,9 +1428,19 @@ int main(int argc, char **argv_orig, char **envp) {
+ 
+     }
+ 
+-    stdin_file = at_file ? strdup(at_file)
+-                         : (char *)alloc_printf("%s/.afl-showmap-temp-%u",
+-                                                use_dir, (u32)getpid());
++    if (at_file) {
++      stdin_file = strdup(at_file);
++    } else {
++      char* file_ext = get_afl_env("FILE_EXT");
++      if (file_ext)
++        stdin_file =
++            (char *)alloc_printf("%s/.afl-showmap-temp-%u.%s",
++                                 use_dir, (u32)getpid(), file_ext);
++      else
++        stdin_file =
++            (char *)alloc_printf("%s/.afl-showmap-temp-%u",
++                                 use_dir, (u32)getpid());
++    }
+     unlink(stdin_file);
+ 
+     // If @@ are in the target args, replace them and also set use_stdin=false.
diff --git a/patches/fuzzolic-solver-install.patch b/patches/fuzzolic-solver-install.patch
new file mode 100644
index 0000000..430356e
--- /dev/null
+++ b/patches/fuzzolic-solver-install.patch
@@ -0,0 +1,10 @@
+diff --git a/solver/CMakeLists.txt b/solver/CMakeLists.txt
+index a159187a5b27..9618f9a0576d 100644
+--- a/solver/CMakeLists.txt
++++ b/solver/CMakeLists.txt
+@@ -28,3 +28,5 @@ set(CMAKE_CXX_FLAGS "-Wall -Wextra -O3 -g")
+ set(CMAKE_C_FLAGS "-O3 -g")
+ #set(CMAKE_CXX_FLAGS_DEBUG "-g")
+ #set(CMAKE_CXX_FLAGS_RELEASE "-O3")
++
++install(TARGETS solver-smt solver-fuzzy)
diff --git a/patches/fuzzolic-solver-unbundle.patch b/patches/fuzzolic-solver-unbundle.patch
new file mode 100644
index 0000000..f34940d
--- /dev/null
+++ b/patches/fuzzolic-solver-unbundle.patch
@@ -0,0 +1,598 @@
+commit 7b451dd864314d30aa4137163aa318fad711833b
+Author: Nguyễn Gia Phong <cnx@loang.net>
+Date:   2025-04-29 11:23:26 +0900
+
+    Unbundle FUZZY-SAT, QEMU, xxHash and Z3
+
+diff --git a/solver/CMakeLists.txt b/solver/CMakeLists.txt
+index a159187a5b27..4a252172da29 100644
+--- a/solver/CMakeLists.txt
++++ b/solver/CMakeLists.txt
+@@ -2,27 +2,40 @@ cmake_minimum_required(VERSION 3.7)
+ 
+ project(Solver)
+ 
+-add_executable(solver-smt main.c i386.c branch_coverage.c opts.c xxHash/xxhash.c)
+-add_executable(solver-fuzzy main.c i386.c branch_coverage.c opts.c xxHash/xxhash.c)
++add_executable(solver-smt main.c i386.c branch_coverage.c opts.c)
++add_executable(solver-fuzzy main.c i386.c branch_coverage.c opts.c)
+ 
+ target_compile_definitions(solver-smt PRIVATE USE_FUZZY_SOLVER=0)
+ target_compile_definitions(solver-fuzzy PRIVATE USE_FUZZY_SOLVER=1)
+ 
+ # z3
+-target_link_libraries(solver-smt z3)
+-target_link_libraries(solver-fuzzy z3)
++find_package(Z3 REQUIRED)
++target_include_directories(solver-smt PRIVATE ${Z3_INCLUDE_DIRS})
++target_include_directories(solver-fuzzy PRIVATE ${Z3_INCLUDE_DIRS})
++target_link_libraries(solver-smt ${Z3_LIBRARIES})
++target_link_libraries(solver-fuzzy ${Z3_LIBRARIES})
+ 
+ # fuzzy
+-target_link_libraries(solver-smt ${CMAKE_SOURCE_DIR}/fuzzy-sat/libZ3Fuzzy.a)
+-target_link_libraries(solver-fuzzy ${CMAKE_SOURCE_DIR}/fuzzy-sat/libZ3Fuzzy.a)
++find_package(Z3Fuzzy REQUIRED)
++target_include_directories(solver-smt PRIVATE ${Z3Fuzzy_INCLUDE_DIRS})
++target_include_directories(solver-fuzzy PRIVATE ${Z3Fuzzy_INCLUDE_DIRS})
++target_link_libraries(solver-smt "Z3Fuzzy")
++target_link_libraries(solver-fuzzy "Z3Fuzzy")
+ 
+ # glib
+ find_package(PkgConfig REQUIRED)
+ pkg_search_module(GLIB REQUIRED glib-2.0)
+ target_include_directories(solver-smt PRIVATE ${GLIB_INCLUDE_DIRS})
+ target_include_directories(solver-fuzzy PRIVATE ${GLIB_INCLUDE_DIRS})
+-target_link_libraries(solver-smt ${GLIB_LDFLAGS})
+-target_link_libraries(solver-fuzzy ${GLIB_LDFLAGS})
++target_link_libraries(solver-smt ${GLIB_LIBRARIES})
++target_link_libraries(solver-fuzzy ${GLIB_LIBRARIES})
++
++# xxHash
++pkg_search_module(XXHASH REQUIRED libxxhash)
++target_include_directories(solver-smt PRIVATE ${XXHASH_INCLUDE_DIRS})
++target_include_directories(solver-fuzzy PRIVATE ${XXHASH_INCLUDE_DIRS})
++target_link_libraries(solver-smt ${XXHASH_LIBRARIES})
++target_link_libraries(solver-fuzzy ${XXHASH_LIBRARIES})
+ 
+ set(CMAKE_CXX_FLAGS "-Wall -Wextra -O3 -g")
+ set(CMAKE_C_FLAGS "-O3 -g")
+diff --git a/solver/branch_coverage.c b/solver/branch_coverage.c
+index 4d726f6e592c..88ca22b37ad2 100644
+--- a/solver/branch_coverage.c
++++ b/solver/branch_coverage.c
+@@ -3,8 +3,7 @@
+ 
+ extern Config config;
+ 
+-#define XXH_STATIC_LINKING_ONLY
+-#include "xxHash/xxhash.h"
++#include <xxhash.h>
+ 
+ #include <stdio.h>
+ 
+@@ -42,11 +41,13 @@ static inline uintptr_t hash_pc(uintptr_t pc, uint8_t taken)
+         taken = 1;
+     }
+ 
+-    XXH32_state_t state;
+-    XXH32_reset(&state, 0); // seed = 0
+-    XXH32_update(&state, &pc, sizeof(pc));
+-    XXH32_update(&state, &taken, sizeof(taken));
+-    return XXH32_digest(&state) % BRANCH_BITMAP_SIZE;
++    XXH32_state_t *state = XXH32_createState();
++    XXH32_reset(state, 0); // seed = 0
++    XXH32_update(state, &pc, sizeof(pc));
++    XXH32_update(state, &taken, sizeof(taken));
++    const uintptr_t digest = XXH32_digest(state) % BRANCH_BITMAP_SIZE;
++    XXH32_freeState(state);
++    return digest;
+ }
+ 
+ static inline void load_bitmap(const char* path, uint8_t* data, size_t size)
+@@ -126,17 +127,17 @@ static inline int is_interesting_context(uintptr_t h, uint8_t bits)
+     gpointer       key, value;
+     GHashTableIter iter;
+     g_hash_table_iter_init(&iter, visited_branches);
++    XXH32_state_t *state = XXH32_createState();
+     while (g_hash_table_iter_next(&iter, &key, &value)) {
+ 
+         uintptr_t prev_h = (uintptr_t)key;
+ 
+         // Calculate hash(prev_h || h)
+-        XXH32_state_t state;
+-        XXH32_reset(&state, 0);
+-        XXH32_update(&state, &prev_h, sizeof(prev_h));
+-        XXH32_update(&state, &h, sizeof(h));
++        XXH32_reset(state, 0);
++        XXH32_update(state, &prev_h, sizeof(prev_h));
++        XXH32_update(state, &h, sizeof(h));
+ 
+-        uintptr_t hash = XXH32_digest(&state) % (BRANCH_BITMAP_SIZE * CHAR_BIT);
++        uintptr_t hash = XXH32_digest(state) % (BRANCH_BITMAP_SIZE * CHAR_BIT);
+         uintptr_t idx  = hash / CHAR_BIT;
+         uintptr_t mask = 1 << (hash % CHAR_BIT);
+ 
+@@ -145,6 +146,7 @@ static inline int is_interesting_context(uintptr_t h, uint8_t bits)
+             interesting = 1;
+         }
+     }
++    XXH32_freeState(state);
+ 
+     if (bits == 0) {
+         g_hash_table_add(visited_branches, (gpointer)h);
+diff --git a/solver/debug.h b/solver/debug.h
+index b3ce2405074a..02614765f780 100644
+--- a/solver/debug.h
++++ b/solver/debug.h
+@@ -17,6 +17,8 @@
+ #ifndef _HAVE_DEBUG_H
+ #define _HAVE_DEBUG_H
+ 
++#include <z3.h>
++
+ #include <errno.h>
+ 
+ //#include "config.h"
+diff --git a/solver/eval-driver.c b/solver/eval-driver.c
+index 1140a87570a8..25390384114b 100644
+--- a/solver/eval-driver.c
++++ b/solver/eval-driver.c
+@@ -14,7 +14,6 @@
+ #include <stdlib.h>
+ #include <assert.h>
+ #include <sys/time.h>
+-static_assert(Z3_VERSION == 487, "This executable requires z3 4.8.7+");
+ 
+ typedef struct {
+     uint8_t* data;
+@@ -120,15 +119,15 @@ unsigned long z3fuzz_evaluate_expression_z3(Z3_context ctx,
+ 
+     // evaluate the query in the model
+     Z3_ast  solution;
+-    Z3_bool successfulEval =
+-        Z3_model_eval(ctx, z3_m, query, Z3_TRUE, &solution);
++    bool    successfulEval =
++        Z3_model_eval(ctx, z3_m, query, true, &solution);
+     assert(successfulEval && "Failed to evaluate model");
+ 
+     Z3_model_dec_ref(ctx, z3_m);
+     if (Z3_get_ast_kind(ctx, solution) == Z3_NUMERAL_AST) {
+-        Z3_bool successGet = Z3_get_numeral_uint64(ctx, solution, &res);
+-        assert(successGet == Z3_TRUE &&
+-               "z3fuzz_evaluate_expression_z3() failed to get "
++        bool successGet = Z3_get_numeral_uint64(ctx, solution, &res);
++        assert(successGet
++	       && "z3fuzz_evaluate_expression_z3() failed to get "
+                "constant");
+     } else
+         res = Z3_get_bool_value(ctx, solution) == Z3_L_TRUE ? 1UL : 0UL;
+@@ -179,15 +178,11 @@ __evaluate_expression(Z3_context ctx, Z3_ast value, Z3_ast* values,
+                     Z3_symbol s = Z3_get_decl_name(ctx, decl);
+ #if 0
+                     int       symbol_index = Z3_get_symbol_int(ctx, s);
+-                    Z3_bool   successGet =
++                    bool      successGet =
+                         Z3_get_numeral_uint64(ctx, values[symbol_index],
+-#if Z3_VERSION <= 451
+-                                              (long long unsigned int*)&res
+-#else
+                                               (uint64_t*)&res
+-#endif
+                         );
+-                    assert(successGet == Z3_TRUE &&
++                    assert(successGet &&
+                            "z3fuzz_evaluate_expression() failed to get "
+                            "constant (symbol)");
+ #else
+@@ -971,15 +966,9 @@ __evaluate_expression(Z3_context ctx, Z3_ast value, Z3_ast* values,
+             break;
+         }
+         case Z3_NUMERAL_AST: {
+-            Z3_bool successGet =
+-                Z3_get_numeral_uint64(ctx, value,
+-#if Z3_VERSION <= 451
+-                                      (long long unsigned int*)&res
+-#else
+-                                      (uint64_t*)&res
+-#endif
+-                );
+-            assert(successGet == Z3_TRUE &&
++            bool successGet =
++                Z3_get_numeral_uint64(ctx, value, (uint64_t*) &res);
++            assert(successGet &&
+                    "z3fuzz_evaluate_expression() failed to get constant");
+             break;
+         }
+diff --git a/solver/eval.c b/solver/eval.c
+index 4fd0e11bc187..837f1152adb9 100644
+--- a/solver/eval.c
++++ b/solver/eval.c
+@@ -1,6 +1,4 @@
+-
+-#define XXH_STATIC_LINKING_ONLY
+-#include "xxHash/xxhash.h"
++#include <xxhash.h>
+ 
+ #define DICT_DATA_T uint64_t
+ #include "dict.h"
+@@ -534,12 +532,8 @@ static uintptr_t conc_eval(uint8_t* m, size_t n, dict__uint64_t* m_others,
+ 
+         case Z3_NUMERAL_AST: {
+             uint64_t value;
+-            Z3_bool  r = Z3_get_numeral_uint64(ctx, e,
+-#if Z3_VERSION <= 451
+-                                              (long long unsigned int*)
+-#endif
+-                                              &value);
+-            assert(r == Z3_TRUE);
++            bool     r = Z3_get_numeral_uint64(ctx, e, &value);
++            assert(r);
+             res = value;
+             break;
+         }
+diff --git a/solver/fuzzy-solver-expr.c b/solver/fuzzy-solver-expr.c
+index a54b782456d7..f5a44032230c 100644
+--- a/solver/fuzzy-solver-expr.c
++++ b/solver/fuzzy-solver-expr.c
+@@ -7,9 +7,6 @@
+ #include <time.h>
+ #include <unistd.h>
+ 
+-#include <z3.h>
+-#define Z3_VERSION 487
+-
+ #define USE_COLOR
+ #include "debug.h"
+ 
+@@ -17,7 +14,9 @@
+ #define EXPR_QUEUE_POLLING_TIME_NS 5000
+ 
+ #include "index-queue.h"
+-#include "../tracer/tcg/symbolic/symbolic-struct.h"
++
++#include <qemu/tcg/symbolic/symbolic-struct.h>
++#include <z3.h>
+ 
+ static unsigned char* testcase_bytes   = 0;
+ static unsigned char* tmp_testcase     = 0;
+@@ -40,17 +39,9 @@ static void exitf(const char* message)
+     exit(1);
+ }
+ 
+-#if Z3_VERSION <= 441
+-static void smt_error_handler(Z3_context c)
+-#else
+ static void smt_error_handler(Z3_context c, Z3_error_code e)
+-#endif
+ {
+-#if Z3_VERSION <= 441
+-    printf("Error code: %s\n", Z3_get_error_msg(smt_solver.ctx));
+-#else
+     printf("Error code: %s\n", Z3_get_error_msg(smt_solver.ctx, e));
+-#endif
+     exitf("incorrect use of Z3");
+ }
+ 
+@@ -141,14 +132,14 @@ static void     smt_dump_solution(Z3_model m)
+         Z3_ast  input_slice = Z3_mk_extract(smt_solver.ctx, (8 * (i + 1)) - 1,
+                                            8 * i, cached_input);
+         Z3_ast  solution;
+-        Z3_bool successfulEval =
++        bool    successfulEval =
+             Z3_model_eval(smt_solver.ctx, m, input_slice,
+-                          /*model_completion=*/Z3_TRUE, &solution);
++                          /*model_completion=*/true, &solution);
+         assert(successfulEval && "Failed to evaluate model");
+         assert(Z3_get_ast_kind(smt_solver.ctx, solution) == Z3_NUMERAL_AST &&
+                "Evaluated expression has wrong sort");
+         int     solution_byte = 0;
+-        Z3_bool successGet =
++        bool    successGet =
+             Z3_get_numeral_int(smt_solver.ctx, solution, &solution_byte);
+         if (solution_byte)
+             printf("Solution[%ld]: %x\n", i, solution_byte);
+diff --git a/solver/fuzzy-solver.c b/solver/fuzzy-solver.c
+index 5661dffb0dcb..42bb37f6c890 100644
+--- a/solver/fuzzy-solver.c
++++ b/solver/fuzzy-solver.c
+@@ -7,8 +7,6 @@
+ #include <time.h>
+ #include <unistd.h>
+ 
+-#include <z3.h>
+-#define Z3_VERSION 487
+ 
+ #define FOUND_SUB_AND 1
+ #define FOUND_COMPARISON 2
+@@ -23,7 +21,9 @@
+ 
+ #include "index-queue.h"
+ #include "testcase-list.h"
+-#include "../tracer/tcg/symbolic/symbolic-struct.h"
++
++#include <qemu/tcg/symbolic/symbolic-struct.h>
++#include <z3.h>
+ 
+ static int expr_pool_shm_id = -1;
+ Expr*      pool;
+@@ -48,17 +48,9 @@ static void exitf(const char* message)
+     exit(1);
+ }
+ 
+-#if Z3_VERSION <= 441
+-static void smt_error_handler(Z3_context c)
+-#else
+ static void smt_error_handler(Z3_context c, Z3_error_code e)
+-#endif
+ {
+-#if Z3_VERSION <= 441
+-    printf("Error code: %s\n", Z3_get_error_msg(smt_solver.ctx));
+-#else
+     printf("Error code: %s\n", Z3_get_error_msg(smt_solver.ctx, e));
+-#endif
+     exitf("incorrect use of Z3");
+ }
+ 
+@@ -131,9 +123,9 @@ static void     smt_dump_solution(Z3_model m)
+         Z3_ast  input_slice = Z3_mk_extract(smt_solver.ctx, (8 * (i + 1)) - 1,
+                                            8 * i, cached_input);
+         Z3_ast  solution;
+-        Z3_bool successfulEval =
++        bool    successfulEval =
+             Z3_model_eval(smt_solver.ctx, m, input_slice,
+-                          /*model_completion=*/Z3_TRUE, &solution);
++                          /*model_completion=*/true, &solution);
+         assert(successfulEval && "Failed to evaluate model");
+         solution = Z3_simplify(smt_solver.ctx,
+                                solution); // otherwise, concrete expression...
+@@ -141,7 +133,7 @@ static void     smt_dump_solution(Z3_model m)
+         assert(Z3_get_ast_kind(smt_solver.ctx, solution) == Z3_NUMERAL_AST &&
+                "Evaluated expression has wrong sort");
+         int     solution_byte = 0;
+-        Z3_bool successGet =
++        bool    successGet =
+             Z3_get_numeral_int(smt_solver.ctx, solution, &solution_byte);
+         if (solution_byte)
+             printf("Solution[%ld]: %x\n", i, solution_byte);
+@@ -191,7 +183,7 @@ static int ast_find_early_constants(Z3_ast v, unsigned long* sub_add,
+     int res = 0;
+     switch (Z3_get_ast_kind(smt_solver.ctx, v)) {
+         case Z3_APP_AST: {
+-            Z3_bool      successGet;
++            bool         successGet;
+             Z3_ast       child1, child2;
+             Z3_app       app       = Z3_to_app(smt_solver.ctx, v);
+             Z3_func_decl decl      = Z3_get_app_decl(smt_solver.ctx, app);
+@@ -218,15 +210,13 @@ static int ast_find_early_constants(Z3_ast v, unsigned long* sub_add,
+                         Z3_NUMERAL_AST) {
+                         successGet = Z3_get_numeral_uint64(smt_solver.ctx,
+                                                            child1, comparison);
+-                        assert(successGet == Z3_TRUE &&
+-                               "failed to get constant");
++                        assert(successGet && "failed to get constant");
+                         res = FOUND_COMPARISON;
+                     } else if (Z3_get_ast_kind(smt_solver.ctx, child2) ==
+                                Z3_NUMERAL_AST) {
+                         successGet = Z3_get_numeral_uint64(smt_solver.ctx,
+                                                            child2, comparison);
+-                        assert(successGet == Z3_TRUE &&
+-                               "failed to get constant");
++                        assert(successGet && "failed to get constant");
+                         res = FOUND_COMPARISON;
+                     }
+ 
+@@ -255,15 +245,13 @@ static int ast_find_early_constants(Z3_ast v, unsigned long* sub_add,
+                         Z3_NUMERAL_AST) {
+                         successGet = Z3_get_numeral_uint64(smt_solver.ctx,
+                                                            child1, sub_add);
+-                        assert(successGet == Z3_TRUE &&
+-                               "failed to get constant");
++                        assert(successGet && "failed to get constant");
+                         res = FOUND_SUB_AND;
+                     } else if (Z3_get_ast_kind(smt_solver.ctx, child2) ==
+                                Z3_NUMERAL_AST) {
+                         successGet = Z3_get_numeral_uint64(smt_solver.ctx,
+                                                            child2, sub_add);
+-                        assert(successGet == Z3_TRUE &&
+-                               "failed to get constant");
++                        assert(successGet && "failed to get constant");
+                         res = FOUND_SUB_AND;
+                     }
+                     break;
+@@ -352,9 +340,9 @@ static void ast_find_involved_inputs(Z3_ast v)
+     switch (Z3_get_ast_kind(smt_solver.ctx, v)) {
+         case Z3_NUMERAL_AST: {
+             unsigned long value = -1;
+-            Z3_bool       successGet =
++            bool          successGet =
+                 Z3_get_numeral_uint64(smt_solver.ctx, v, &value);
+-            assert(successGet == Z3_TRUE && "failed to get constant");
++            assert(successGet && "failed to get constant");
+             ADD_VALUE(value);
+             break;
+         }
+@@ -457,8 +445,8 @@ static int smt_query_evaluate(Z3_symbol input, Z3_ast input_val, Z3_ast query,
+ 
+     // evaluate the query in the model
+     Z3_ast  solution;
+-    Z3_bool successfulEval =
+-        Z3_model_eval(smt_solver.ctx, z3_m, query, Z3_TRUE, &solution);
++    bool    successfulEval =
++        Z3_model_eval(smt_solver.ctx, z3_m, query, true, &solution);
+     assert(successfulEval && "Failed to evaluate model");
+     assert(Z3_get_ast_kind(smt_solver.ctx, solution) == Z3_APP_AST &&
+            "Evaluated expression has wrong sort");
+diff --git a/solver/main.c b/solver/main.c
+index 42bedd8841fa..d0a0b58d51cd 100644
+--- a/solver/main.c
++++ b/solver/main.c
+@@ -9,11 +9,11 @@
+ #include <execinfo.h>
+ #include <string.h>
+ 
++#include <z3-fuzzy.h>
++
+ #include "debug-config.h"
+ #include "solver.h"
+ #include "i386.h"
+-#include "fuzzy-sat/z3-fuzzy.h"
+-
+ 
+ #define EXPR_QUEUE_POLLING_TIME_SECS 0
+ #define EXPR_QUEUE_POLLING_TIME_NS   5000
+@@ -177,17 +177,9 @@ static void exitf(const char* message)
+     exit(1);
+ }
+ 
+-#if Z3_VERSION <= 451
+-static void smt_error_handler(Z3_context c, Z3_error_code e)
+-#else
+ static void smt_error_handler(Z3_context c, Z3_error_code e)
+-#endif
+ {
+-#if Z3_VERSION <= 451
+-    printf("Error code: %s\n", Z3_get_error_msg(e));
+-#else
+     printf("Error code: %s\n", Z3_get_error_msg(smt_solver.ctx, e));
+-#endif
+     ABORT();
+     exitf("incorrect use of Z3");
+ }
+@@ -834,12 +826,12 @@ static void smt_dump_solution(Z3_context ctx, Z3_model m, size_t idx,
+         if (input_slice) {
+             // SAYF("input slice %ld\n", i);
+             Z3_ast  solution;
+-            Z3_bool successfulEval = Z3_model_eval(ctx, m, input_slice,
+-                                                   Z3_FALSE, // model_completion
++            bool    successfulEval = Z3_model_eval(ctx, m, input_slice,
++                                                   false, // model_completion
+                                                    &solution);
+             assert(successfulEval && "Failed to evaluate model");
+             if (Z3_get_ast_kind(ctx, solution) == Z3_NUMERAL_AST) {
+-                Z3_bool successGet =
++                bool successGet =
+                     Z3_get_numeral_int(ctx, solution, &solution_byte);
+                 if (successGet) { // && solution_byte
+                     // printf("Solution[%ld]: 0x%x\n", i, solution_byte);
+@@ -997,7 +989,7 @@ static void inline smt_dump_debug_query(Z3_solver solver, Z3_ast expr, uint64_t
+         Z3_model model = Z3_solver_get_model(smt_solver.ctx, solver);
+         Z3_model_inc_ref(smt_solver.ctx, model);
+         Z3_ast solution = NULL;
+-        Z3_model_eval(smt_solver.ctx, model, expr, Z3_TRUE, &solution);
++        Z3_model_eval(smt_solver.ctx, model, expr, true, &solution);
+         uint64_t value = 0;
+         if (is_bool) {
+           Z3_lbool res = Z3_get_bool_value(smt_solver.ctx, solution);
+@@ -1028,9 +1020,10 @@ static void inline smt_dump_debug_query(Z3_solver solver, Z3_ast expr, uint64_t
+             if (input_slice) {
+                 // SAYF("input slice %ld\n", i);
+                 Z3_ast  solution;
+-                Z3_bool successfulEval = Z3_model_eval(smt_solver.ctx, model, input_slice,
+-                                                    Z3_FALSE, // model_completion
+-                                                    &solution);
++                bool    successfulEval = Z3_model_eval(smt_solver.ctx,
++                                                       model, input_slice,
++                                  /*model_completion=*/false,
++                                                       &solution);
+                 assert(successfulEval && "Failed to evaluate model");
+                 if (Z3_get_ast_kind(smt_solver.ctx, solution) == Z3_NUMERAL_AST) {
+                     Z3_get_numeral_int(smt_solver.ctx, solution, &solution_byte);
+@@ -1113,18 +1106,12 @@ static uintptr_t smt_query_eval_uint64(Z3_model m, Z3_ast e)
+ {
+     uintptr_t value;
+     Z3_ast    solution;
+-    Z3_bool   successfulEval =
+-        Z3_model_eval(smt_solver.ctx, m, e, Z3_TRUE, &solution);
++    bool      successfulEval =
++        Z3_model_eval(smt_solver.ctx, m, e, true, &solution);
+     assert(successfulEval && "Failed to evaluate model");
+     if (Z3_get_ast_kind(smt_solver.ctx, solution) == Z3_NUMERAL_AST) {
+-
+-#if Z3_VERSION <= 451
+-        Z3_bool successGet = Z3_get_numeral_int64(smt_solver.ctx, solution,
+-                                                  (long long int*)&value);
+-#else
+-        Z3_bool successGet =
++        bool successGet =
+             Z3_get_numeral_int64(smt_solver.ctx, solution, (int64_t*)&value);
+-#endif
+         return value;
+     } else {
+         ABORT("Failed to evaluate using Z3 model.\n");
+@@ -1204,12 +1191,8 @@ static void print_z3_ast_internal(Z3_ast e, uint8_t invert_op,
+             Z3_sort  sort = Z3_get_sort(ctx, e);
+             size_t   size = Z3_get_bv_sort_size(ctx, sort);
+             uint64_t value;
+-            Z3_bool  r = Z3_get_numeral_uint64(ctx, e,
+-#if Z3_VERSION <= 451
+-                                              (long long unsigned int*)
+-#endif
+-                                              &value);
+-            if (r == Z3_TRUE) {
++            bool     r = Z3_get_numeral_uint64(ctx, e, &value);
++            if (r) {
+                 printf("%lx#%lu", value, size);
+             } else {
+                 const char* z3_query_str = Z3_ast_to_string(smt_solver.ctx, e);
+@@ -1557,12 +1540,8 @@ static inline uint8_t is_zero_const(Z3_ast e)
+ 
+     if (kind == Z3_NUMERAL_AST) {
+         uint64_t value;
+-        Z3_bool  r = Z3_get_numeral_uint64(ctx, e,
+-#if Z3_VERSION <= 451
+-                                          (long long unsigned int*)
+-#endif
+-                                          &value);
+-        if (r == Z3_FALSE) {
++        bool     r = Z3_get_numeral_uint64(ctx, e, &value);
++        if (!r) {
+             // result does not fit into 64 bits
+             return 0;
+         }
+@@ -1578,12 +1557,8 @@ static inline uint8_t is_const(Z3_ast e, uint64_t* value)
+     Z3_ast_kind kind = Z3_get_ast_kind(ctx, e);
+ 
+     if (kind == Z3_NUMERAL_AST) {
+-        Z3_bool r = Z3_get_numeral_uint64(ctx, e,
+-#if Z3_VERSION <= 451
+-                                          (long long unsigned int*)
+-#endif
+-                                              value);
+-        if (r == Z3_FALSE) {
++        bool r = Z3_get_numeral_uint64(ctx, e, value);
++        if (!r) {
+             // result does not fit into 64 bits
+             return 0;
+         }
+@@ -5518,8 +5493,8 @@ static int get_eval_uint64(Z3_model m, Z3_ast e, uintptr_t* value)
+ {
+     Z3_ast solution;
+ 
+-    Z3_bool successfulEval =
+-        Z3_model_eval(smt_solver.ctx, m, e, Z3_FALSE, &solution);
++    bool successfulEval =
++        Z3_model_eval(smt_solver.ctx, m, e, false, &solution);
+     assert(successfulEval && "Failed to evaluate model");
+ 
+     if (Z3_get_ast_kind(smt_solver.ctx, solution) == Z3_NUMERAL_AST) {
+diff --git a/solver/solver.h b/solver/solver.h
+index 3efb1ebcb163..bea15d608bf7 100644
+--- a/solver/solver.h
++++ b/solver/solver.h
+@@ -6,13 +6,11 @@
+ 
+ #include <gmodule.h>
+ 
+-#include <z3.h>
+-#define Z3_VERSION 487
+-
+ #define USE_COLOR
+ #include "debug.h"
+ 
+-#include "../tracer/tcg/symbolic/symbolic-struct.h"
++#include <qemu/tcg/symbolic/symbolic-struct.h>
++#include <z3.h>
+ 
+ typedef enum ExprAnnotationType {
+     COSTANT_AND,
diff --git a/patches/fuzzolic-test-fix-runner.patch b/patches/fuzzolic-test-fix-runner.patch
new file mode 100644
index 0000000..7610eca
--- /dev/null
+++ b/patches/fuzzolic-test-fix-runner.patch
@@ -0,0 +1,326 @@
+commit c9d5d6f3872991e7f5cffc8146d3abe121883d61
+Author: Nguyễn Gia Phong <cnx@loang.net>
+Date:   2025-05-08 11:13:10 +0900
+
+    Use temporary directories for tests
+
+diff --git a/tests/run.py b/tests/run.py
+index 2144d96c7544..0b69d990faf5 100755
+--- a/tests/run.py
++++ b/tests/run.py
+@@ -9,14 +9,13 @@ import time
+ import pytest
+ 
+ SCRIPT_DIR = os.path.dirname(os.path.realpath(__file__))
+-WORKDIR = SCRIPT_DIR + "/workdir"
+ 
+ 
+ def pytest_addoption(parser):
+     parser.addoption("--fuzzy", action="store_true", default="run tests using Fuzzy-SAT")
+ 
+ 
+-def run(test, 
++def run(test, workdir,
+         use_duplicate_testcase_checker=False, 
+         expected_inputs=1, 
+         perf_run=False, 
+@@ -25,8 +24,7 @@ def run(test,
+         use_fuzzy=False,
+         use_memory_slice=False,
+         use_address_reasoning=False):
+-
+-    initial_input = "%s/%s_0.dat" % (SCRIPT_DIR, test)
++    initial_input = os.path.join(SCRIPT_DIR, f"{test}_0.dat")
+     assert os.path.exists(initial_input)
+ 
+     env = os.environ.copy()
+@@ -36,14 +34,10 @@ def run(test,
+     native_time = None
+     if perf_run:
+         start = time.time()
+-        p = subprocess.Popen(
+-                                [
+-                                    SCRIPT_DIR + "/driver", test
+-                                ],
+-                                stderr=subprocess.DEVNULL,
+-                                stdin=subprocess.PIPE,
+-                                env=env
+-                            )
++        p = subprocess.Popen((os.path.join(SCRIPT_DIR, "driver"), test),
++                             stderr=subprocess.DEVNULL,
++                             stdin=subprocess.PIPE,
++                             env=env)
+         with open(initial_input, "rb") as f:
+             p.stdin.write(f.read())
+             p.stdin.close()
+@@ -51,27 +45,18 @@ def run(test,
+         end = time.time()
+         native_time = end - start
+ 
++    (workdir/'.fuzzolic_workdir').mkdir()
++    command = ['fuzzolic', '-o', workdir, '-i', initial_input, '-k']
++    if perf_run: command.extend(('-d', 'out'))
++    if use_lib_models: command.append('-l')
++    if use_fuzzy: command.append('-f')
++    if use_memory_slice: command.append('-s')
++    if use_address_reasoning: command.append('-r')
++    command.extend((os.path.join(SCRIPT_DIR, "driver"), test))
++    print(*command)
++
+     start = time.time()
+-    p = subprocess.Popen(
+-                            [
+-                                SCRIPT_DIR + "/../fuzzolic/fuzzolic.py",
+-                                "-o", WORKDIR,
+-                                "-i", initial_input,
+-                                "-k",
+-                            ] 
+-                            + (['-d', 'out'] if perf_run else []) 
+-                            + (['-l'] if use_lib_models else [])
+-                            + (['-f'] if use_fuzzy else [])
+-                            + (['-s'] if use_memory_slice else [])
+-                            + (['-r'] if use_address_reasoning else [])
+-                            + [
+-                                SCRIPT_DIR + "/driver", test
+-                            ],
+-                            stderr=subprocess.DEVNULL,
+-                            stdin=subprocess.DEVNULL,
+-                            env=env
+-                        )
+-    p.wait()
++    subprocess.run(command, env=env)
+     end = time.time()
+     emulated_time = end - start
+ 
+@@ -80,25 +65,17 @@ def run(test,
+         print("Slowdown: %s" % round(slowdown, 1))
+         assert slowdown < 70
+ 
+-    if expected_inputs > 0:
+-        testcases = glob.glob(WORKDIR + "/tests/test_*.dat") 
+-        assert len(testcases) == expected_inputs
+-    else:
+-        testcases = glob.glob(WORKDIR + "/fuzzolic-00000/test_*.dat")
++    testcases = tuple(workdir.glob('**/test_case_*.dat'))
++    assert len(testcases) >= expected_inputs
+ 
+     match = False
+-
+     if match_output:
+         for f in testcases:
+-            p = subprocess.Popen(
+-                                    [
+-                                        SCRIPT_DIR + "/driver", test
+-                                    ],
+-                                    stderr=subprocess.DEVNULL,
+-                                    stdin=subprocess.PIPE,
+-                                    stdout=subprocess.PIPE,
+-                                    env=env
+-                                )
++            p = subprocess.Popen([os.path.join(SCRIPT_DIR, "driver"), test],
++                                 stderr=subprocess.DEVNULL,
++                                 stdin=subprocess.PIPE,
++                                 stdout=subprocess.PIPE,
++                                 env=env)
+             with open(f, "rb") as fp:
+                 p.stdin.write(fp.read())
+             stdout = p.communicate()[0].decode("utf-8") 
+@@ -114,125 +91,142 @@ def run(test,
+     assert match
+ 
+ 
+-def test_simple_if(fuzzy):
+-    run("simple_if", use_fuzzy=fuzzy)
++def test_simple_if(tmp_path, fuzzy):
++    run("simple_if", tmp_path, use_fuzzy=fuzzy)
+ 
+ 
+-def test_nested_if(fuzzy):
+-    run("nested_if", expected_inputs=4, use_fuzzy=fuzzy)
++def test_nested_if(tmp_path, fuzzy):
++    run("nested_if", tmp_path, expected_inputs=4, use_fuzzy=fuzzy)
+ 
+ 
+-def test_mystrcmp(fuzzy):
++def test_mystrcmp(tmp_path, fuzzy):
+     # FixMe: to generate the correct input, we have to: 
+     #   (1) disable bitmap filtering
+     #   (2) start with a seed with enough bytes
+-    run("mystrcmp", use_duplicate_testcase_checker=True, expected_inputs=8, use_fuzzy=fuzzy)
++    run("mystrcmp", tmp_path, use_duplicate_testcase_checker=True,
++        expected_inputs=8, use_fuzzy=fuzzy)
+ 
+ 
+-def test_all_concrete(fuzzy):
++def test_all_concrete(tmp_path, fuzzy):
+     # performance test
+-    run("all_concrete", use_duplicate_testcase_checker=False, expected_inputs=1, perf_run=True, use_fuzzy=fuzzy)
++    run("all_concrete", tmp_path, perf_run=True,
++        use_duplicate_testcase_checker=False, use_fuzzy=fuzzy)
+ 
+ 
+-def test_div3(fuzzy):
++def test_div3(tmp_path, fuzzy):
+     if fuzzy:
+         pytest.skip("Fuzzy-SAT cannot deterministically solve this")
+-    run("div3", expected_inputs=1)
++    run("div3", tmp_path)
+ 
+ 
+-def test_addq(fuzzy):
+-    run("addq", expected_inputs=1, match_output=True, use_fuzzy=fuzzy)
++def test_addq(tmp_path, fuzzy):
++    run("addq", tmp_path, match_output=True, use_fuzzy=fuzzy)
+ 
+ 
+-def test_addl(fuzzy):
+-    run("addl", expected_inputs=1, match_output=True, use_fuzzy=fuzzy)
++def test_addl(tmp_path, fuzzy):
++    run("addl", tmp_path, match_output=True, use_fuzzy=fuzzy)
+ 
+ 
+-def test_addw(fuzzy):
+-    run("addw", expected_inputs=1, match_output=True, use_fuzzy=fuzzy)
++def test_addw(tmp_path, fuzzy):
++    run("addw", tmp_path, match_output=True, use_fuzzy=fuzzy)
+ 
+ 
+-def test_addb(fuzzy):
+-    run("addb", expected_inputs=1, match_output=True, use_fuzzy=fuzzy)
++def test_addb(tmp_path, fuzzy):
++    run("addb", tmp_path, match_output=True, use_fuzzy=fuzzy)
+ 
+ 
+-def test_adcq(fuzzy):
+-    run("adcq", expected_inputs=1, match_output=True, use_fuzzy=fuzzy)
++def test_adcq(tmp_path, fuzzy):
++    run("adcq", tmp_path, match_output=True, use_fuzzy=fuzzy)
+ 
+ 
+-def test_adcl(fuzzy):
+-    run("adcl", expected_inputs=1, match_output=True, use_fuzzy=fuzzy)
++def test_adcl(tmp_path, fuzzy):
++    run("adcl", tmp_path, match_output=True, use_fuzzy=fuzzy)
+ 
+ 
+-def test_adcw(fuzzy):
+-    run("adcw", expected_inputs=1, match_output=True, use_fuzzy=fuzzy)
++def test_adcw(tmp_path, fuzzy):
++    run("adcw", tmp_path, match_output=True, use_fuzzy=fuzzy)
+ 
+ 
+-def test_adcb(fuzzy):
+-    run("adcb", expected_inputs=1, match_output=True, use_fuzzy=fuzzy)
++def test_adcb(tmp_path, fuzzy):
++    run("adcb", tmp_path, match_output=True, use_fuzzy=fuzzy)
+ 
+ 
+-def test_model_strcmp(fuzzy):
+-    run("model_strcmp", expected_inputs=1, match_output=True, use_lib_models=True, use_fuzzy=fuzzy)
++def test_model_strcmp(tmp_path, fuzzy):
++    run("model_strcmp", tmp_path, match_output=True,
++        use_lib_models=True, use_fuzzy=fuzzy)
+ 
+ 
+-def test_model_strncmp(fuzzy):
+-    run("model_strncmp", expected_inputs=1, match_output=True, use_lib_models=True, use_fuzzy=fuzzy)
++def test_model_strncmp(tmp_path, fuzzy):
++    run("model_strncmp", tmp_path, match_output=True,
++        use_lib_models=True, use_fuzzy=fuzzy)
+ 
+ 
+-def test_model_strlen(fuzzy):
+-    run("model_strlen", expected_inputs=1, match_output=True, use_lib_models=True, use_fuzzy=fuzzy)
++def test_model_strlen(tmp_path, fuzzy):
++    run("model_strlen", tmp_path, match_output=True,
++        use_lib_models=True, use_fuzzy=fuzzy)
+ 
+ 
+-def test_model_strnlen_v0(fuzzy):
+-    run("model_strnlen_v0", expected_inputs=1, match_output=True, use_lib_models=True, use_fuzzy=fuzzy)
++def test_model_strnlen_v0(tmp_path, fuzzy):
++    run("model_strnlen_v0", tmp_path, match_output=True,
++        use_lib_models=True, use_fuzzy=fuzzy)
+ 
+ 
+-def test_model_strnlen_v1(fuzzy):
+-    run("model_strnlen_v1", expected_inputs=1, match_output=True, use_lib_models=True, use_fuzzy=fuzzy)
++def test_model_strnlen_v1(tmp_path, fuzzy):
++    run("model_strnlen_v1", tmp_path, match_output=True,
++        use_lib_models=True, use_fuzzy=fuzzy)
+ 
+ 
+-def test_model_memcmp_v0(fuzzy):
+-    run("model_memcmp_v0", expected_inputs=1, match_output=True, use_lib_models=True, use_fuzzy=fuzzy)
++def test_model_memcmp_v0(tmp_path, fuzzy):
++    run("model_memcmp_v0", tmp_path, match_output=True,
++        use_lib_models=True, use_fuzzy=fuzzy)
+ 
+ 
+-def test_model_memcmp_v1(fuzzy):
+-    run("model_memcmp_v1", expected_inputs=1, match_output=True, use_lib_models=True, use_fuzzy=fuzzy)
++def test_model_memcmp_v1(tmp_path, fuzzy):
++    run("model_memcmp_v1", tmp_path, match_output=True,
++        use_lib_models=True, use_fuzzy=fuzzy)
+ 
+ 
+-def test_model_memchr(fuzzy):
+-    run("model_memchr", expected_inputs=1, match_output=True, use_lib_models=True, use_fuzzy=fuzzy)
++def test_model_memchr(tmp_path, fuzzy):
++    run("model_memchr", tmp_path, match_output=True,
++        use_lib_models=True, use_fuzzy=fuzzy)
+ 
+ 
+-def test_symbolic_index(fuzzy):
++def test_symbolic_index(tmp_path, fuzzy):
+     pytest.skip("This test requires to build the tracer with memory slice support")
+-    run("symbolic_index", expected_inputs=1, use_fuzzy=fuzzy, use_memory_slice=True)
++    run("symbolic_index", tmp_path, use_fuzzy=fuzzy,
++        use_memory_slice=True)
+ 
+ 
+-def test_symbolic_read(fuzzy):
+-    run("symbolic_read", expected_inputs=2, match_output=True, use_fuzzy=fuzzy, use_memory_slice=True)
++def test_symbolic_read(tmp_path, fuzzy):
++    run("symbolic_read", tmp_path, expected_inputs=2, match_output=True,
++        use_fuzzy=fuzzy, use_memory_slice=True)
+ 
+ 
+-def test_switch(fuzzy):
++def test_switch(tmp_path, fuzzy):
+     pytest.skip("This test requires to build the tracer with memory slice support")
+-    run("switch", expected_inputs=7, match_output=True, use_fuzzy=fuzzy, use_address_reasoning=True)
++    run("switch", tmp_path, expected_inputs=7, match_output=True,
++        use_fuzzy=fuzzy, use_address_reasoning=True)
+ 
+ 
+-def test_model_malloc_min(fuzzy):
++def test_model_malloc_min(tmp_path, fuzzy):
+     pytest.skip("We need to revise this test")
+-    run("model_malloc_min", expected_inputs=0, match_output=True, use_lib_models=True, use_fuzzy=fuzzy)
++    run("model_malloc_min", tmp_path, expected_inputs=0, match_output=True,
++        use_lib_models=True, use_fuzzy=fuzzy)
+ 
+ 
+-def test_model_malloc_max(fuzzy):
++def test_model_malloc_max(tmp_path, fuzzy):
+     pytest.skip("We need to revise this test")
+-    run("model_malloc_max", expected_inputs=0, match_output=True, use_lib_models=True, use_fuzzy=fuzzy)
++    run("model_malloc_max", tmp_path, expected_inputs=0, match_output=True,
++        use_lib_models=True, use_fuzzy=fuzzy)
+ 
+ 
+-def test_model_realloc_min(fuzzy):
++def test_model_realloc_min(tmp_path, fuzzy):
+     pytest.skip("We need to revise this test")
+-    run("model_realloc_min", expected_inputs=0, match_output=True, use_lib_models=True, use_fuzzy=fuzzy)
++    run("model_realloc_min", tmp_path, expected_inputs=0, match_output=True,
++        use_lib_models=True, use_fuzzy=fuzzy)
+ 
+ 
+-def test_model_realloc_max(fuzzy):
++def test_model_realloc_max(tmp_path, fuzzy):
+     pytest.skip("We need to revise this test")
+-    run("model_realloc_max", expected_inputs=0, match_output=True, use_lib_models=True, use_fuzzy=fuzzy)
++    run("model_realloc_max", tmp_path, expected_inputs=0, match_output=True,
++        use_lib_models=True, use_fuzzy=fuzzy)
diff --git a/patches/fuzzolic-test-skip-nondeterministic.patch b/patches/fuzzolic-test-skip-nondeterministic.patch
new file mode 100644
index 0000000..2d390db
--- /dev/null
+++ b/patches/fuzzolic-test-skip-nondeterministic.patch
@@ -0,0 +1,23 @@
+commit 8350c6e96aba15b548ecd423b99b88da35310645
+Author: Nguyễn Gia Phong <cnx@loang.net>
+Date:   2025-05-08 11:23:51 +0900
+
+    Skip nondeterministic test
+    
+    Test div3 probably used to depend on an implementation detail of Z3
+    that is no longer present.
+
+diff --git a/tests/run.py b/tests/run.py
+index 0b69d990faf5..7db888dfa973 100755
+--- a/tests/run.py
++++ b/tests/run.py
+@@ -114,8 +114,7 @@ def test_all_concrete(tmp_path, fuzzy):
+ 
+ 
+ def test_div3(tmp_path, fuzzy):
+-    if fuzzy:
+-        pytest.skip("Fuzzy-SAT cannot deterministically solve this")
++    pytest.skip("Not deterministic")
+     run("div3", tmp_path)
+ 
+ 
diff --git a/patches/fuzzolic-timeout-solver.patch b/patches/fuzzolic-timeout-solver.patch
new file mode 100644
index 0000000..95b971b
--- /dev/null
+++ b/patches/fuzzolic-timeout-solver.patch
@@ -0,0 +1,22 @@
+From f06525aaf9790b0eecef317e4aaf444189e6042b Mon Sep 17 00:00:00 2001
+From: Andrew Haberlandt <ahaberla@andrew.cmu.edu>
+Date: Sun, 19 May 2024 06:46:05 +0000
+Subject: [PATCH] fix: executor fails to kill solver if it hangs
+
+---
+ fuzzolic/executor.py | 2 +-
+ 1 file changed, 1 insertion(+), 1 deletion(-)
+
+diff --git a/fuzzolic/executor.py b/fuzzolic/executor.py
+index 39c6aa6..e660314 100644
+--- a/fuzzolic/executor.py
++++ b/fuzzolic/executor.py
+@@ -449,7 +449,7 @@ def fuzz_one(self, testcase, target, force_smt=False):
+                 print('[FUZZOLIC] Solver is taking too long. Let us stop it.')
+                 p_solver.send_signal(signal.SIGUSR2)
+                 try:
+-                    p_solver.wait(SOLVER_TIMEOUT)
++                    p_solver.wait(SOLVER_TIMEOUT / 1000)
+                 except subprocess.TimeoutExpired:
+                     print('[FUZZOLIC] Solver will be killed.')
+                     p_solver.send_signal(signal.SIGKILL)
diff --git a/patches/fuzzolic-unbundle.patch b/patches/fuzzolic-unbundle.patch
new file mode 100644
index 0000000..803f621
--- /dev/null
+++ b/patches/fuzzolic-unbundle.patch
@@ -0,0 +1,108 @@
+commit 24044a2d0341cfdd3c7cc7320cbbd49591ef28ce
+Author: Nguyễn Gia Phong <cnx@loang.net>
+Date:   2025-04-29 16:44:20 +0900
+
+    Unbundle required utilities
+
+diff --git a/fuzzolic/executor.py b/fuzzolic/executor.py
+index f2639eb8da6a..06d0253a3b07 100644
+--- a/fuzzolic/executor.py
++++ b/fuzzolic/executor.py
+@@ -21,14 +21,9 @@ from . import minimizer_qsym
+ from . import minimizer
+ 
+ SCRIPT_DIR = os.path.dirname(os.path.realpath(__file__))
+-SOLVER_SMT_BIN = SCRIPT_DIR + '/../solver/solver-smt'
+-SOLVER_FUZZY_BIN = SCRIPT_DIR + '/../solver/solver-fuzzy'
+-TRACER_BIN = SCRIPT_DIR + '/../tracer/x86_64-linux-user/qemu-x86_64'
+-
+-if 'AFL_PATH' not in os.environ:
+-    AFL_PATH = SCRIPT_DIR + '/../../AFLplusplus/'
+-else:
+-    AFL_PATH = os.environ['AFL_PATH']
++SOLVER_SMT_BIN = 'solver-smt'
++SOLVER_FUZZY_BIN = 'solver-fuzzy'
++TRACER_BIN = 'qemu-x86_64'
+ 
+ SOLVER_WAIT_TIME_AT_STARTUP = 0.0010
+ SOLVER_TIMEOUT = 1000
+@@ -84,15 +79,12 @@ class Executor(object):
+                 sys.exit('ERROR: invalid AFL workdir')
+             self.afl = os.path.abspath(afl)
+             self.minimizer = minimizer_qsym.TestcaseMinimizer(
+-                [binary] + binary_args, AFL_PATH, output_dir, True, input_fixed_name)
++                [binary] + binary_args, output_dir, True, input_fixed_name)
+             #  self.minimizer = minimizer.TestcaseMinimizer([binary] + binary_args, self.global_bitmap)
+         else:
+             self.afl = None
+-            if minimizer_qsym.is_afl_showmap_available():
+-                self.minimizer = minimizer_qsym.TestcaseMinimizer(
+-                    [binary] + binary_args, AFL_PATH, output_dir, True, input_fixed_name)
+-            else:
+-                self.minimizer = minimizer.TestcaseMinimizer([binary] + binary_args, self.global_bitmap)
++            self.minimizer = minimizer_qsym.TestcaseMinimizer(
++                [binary] + binary_args, output_dir, True, input_fixed_name)
+ 
+         self.afl_processed_testcases = set()
+         self.afl_alt_processed_testcases = set()
+@@ -126,16 +118,8 @@ class Executor(object):
+ 
+         if use_symbolic_models:
+             plt_info_file = self.__get_root_dir() + "/plt_info.txt"
+-            p = subprocess.Popen(
+-                                [
+-                                    SCRIPT_DIR + "/find_models_addrs.py",
+-                                    "-o", plt_info_file,
+-                                    binary
+-                                ],
+-                                # stderr=subprocess.DEVNULL,
+-                                # stdin=subprocess.DEVNULL,
+-                                )
+-            p.wait()
++            subprocess.run(["fuzzolic-find-models-addrs",
++                            "-o", plt_info_file, binary])
+             self.plt_info = plt_info_file
+         else:
+             self.plt_info = None
+diff --git a/fuzzolic/minimizer_qsym.py b/fuzzolic/minimizer_qsym.py
+index 6d0170577392..1c31df0b9f0a 100644
+--- a/fuzzolic/minimizer_qsym.py
++++ b/fuzzolic/minimizer_qsym.py
+@@ -81,15 +81,13 @@ def fix_at_file(cmd, testcase):
+ 
+     return cmd, stdin
+ 
+-def is_afl_showmap_available():
+-    return os.path.exists(os.path.join(SCRIPT_DIR, "../utils/afl-showmap"))
+ 
+ class TestcaseMinimizer(object):
+-    def __init__(self, cmd, afl_path, out_dir, qemu_mode, fixed_name, map_size=MAP_SIZE):
++    def __init__(self, cmd, out_dir, qemu_mode, fixed_name, map_size=MAP_SIZE):
+         self.cmd = cmd
+         self.qemu_mode = qemu_mode
+-        self.showmap = os.path.join(afl_path, "afl-showmap")
+-        self.showmap_fork = os.path.join(SCRIPT_DIR, "../utils/afl-showmap")
++        self.showmap = "afl-showmap"
++        self.showmap_fork = "fuzzolic-showmap"
+         self.bitmap_file = os.path.join(out_dir, "afl-bitmap")
+         self.crash_bitmap_file = os.path.join(out_dir, "afl-crash-bitmap")
+         _, self.temp_file = tempfile.mkstemp(dir=out_dir)
+@@ -225,16 +223,8 @@ class TestcaseMinimizer(object):
+         return interesting
+ 
+     def is_interesting_testcase_fork(self, bitmap, my_bitmap_file=None):
+-        if my_bitmap_file is None:
+-            my_bitmap_file = self.bitmap_file
+-
+-        cmd = [
+-            SCRIPT_DIR + '/../utils/merge_bitmap',
+-            bitmap,
+-            my_bitmap_file
+-        ]
+-        # print(cmd)
+-
++        cmd = ('fuzzolic-merge-bitmap', bitmap,
++               my_bitmap_file or self.bitmap_file)
+         with open(os.devnull, "wb") as devnull:
+             proc = sp.Popen(cmd, stdin=None, stdout=devnull, stderr=devnull)
+             proc.wait()
diff --git a/patches/fuzzolic-utils-make.patch b/patches/fuzzolic-utils-make.patch
new file mode 100644
index 0000000..4a971a5
--- /dev/null
+++ b/patches/fuzzolic-utils-make.patch
@@ -0,0 +1,34 @@
+commit 1bfb2b78e56f953956f2125980992b91ad355774
+Author: Nguyễn Gia Phong <cnx@loang.net>
+Date:   2025-05-08 11:01:05 +0900
+
+    Build and install utilities
+
+diff --git a/Makefile b/Makefile
+index 395f7a387bd9..feaef92f3266 100644
+--- a/Makefile
++++ b/Makefile
+@@ -1,3 +1,23 @@
++.POSIX:
++.PHONY: all install
++
++PREFIX ?= /usr/local
++BINDIR ::= $(DESTDIR)$(PREFIX)/bin
++BIN ::= fuzzolic-merge-bitmap fuzzolic-find-models-addrs
++
++all: $(BIN)
++
++fuzzolic-find-models-addrs: fuzzolic/find_models_addrs.py
++	cp $< $@
++
++fuzzolic-merge-bitmap: utils/merge_bitmap.o
++	$(CC) $(LDFLAGS) $< $(LOADLIBES) $(LDLIBS) -o $@
++
++install: $(BIN:%=$(BINDIR)/%)
++
++$(BINDIR)/%: %
++	install -Dm 755 $< $@
++
+ simpleif: build clean-work-dir
+ 	./fuzzolic/fuzzolic.py -o workdir -i tests/simple_if_0.dat tests/driver simple_if
+ 	./utils/print_test_cases.py workdir/tests
diff --git a/patches/fuzzy-sat-install.patch b/patches/fuzzy-sat-install.patch
new file mode 100644
index 0000000..2c68cbc
--- /dev/null
+++ b/patches/fuzzy-sat-install.patch
@@ -0,0 +1,65 @@
+commit 3a8ce277d2f26409a1eb139641f0733979bd21ab
+Author: Nguyễn Gia Phong <cnx@loang.net>
+Date:   2025-04-24 13:10:50 +0900
+
+    Install libraries and tools
+
+diff --git a/CMakeLists.txt b/CMakeLists.txt
+index 7cfa95cc7174..695bc8757fa5 100644
+--- a/CMakeLists.txt
++++ b/CMakeLists.txt
+@@ -1,5 +1,5 @@
+ cmake_minimum_required(VERSION 3.7)
+-
++include(CMakePackageConfigHelpers)
+ set(CMAKE_POLICY_DEFAULT_CMP0077 NEW)
+ 
+ project(Z3Fuzzy)
+@@ -7,3 +7,10 @@ project(Z3Fuzzy)
+ set(Z3_BUILD_PYTHON_BINDINGS true)
+ add_subdirectory(lib)
+ add_subdirectory(tools)
++
++install(EXPORT Z3Fuzzy DESTINATION ${CMAKE_INSTALL_LIBDIR}/cmake/Z3Fuzzy)
++configure_package_config_file(${CMAKE_CURRENT_SOURCE_DIR}/Config.cmake.in
++  "${CMAKE_CURRENT_BINARY_DIR}/Z3FuzzyConfig.cmake"
++  INSTALL_DESTINATION ${CMAKE_INSTALL_LIBDIR}/cmake/Z3Fuzzy)
++install(FILES "${CMAKE_CURRENT_BINARY_DIR}/Z3FuzzyConfig.cmake"
++        DESTINATION ${CMAKE_INSTALL_LIBDIR}/cmake/Z3Fuzzy)
+diff --git a/Config.cmake.in b/Config.cmake.in
+new file mode 100644
+index 000000000000..64b0eaa487fb
+--- /dev/null
++++ b/Config.cmake.in
+@@ -0,0 +1,3 @@
++@PACKAGE_INIT@
++include("${CMAKE_CURRENT_LIST_DIR}/Z3Fuzzy.cmake")
++check_required_components(Z3Fuzzy)
+diff --git a/lib/CMakeLists.txt b/lib/CMakeLists.txt
+index 558c01b7c725..c30f0f41206a 100644
+--- a/lib/CMakeLists.txt
++++ b/lib/CMakeLists.txt
+@@ -31,7 +31,9 @@ target_link_libraries(Z3Fuzzy_static
+ target_link_libraries(Z3Fuzzy_shared
+                       PUBLIC ${XXHASH_LIBRARIES}
+                       PUBLIC ${Z3_LIBRARIES})
+-set_target_properties(Z3Fuzzy_static PROPERTIES OUTPUT_NAME Z3Fuzzy)
+-set_target_properties(Z3Fuzzy_shared PROPERTIES OUTPUT_NAME Z3Fuzzy)
++set_target_properties(Z3Fuzzy_static PROPERTIES OUTPUT_NAME Z3Fuzzy
++                      PUBLIC_HEADER z3-fuzzy.h)
++set_target_properties(Z3Fuzzy_shared PROPERTIES OUTPUT_NAME Z3Fuzzy
++                      PUBLIC_HEADER z3-fuzzy.h)
+ 
+-install(FILES z3-fuzzy.h DESTINATION include)
++install(TARGETS Z3Fuzzy_shared Z3Fuzzy_static EXPORT Z3Fuzzy)
+diff --git a/tools/CMakeLists.txt b/tools/CMakeLists.txt
+index a9c1a07fc541..732818c3ad9e 100644
+--- a/tools/CMakeLists.txt
++++ b/tools/CMakeLists.txt
+@@ -27,3 +27,6 @@ add_executable(stats-collection-z3
+     stats-collection-z3.c
+     pretty-print.c)
+ LinkBin(stats-collection-z3)
++
++install(TARGETS fuzzy-solver fuzzy-solver-vs-z3
++        stats-collection-fuzzy stats-collection-z3)
diff --git a/patches/fuzzy-sat-unbundle.patch b/patches/fuzzy-sat-unbundle.patch
new file mode 100644
index 0000000..116369d
--- /dev/null
+++ b/patches/fuzzy-sat-unbundle.patch
@@ -0,0 +1,346 @@
+commit 6033d69cf4826ced4f94e7b1543a2bb0ab7a5cbc
+Author: Nguyễn Gia Phong <cnx@loang.net>
+Date:   2025-04-24 11:34:16 +0900
+
+    Unbundle xxHash and Fuzzolic Z3
+
+diff --git a/CMakeLists.txt b/CMakeLists.txt
+index 13622ddc6ff4..7cfa95cc7174 100644
+--- a/CMakeLists.txt
++++ b/CMakeLists.txt
+@@ -5,6 +5,5 @@ set(CMAKE_POLICY_DEFAULT_CMP0077 NEW)
+ project(Z3Fuzzy)
+ 
+ set(Z3_BUILD_PYTHON_BINDINGS true)
+-add_subdirectory(fuzzolic-z3)
+ add_subdirectory(lib)
+ add_subdirectory(tools)
+diff --git a/lib/CMakeLists.txt b/lib/CMakeLists.txt
+index df3a4fa9a614..558c01b7c725 100644
+--- a/lib/CMakeLists.txt
++++ b/lib/CMakeLists.txt
+@@ -1,5 +1,9 @@
+ cmake_minimum_required(VERSION 3.7)
+ 
++find_package(PkgConfig REQUIRED)
++pkg_check_modules(XXHASH REQUIRED libxxhash)
++find_package(Z3 REQUIRED)
++
+ # Strip the binary in release mode
+ set(CMAKE_C_FLAGS_RELEASE "${CMAKE_C_FLAGS_RELEASE} -s")
+ 
+@@ -18,9 +22,15 @@ set_property(TARGET objZ3FuzzyLib PROPERTY POSITION_INDEPENDENT_CODE 1)
+ add_library(Z3Fuzzy_static STATIC $<TARGET_OBJECTS:objZ3FuzzyLib>)
+ add_library(Z3Fuzzy_shared SHARED $<TARGET_OBJECTS:objZ3FuzzyLib>)
+ 
+-target_include_directories (objZ3FuzzyLib PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/../fuzzolic-z3/src/api")
+-target_link_libraries (Z3Fuzzy_shared LINK_PUBLIC libz3)
+-
++target_include_directories(objZ3FuzzyLib
++                           PUBLIC ${Z3_C_INCLUDE_DIRS}
++                           PUBLIC ${XXHASH_C_INCLUDE_DIRS})
++target_link_libraries(Z3Fuzzy_static
++                      PRIVATE ${XXHASH_LIBRARIES}
++                      PRIVATE ${Z3_LIBRARIES})
++target_link_libraries(Z3Fuzzy_shared
++                      PUBLIC ${XXHASH_LIBRARIES}
++                      PUBLIC ${Z3_LIBRARIES})
+ set_target_properties(Z3Fuzzy_static PROPERTIES OUTPUT_NAME Z3Fuzzy)
+ set_target_properties(Z3Fuzzy_shared PROPERTIES OUTPUT_NAME Z3Fuzzy)
+ 
+diff --git a/lib/z3-fuzzy.c b/lib/z3-fuzzy.c
+index 69ecb006fd1f..b5cb8206ebb5 100644
+--- a/lib/z3-fuzzy.c
++++ b/lib/z3-fuzzy.c
+@@ -1,6 +1,7 @@
+ #define FUZZY_SOURCE
+ 
+ #include <fcntl.h>
++#include <stdbool.h>
+ #include <stdio.h>
+ #include <stdlib.h>
+ #include <unistd.h>
+@@ -92,7 +93,7 @@ static int performing_aggressive_optimistic = 0;
+ #ifdef USE_MD5_HASH
+ #include "md5.h"
+ #else
+-#include "xxhash/xxh3.h"
++#include <xxhash.h>
+ #endif
+ 
+ // generate parametric data structures
+@@ -1491,18 +1492,18 @@ static int __detect_input_group(fuzzy_ctx_t* ctx, Z3_ast node,
+                     unsigned long mask;
+                     if (Z3_get_ast_kind(ctx->z3_ctx, child_1) ==
+                         Z3_NUMERAL_AST) {
+-                        Z3_bool successGet = Z3_get_numeral_uint64(
++                        bool successGet = Z3_get_numeral_uint64(
+                             ctx->z3_ctx, child_1, (uint64_t*)&mask);
+-                        if (successGet == Z3_FALSE) {
++                        if (successGet == false) {
+                             res = 0;
+                             goto BVAND_EXIT;
+                         }
+                         subexpr = child_2;
+                     } else if (Z3_get_ast_kind(ctx->z3_ctx, child_2) ==
+                                Z3_NUMERAL_AST) {
+-                        Z3_bool successGet = Z3_get_numeral_uint64(
++                        bool successGet = Z3_get_numeral_uint64(
+                             ctx->z3_ctx, child_2, (uint64_t*)&mask);
+-                        if (successGet == Z3_FALSE) {
++                        if (successGet == false) {
+                             res = 0; // constant is too big
+                             goto BVAND_EXIT;
+                         }
+@@ -1668,7 +1669,7 @@ static int __detect_input_group(fuzzy_ctx_t* ctx, Z3_ast node,
+                                 Z3_ast subexpr = NULL;
+                                 if (Z3_get_ast_kind(ctx->z3_ctx, child_2) ==
+                                     Z3_NUMERAL_AST) {
+-                                    Z3_bool successGet = Z3_get_numeral_uint64(
++                                    bool successGet = Z3_get_numeral_uint64(
+                                         ctx->z3_ctx, child_2,
+                                         (uint64_t*)&shift_val);
+                                     if (!successGet)
+@@ -1806,7 +1807,7 @@ static int __detect_input_group(fuzzy_ctx_t* ctx, Z3_ast node,
+         }
+         case Z3_NUMERAL_AST: {
+             // uint64_t v;
+-            // Z3_bool  successGet =
++            // bool     successGet =
+             //     Z3_get_numeral_uint64(ctx->z3_ctx, node, (uint64_t*)&v);
+             // if (!successGet || v != 0)
+             //     *approx = 1;
+@@ -1918,9 +1919,9 @@ static void __detect_input_to_state_query(fuzzy_ctx_t* ctx, Z3_ast node,
+     Z3_ast   other_child = Z3_get_app_arg(ctx->z3_ctx, node_app, const_operand);
+     Z3_inc_ref(ctx->z3_ctx, other_child);
+     if (Z3_get_ast_kind(ctx->z3_ctx, other_child) == Z3_NUMERAL_AST) {
+-        Z3_bool successGet = Z3_get_numeral_uint64(
++        bool successGet = Z3_get_numeral_uint64(
+             ctx->z3_ctx, other_child, (uint64_t*)&data->input_to_state_const);
+-        if (successGet == Z3_FALSE) {
++        if (successGet == false) {
+             Z3_dec_ref(ctx->z3_ctx, other_child);
+             data->is_input_to_state = 0;
+             return; // constant is too big
+@@ -2308,7 +2309,7 @@ static void __detect_early_constants(fuzzy_ctx_t* ctx, Z3_ast v,
+     unsigned long tmp_const;
+     switch (Z3_get_ast_kind(ctx->z3_ctx, v)) {
+         case Z3_APP_AST: {
+-            Z3_bool      successGet;
++            bool         successGet;
+             Z3_ast       child1, child2;
+             Z3_app       app       = Z3_to_app(ctx->z3_ctx, v);
+             Z3_func_decl decl      = Z3_get_app_decl(ctx->z3_ctx, app);
+@@ -2364,7 +2365,7 @@ static void __detect_early_constants(fuzzy_ctx_t* ctx, Z3_ast v,
+                         Z3_NUMERAL_AST) {
+                         successGet = Z3_get_numeral_uint64(
+                             ctx->z3_ctx, child1, (uint64_t*)&tmp_const);
+-                        if (successGet == Z3_FALSE)
++                        if (successGet == false)
+                             break; // constant bigger than 64
+                         da_add_item__ulong(&data->values, tmp_const);
+                         da_add_item__ulong(&data->values, tmp_const + 1);
+@@ -2373,7 +2374,7 @@ static void __detect_early_constants(fuzzy_ctx_t* ctx, Z3_ast v,
+                                Z3_NUMERAL_AST) {
+                         successGet = Z3_get_numeral_uint64(
+                             ctx->z3_ctx, child2, (uint64_t*)&tmp_const);
+-                        if (successGet == Z3_FALSE)
++                        if (successGet == false)
+                             break; // constant bigger than 64
+                         da_add_item__ulong(&data->values, tmp_const);
+                         da_add_item__ulong(&data->values, tmp_const + 1);
+@@ -2400,8 +2401,7 @@ static void __detect_early_constants(fuzzy_ctx_t* ctx, Z3_ast v,
+                         Z3_NUMERAL_AST) {
+                         successGet = Z3_get_numeral_uint64(
+                             ctx->z3_ctx, child1, (uint64_t*)&tmp_const);
+-                        ASSERT_OR_ABORT(successGet == Z3_TRUE,
+-                                        "failed to get constant");
++                        ASSERT_OR_ABORT(successGet, "failed to get constant");
+                         da_add_item__ulong(&data->values, tmp_const);
+                         da_add_item__ulong(&data->values, tmp_const + 1);
+                         da_add_item__ulong(&data->values, tmp_const - 1);
+@@ -2409,8 +2409,7 @@ static void __detect_early_constants(fuzzy_ctx_t* ctx, Z3_ast v,
+                                Z3_NUMERAL_AST) {
+                         successGet = Z3_get_numeral_uint64(
+                             ctx->z3_ctx, child2, (uint64_t*)&tmp_const);
+-                        ASSERT_OR_ABORT(successGet == Z3_TRUE,
+-                                        "failed to get constant");
++                        ASSERT_OR_ABORT(successGet, "failed to get constant");
+                         da_add_item__ulong(&data->values, tmp_const);
+                         da_add_item__ulong(&data->values, tmp_const + 1);
+                         da_add_item__ulong(&data->values, tmp_const - 1);
+@@ -2527,9 +2526,9 @@ __detect_all_constants(fuzzy_ctx_t* ctx, Z3_ast v, ast_data_t* data)
+         }
+         case Z3_NUMERAL_AST: {
+             unsigned long tmp_const;
+-            Z3_bool       successGet =
++            bool          successGet =
+                 Z3_get_numeral_uint64(ctx->z3_ctx, v, (uint64_t*)&tmp_const);
+-            ASSERT_OR_ABORT(successGet == Z3_TRUE, "failed to get constant");
++            ASSERT_OR_ABORT(successGet, "failed to get constant");
+             da_add_item__ulong(&data->values, tmp_const);
+             da_add_item__ulong(&data->values, tmp_const + 1);
+             da_add_item__ulong(&data->values, tmp_const - 1);
+@@ -2695,9 +2694,9 @@ static inline int __find_child_constant(Z3_context ctx, Z3_app app,
+     for (i = 0; i < num_fields; ++i) {
+         Z3_ast child = Z3_get_app_arg(ctx, app, i);
+         if (Z3_get_ast_kind(ctx, child) == Z3_NUMERAL_AST) {
+-            Z3_bool successGet =
++            bool successGet =
+                 Z3_get_numeral_uint64(ctx, child, (uint64_t*)constant);
+-            if (successGet == Z3_FALSE)
++            if (successGet == false)
+                 return 0; // constant is too big
+             condition_ok   = 1;
+             *const_operand = i;
+@@ -2915,10 +2914,10 @@ static inline int __check_if_range(fuzzy_ctx_t* ctx, Z3_ast expr,
+ 
+             if (Z3_get_ast_kind(ctx->z3_ctx, tmp_expr) == Z3_NUMERAL_AST) {
+                 uint64_t v;
+-                Z3_bool  successGet =
++                bool     successGet =
+                     Z3_get_numeral_uint64(ctx->z3_ctx, tmp_expr, &v);
+ 
+-                if (successGet != Z3_FALSE && v == 0) {
++                if (successGet != false && v == 0) {
+                     has_zext                     = 1;
+                     Z3_ast old_non_const_operand = non_const_operand;
+                     non_const_operand =
+@@ -3163,7 +3162,7 @@ static inline int __detect_strcmp_pattern(fuzzy_ctx_t* ctx, Z3_ast ast,
+                 ...
+                 (ite (= inp_i const_i) #b1 #b0)))
+     */
+-    Z3_bool     successGet;
++    bool        successGet;
+     unsigned    i;
+     Z3_ast_kind kind = Z3_get_ast_kind(ctx->z3_ctx, ast);
+     if (kind != Z3_APP_AST)
+@@ -8353,14 +8352,14 @@ unsigned long z3fuzz_evaluate_expression_z3(fuzzy_ctx_t* ctx, Z3_ast query,
+ 
+     // evaluate the query in the model
+     Z3_ast  solution;
+-    Z3_bool successfulEval =
+-        Z3_model_eval(ctx->z3_ctx, z3_m, query, Z3_TRUE, &solution);
++    bool successfulEval =
++        Z3_model_eval(ctx->z3_ctx, z3_m, query, true, &solution);
+     ASSERT_OR_ABORT(successfulEval, "Failed to evaluate model");
+ 
+     Z3_model_dec_ref(ctx->z3_ctx, z3_m);
+     if (Z3_get_ast_kind(ctx->z3_ctx, solution) == Z3_NUMERAL_AST) {
+-        Z3_bool successGet = Z3_get_numeral_uint64(ctx->z3_ctx, solution, &res);
+-        ASSERT_OR_ABORT(successGet == Z3_TRUE,
++        bool successGet = Z3_get_numeral_uint64(ctx->z3_ctx, solution, &res);
++        ASSERT_OR_ABORT(successGet,
+                         "z3fuzz_evaluate_expression_z3() failed to get "
+                         "constant");
+     } else
+diff --git a/tools/CMakeLists.txt b/tools/CMakeLists.txt
+index 7af05f878bec..a9c1a07fc541 100644
+--- a/tools/CMakeLists.txt
++++ b/tools/CMakeLists.txt
+@@ -1,9 +1,10 @@
+ cmake_minimum_required(VERSION 3.7)
+ 
++find_package(Z3 REQUIRED)
+ macro(LinkBin exe_name)
+-    target_link_libraries(${exe_name} LINK_PUBLIC libz3)
++    target_link_libraries(${exe_name} LINK_PUBLIC ${Z3_LIBRARIES})
+     target_link_libraries(${exe_name} LINK_PUBLIC Z3Fuzzy_static)
+-    target_include_directories(${exe_name} PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/../fuzzolic-z3/src/api")
++    target_include_directories(${exe_name} PUBLIC ${Z3_C_INCLUDE_DIRS})
+     target_include_directories(${exe_name} PUBLIC "${CMAKE_CURRENT_SOURCE_DIR}/../lib")
+ endmacro()
+ 
+diff --git a/tools/fuzzy-solver-notify.c b/tools/fuzzy-solver-notify.c
+index 97abd8f71488..c0cca0ecb6ee 100644
+--- a/tools/fuzzy-solver-notify.c
++++ b/tools/fuzzy-solver-notify.c
+@@ -1,5 +1,6 @@
+ #define FUZZY_SOURCE
+ 
++#include <stdbool.h>
+ #include <stdio.h>
+ #include <stdlib.h>
+ #include <assert.h>
+@@ -119,8 +120,8 @@ static uint64_t Z3_eval(Z3_context ctx, Z3_ast query, uint64_t* data,
+ 
+     // evaluate the query in the model
+     Z3_ast  solution;
+-    Z3_bool successfulEval =
+-        Z3_model_eval(ctx, z3_m, query, Z3_TRUE, &solution);
++    bool    successfulEval =
++        Z3_model_eval(ctx, z3_m, query, true, &solution);
+     if (!successfulEval) {
+         puts("Failed to evaluate model");
+         exit(1);
+@@ -128,8 +129,8 @@ static uint64_t Z3_eval(Z3_context ctx, Z3_ast query, uint64_t* data,
+ 
+     Z3_model_dec_ref(ctx, z3_m);
+     if (Z3_get_ast_kind(ctx, solution) == Z3_NUMERAL_AST) {
+-        Z3_bool successGet = Z3_get_numeral_uint64(ctx, solution, &res);
+-        if (successGet != Z3_TRUE) {
++        bool successGet = Z3_get_numeral_uint64(ctx, solution, &res);
++        if (successGet != true) {
+             puts("Z3_get_numeral_uint64() failed to get constant");
+             exit(1);
+         }
+diff --git a/tools/maxmin-driver.c b/tools/maxmin-driver.c
+index 2e32f6410f68..26963f780223 100644
+--- a/tools/maxmin-driver.c
++++ b/tools/maxmin-driver.c
+@@ -1,3 +1,4 @@
++#include <stdbool.h>
+ #include <stdlib.h>
+ #include <assert.h>
+ #include <sys/time.h>
+@@ -36,14 +37,14 @@ static inline void dump_proof(Z3_context ctx, Z3_model m,
+         Z3_ast    s_bv = Z3_mk_const(ctx, s, bsort);
+ 
+         Z3_ast  solution;
+-        Z3_bool successfulEval =
++        bool    successfulEval =
+             Z3_model_eval(ctx, m, s_bv,
+-                          /*model_completion=*/Z3_TRUE, &solution);
++                          /*model_completion=*/true, &solution);
+         assert(successfulEval && "Failed to evaluate model");
+ 
+         int     solution_byte = 0;
+-        Z3_bool successGet = Z3_get_numeral_int(ctx, solution, &solution_byte);
+-        assert (successGet == Z3_TRUE);
++        bool    successGet = Z3_get_numeral_int(ctx, solution, &solution_byte);
++        assert (successGet);
+         fwrite(&solution_byte, sizeof(char), 1, fp);
+     }
+     fclose(fp);
+@@ -140,12 +141,12 @@ int main(int argc, char* argv[])
+             dump_proof(ctx, m, "tests/max_val_z3.bin");
+ 
+             Z3_ast  solution;
+-            Z3_bool successfulEval =
++            bool    successfulEval =
+                 Z3_model_eval(ctx, m, bv,
+-                              /*model_completion=*/Z3_TRUE, &solution);
++                              /*model_completion=*/true, &solution);
+             assert(successfulEval && "Failed to evaluate model");
+ 
+-            Z3_bool successGet = Z3_get_numeral_uint64(ctx, solution, &max_val_z3);
++            bool successGet = Z3_get_numeral_uint64(ctx, solution, &max_val_z3);
+             assert(successGet && "Failed to get numeral int");
+ 
+             Z3_model_dec_ref(ctx, m);
+@@ -172,12 +173,12 @@ int main(int argc, char* argv[])
+             dump_proof(ctx, m, "tests/min_val_z3.bin");
+ 
+             Z3_ast  solution;
+-            Z3_bool successfulEval =
++            bool    successfulEval =
+                 Z3_model_eval(ctx, m, bv,
+-                              /*model_completion=*/Z3_TRUE, &solution);
++                              /*model_completion=*/true, &solution);
+             assert(successfulEval && "Failed to evaluate model");
+ 
+-            Z3_bool successGet = Z3_get_numeral_uint64(ctx, solution, &min_val_z3);
++            bool successGet = Z3_get_numeral_uint64(ctx, solution, &min_val_z3);
+             assert(successGet && "Failed to get numeral int");
+             Z3_model_dec_ref(ctx, m);
+             break;
diff --git a/patches/qemu-for-fuzzolic-static-global.patch b/patches/qemu-for-fuzzolic-static-global.patch
new file mode 100644
index 0000000..0cb52af
--- /dev/null
+++ b/patches/qemu-for-fuzzolic-static-global.patch
@@ -0,0 +1,24 @@
+commit a0646eac1b56e4df51e7c6d2e99cb8807c59a1a3
+Author: Nguyễn Gia Phong <cnx@loang.net>
+Date:   2025-04-30 12:10:05 +0900
+
+    Avoid global variable in header
+    
+    Such global would be defined in each compilation unit including the header,
+    preventing them from being linked together.
+
+diff --git a/tcg/symbolic/symbolic-struct.h b/tcg/symbolic/symbolic-struct.h
+index 350522935bf9..684d32acfebd 100644
+--- a/tcg/symbolic/symbolic-struct.h
++++ b/tcg/symbolic/symbolic-struct.h
+@@ -503,9 +503,9 @@ static inline size_t get_opkind_width(OPKIND opkind)
+ }
+ 
+ #define MAX_PRINT_CHECK (1024 * 1024)
+-uint8_t            printed[MAX_PRINT_CHECK];
+ static inline void print_expr_internal(Expr* expr, uint8_t reset)
+ {
++    static uint8_t printed[MAX_PRINT_CHECK];
+     if (reset)
+         for (size_t i = 0; i < MAX_PRINT_CHECK; i++)
+             printed[i] = 0;
diff --git a/patches/qemu-for-fuzzolic-test-opts-range-beyond.patch b/patches/qemu-for-fuzzolic-test-opts-range-beyond.patch
new file mode 100644
index 0000000..9c7a4e0
--- /dev/null
+++ b/patches/qemu-for-fuzzolic-test-opts-range-beyond.patch
@@ -0,0 +1,97 @@
+commit 863f195fa823c0c20d734dadfc5908c2aea34330
+Author: Andrey Shinkevich <andrey.shinkevich@virtuozzo.com>
+Date:   2019-08-05 20:03:06 +0300
+
+    make check-unit: use after free in test-opts-visitor
+    
+    In the struct OptsVisitor, the 'repeated_opts' member points to a list
+    in the 'unprocessed_opts' hash table after the list has been destroyed.
+    A subsequent call to visit_type_int() references the deleted list.
+    It results in use-after-free issue reproduced by running the test case
+    under the Valgrind: valgrind tests/test-opts-visitor.
+    A new mode ListMode::LM_TRAVERSED is declared to mark the list
+    traversal completed.
+    
+    Suggested-by: Markus Armbruster <armbru@redhat.com>
+    Signed-off-by: Andrey Shinkevich <andrey.shinkevich@virtuozzo.com>
+    Message-Id: <1565024586-387112-1-git-send-email-andrey.shinkevich@virtuozzo.com>
+
+diff --git a/qapi/opts-visitor.c b/qapi/opts-visitor.c
+index 324b197495a0..5fe0276c1cc8 100644
+--- a/qapi/opts-visitor.c
++++ b/qapi/opts-visitor.c
+@@ -24,7 +24,8 @@ enum ListMode
+ {
+     LM_NONE,             /* not traversing a list of repeated options */
+ 
+-    LM_IN_PROGRESS,      /* opts_next_list() ready to be called.
++    LM_IN_PROGRESS,      /*
++                          * opts_next_list() ready to be called.
+                           *
+                           * Generating the next list link will consume the most
+                           * recently parsed QemuOpt instance of the repeated
+@@ -36,7 +37,8 @@ enum ListMode
+                           * LM_UNSIGNED_INTERVAL.
+                           */
+ 
+-    LM_SIGNED_INTERVAL,  /* opts_next_list() has been called.
++    LM_SIGNED_INTERVAL,  /*
++                          * opts_next_list() has been called.
+                           *
+                           * Generating the next list link will consume the most
+                           * recently stored element from the signed interval,
+@@ -48,7 +50,14 @@ enum ListMode
+                           * next element of the signed interval.
+                           */
+ 
+-    LM_UNSIGNED_INTERVAL /* Same as above, only for an unsigned interval. */
++    LM_UNSIGNED_INTERVAL, /* Same as above, only for an unsigned interval. */
++
++    LM_TRAVERSED          /*
++                           * opts_next_list() has been called.
++                           *
++                           * No more QemuOpt instance in the list.
++                           * The traversal has been completed.
++                           */
+ };
+ 
+ typedef enum ListMode ListMode;
+@@ -238,6 +247,8 @@ opts_next_list(Visitor *v, GenericList *tail, size_t size)
+     OptsVisitor *ov = to_ov(v);
+ 
+     switch (ov->list_mode) {
++    case LM_TRAVERSED:
++        return NULL;
+     case LM_SIGNED_INTERVAL:
+     case LM_UNSIGNED_INTERVAL:
+         if (ov->list_mode == LM_SIGNED_INTERVAL) {
+@@ -258,6 +269,8 @@ opts_next_list(Visitor *v, GenericList *tail, size_t size)
+         opt = g_queue_pop_head(ov->repeated_opts);
+         if (g_queue_is_empty(ov->repeated_opts)) {
+             g_hash_table_remove(ov->unprocessed_opts, opt->name);
++            ov->repeated_opts = NULL;
++            ov->list_mode = LM_TRAVERSED;
+             return NULL;
+         }
+         break;
+@@ -289,7 +302,8 @@ opts_end_list(Visitor *v, void **obj)
+ 
+     assert(ov->list_mode == LM_IN_PROGRESS ||
+            ov->list_mode == LM_SIGNED_INTERVAL ||
+-           ov->list_mode == LM_UNSIGNED_INTERVAL);
++           ov->list_mode == LM_UNSIGNED_INTERVAL ||
++           ov->list_mode == LM_TRAVERSED);
+     ov->repeated_opts = NULL;
+     ov->list_mode = LM_NONE;
+ }
+@@ -306,6 +320,10 @@ lookup_scalar(const OptsVisitor *ov, const char *name, Error **errp)
+         list = lookup_distinct(ov, name, errp);
+         return list ? g_queue_peek_tail(list) : NULL;
+     }
++    if (ov->list_mode == LM_TRAVERSED) {
++        error_setg(errp, "Fewer list elements than expected");
++        return NULL;
++    }
+     assert(ov->list_mode == LM_IN_PROGRESS);
+     return g_queue_peek_head(ov->repeated_opts);
+ }