diff --git a/README.md b/README.md
index eb35d2e..f8e23a4 100644
--- a/README.md
+++ b/README.md
@@ -36,6 +36,10 @@ 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
@@ -44,3 +48,4 @@ Then run `guix pull`.
[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 c5d3ec8..0ed0433 100644
--- a/REUSE.toml
+++ b/REUSE.toml
@@ -150,6 +150,7 @@ SPDX-License-Identifier = 'CC0-1.0'
path = [ 'patches/afl++-*.patch',
'patches/e9patch-*.patch',
'patches/evocatio-*.patch',
+ 'patches/fuzzy-sat-*.patch',
'patches/jasper-no-define-int-types.patch' ]
SPDX-FileCopyrightText = 'Nguyễn Gia Phong'
SPDX-License-Identifier = 'GPL-3.0-or-later'
diff --git a/loftix/deduction.scm b/loftix/deduction.scm
new file mode 100644
index 0000000..bea4420
--- /dev/null
+++ b/loftix/deduction.scm
@@ -0,0 +1,87 @@
+;;; 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 (gnu packages python-build)
+ #: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 z3-for-fuzzolic
+ (let* ((base z3)
+ (base-version "4.14.1")
+ (base-tag (string-append "z3-" base-version))
+ (revision "fuzzolic")
+ (commit "8a9e291dc2117e5cf48bdf2810f254000c6dd3d9")
+ (upstream "https://github.com/Z3Prover/z3"))
+ (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 "1qgfz4rz4xm1ivr5s0wz5d16mc1gr5yyc400sfbxm8r288pb56bq"))
+ (file-name (string-append name ".patch")))))))
+ (home-page "https://github.com/season-lab/z3")
+ (synopsis "Z3 for FUZZOLIC"))))
+
+(define-public fuzzy-sat
+ (let ((commit "5939b998a28ce2017b2c0dd89434792ab9ce5e51"))
+ (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 "1wm8sznv9w09vfb6nk1c4kbych34zpiywxkz37az81wsvpbwk82s"))
+ (patches (search-patches "patches/fuzzy-sat-include.patch"
+ "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 (not 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/patches/fuzzy-sat-include.patch b/patches/fuzzy-sat-include.patch
new file mode 100644
index 0000000..6798bbd
--- /dev/null
+++ b/patches/fuzzy-sat-include.patch
@@ -0,0 +1,83 @@
+commit bfd24f9cb93fab5317d16c879857221cc70e54c8
+Author: Nguyễn Gia Phong <cnx@loang.net>
+Date: 2025-04-24 11:25:20 +0900
+
+ Include stdio.h
+
+diff --git a/lib/testcase-list.c b/lib/testcase-list.c
+index 0aa223b7a7e4..6457fd5cab87 100644
+--- a/lib/testcase-list.c
++++ b/lib/testcase-list.c
+@@ -1,4 +1,5 @@
+ #include <fts.h>
++#include <stdio.h>
+ #include <stdlib.h>
+ #include "testcase-list.h"
+
+diff --git a/lib/z3-fuzzy-debug-utils.h b/lib/z3-fuzzy-debug-utils.h
+index 0f6f3b891a52..7b88add6c294 100644
+--- a/lib/z3-fuzzy-debug-utils.h
++++ b/lib/z3-fuzzy-debug-utils.h
+@@ -1,3 +1,5 @@
++#include <stdio.h>
++
+ static inline void print_index_queue(ast_info_ptr data)
+ {
+ index_group_t* group;
+diff --git a/lib/z3-fuzzy.c b/lib/z3-fuzzy.c
+index cac1c329088d..69ecb006fd1f 100644
+--- a/lib/z3-fuzzy.c
++++ b/lib/z3-fuzzy.c
+@@ -1,6 +1,7 @@
+ #define FUZZY_SOURCE
+
+ #include <fcntl.h>
++#include <stdio.h>
+ #include <stdlib.h>
+ #include <unistd.h>
+ #include "gradient_descend.h"
+diff --git a/tools/fuzzy-solver-notify.c b/tools/fuzzy-solver-notify.c
+index 821d3aaff15f..97abd8f71488 100644
+--- a/tools/fuzzy-solver-notify.c
++++ b/tools/fuzzy-solver-notify.c
+@@ -1,5 +1,6 @@
+ #define FUZZY_SOURCE
+
++#include <stdio.h>
+ #include <stdlib.h>
+ #include <assert.h>
+ #include <sys/time.h>
+diff --git a/tools/fuzzy-solver-vs-z3.c b/tools/fuzzy-solver-vs-z3.c
+index 8803ff390fa2..ba4e8f5b979a 100644
+--- a/tools/fuzzy-solver-vs-z3.c
++++ b/tools/fuzzy-solver-vs-z3.c
+@@ -1,3 +1,4 @@
++#include <stdio.h>
+ #include <stdlib.h>
+ #include <assert.h>
+ #include <sys/time.h>
+diff --git a/tools/stats-collection-fuzzy.c b/tools/stats-collection-fuzzy.c
+index fdef41761726..c793b1df717d 100644
+--- a/tools/stats-collection-fuzzy.c
++++ b/tools/stats-collection-fuzzy.c
+@@ -1,3 +1,4 @@
++#include <stdio.h>
+ #include <stdlib.h>
+ #include <assert.h>
+ #include <sys/time.h>
+diff --git a/tools/stats-collection-z3.c b/tools/stats-collection-z3.c
+index 504648a1a6c3..f101eeedb32f 100644
+--- a/tools/stats-collection-z3.c
++++ b/tools/stats-collection-z3.c
+@@ -1,3 +1,4 @@
++#include <stdio.h>
+ #include <stdlib.h>
+ #include <assert.h>
+ #include <sys/time.h>
+@@ -105,4 +106,4 @@ int main(int argc, char* argv[])
+ Z3_del_context(ctx);
+ fclose(log_file);
+ return 0;
+-}
+\ No newline at end of file
++}
diff --git a/patches/fuzzy-sat-install.patch b/patches/fuzzy-sat-install.patch
new file mode 100644
index 0000000..3ea77a1
--- /dev/null
+++ b/patches/fuzzy-sat-install.patch
@@ -0,0 +1,34 @@
+commit d36429fa541c69c566f981cd159b82f85d02b4fd
+Author: Nguyễn Gia Phong <cnx@loang.net>
+Date: 2025-04-24 13:10:50 +0900
+
+ Install libraries and tools
+
+diff --git a/lib/CMakeLists.txt b/lib/CMakeLists.txt
+index 558c01b7c725..aca4d9210862 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)
+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;
|
