generate smtlib bench even if skip_smt is on
MODIFY
smt/solver.cpp
smt/solver.cpp
@@ -294,11 +294,6 @@ Result Solver::check() const {
return Result::UNSAT;
}
- if (config::skip_smt) {
- ++num_skips;
- return Result::SKIP;
- }
-
if (!config::smt_benchmark_dir.empty()) {
const char *banner =
R"(Alive2 compiler optimization refinement query
@@ -316,6 +311,11 @@ Result Solver::check() const {
}
}
+ if (config::skip_smt) {
+ ++num_skips;
+ return Result::SKIP;
+ }
+
++num_queries;
if (print_queries)
cout << "\nSMT query:\n" << Z3_solver_to_string(ctx(), s) << endl;

generate smtlib bench even if skip_smt is on