Let tv pass the custom z3 log file path to start_logging
MODIFY
smt/smt.cpp
smt/smt.cpp
@@ -74,8 +74,8 @@ bool hit_half_memory_limit() {
return Z3_get_estimated_alloc_size() >= (z3_memory_limit / 2);
}
-void start_logging() {
- Z3_open_log("z3_log.txt");
+void start_logging(const char *path) {
+ Z3_open_log(path);
string str = string("Alive2 ") + alive_version;
Z3_append_log(str.c_str());
}

MODIFY
smt/smt.h
smt/smt.h
@@ -27,6 +27,6 @@ void set_memory_limit(uint64_t limit);
bool hit_memory_limit();
bool hit_half_memory_limit();
-void start_logging();
+void start_logging(const char *path = "z3_log.txt");
}

MODIFY
tv/tv.cpp
tv/tv.cpp
@@ -259,8 +259,18 @@ struct TVPass final : public llvm::FunctionPass {
report_filename = path;
*out << "Source: " << source_file << endl;
report_dir_created = true;
- } else if (opt_report_dir.empty())
+
+ if (opt_smt_log) {
+ fs::path path_z3log = path;
+ path_z3log.replace_extension("z3_log.txt");
+ smt::start_logging(path_z3log.c_str());
+ }
+ } else if (opt_report_dir.empty()) {
out = &cerr;
+ if (opt_smt_log) {
+ smt::start_logging();
+ }
+ }
showed_stats = false;
smt::solver_print_queries(opt_smt_verbose);
@@ -276,9 +286,6 @@ struct TVPass final : public llvm::FunctionPass {
config::debug = opt_debug;
llvm_util::omit_array_size = opt_omit_array_size;
- if (opt_smt_log)
- smt::start_logging();
-
llvm_util_init.emplace(*out, module.getDataLayout());
smt_init.emplace();
return false;

Let tv pass the custom z3 log file path to start_logging (#497)