alive tool: add -smt-to:xx
MODIFY
smt/ctx.cpp
smt/ctx.cpp
// Distributed under the MIT license that can be found in the LICENSE file.
#include "smt/ctx.h"
+#include "smt/smt.h"
#include <z3.h>
namespace smt {
@@ -10,8 +11,7 @@ context ctx;
void context::init() {
auto config = Z3_mk_config();
- // TODO: make this customizable
- Z3_set_param_value(config, "timeout", "1000");
+ Z3_set_param_value(config, "timeout", get_query_timeout());
ctx = Z3_mk_context_rc(config);
Z3_del_config(config);
}

MODIFY
smt/smt.cpp
smt/smt.cpp
@@ -16,4 +16,15 @@ smt_initializer::~smt_initializer() {
Z3_finalize_memory();
}
+
+static const char *query_timeout = "10000";
+
+void set_query_timeout(const char *ms) {
+ query_timeout = ms;
+}
+
+const char* get_query_timeout() {
+ return query_timeout;
+}
+
}

MODIFY
smt/smt.h
smt/smt.h
@@ -10,4 +10,8 @@ struct smt_initializer {
~smt_initializer();
};
+
+void set_query_timeout(const char *ms);
+const char* get_query_timeout();
+
}

MODIFY
tools/alive.cpp
tools/alive.cpp
@@ -21,11 +21,12 @@ static void show_help() {
cerr <<
"Usage: alive2 <options> <files.opt>\n"
"Options:\n"
- " -root-only:\tCheck the expression's root only\n"
- " -v:\t\tverbose mode\n"
- " -smt-stats:\tshow SMT statistics\n"
- " -skip-smt:\tassume all SMT queries are UNSAT\n"
- " -h / --help:\tshow this help\n";
+ " -root-only\tCheck the expression's root only\n"
+ " -v\t\tVerbose mode\n"
+ " -smt-stats\tShow SMT statistics\n"
+ " -smt-to:x\tTimeout for SMT queries in ms\n"
+ " -skip-smt\tAssume all SMT queries are UNSAT\n"
+ " -h / --help\tShow this help\n";
}
@@ -47,6 +48,8 @@ int main(int argc, char **argv) {
verbose = true;
else if (arg == "-smt-stats")
show_smt_stats = true;
+ else if (arg.compare(0, 8, "-smt-to:") == 0 && arg.size() > 8)
+ smt::set_query_timeout(arg.substr(8).data());
else if (arg == "-skip-smt")
config::skip_smt = true;
else if (arg == "-h" || arg == "--help") {

alive tool: add -smt-to:xx