mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

improve interrupts

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-10-11 18:10:38 -07:00
parent f7f4feaa47
commit e774634217
1 changed files with 11 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/shell/opt_frontend.cpp
View file

@ -309,12 +309,17 @@ static unsigned parse_opt(std::istream& in, bool is_wcnf) {
opb opb(opt, _in); opb opb(opt, _in);
opb.parse(); opb.parse();
} }
try {
lbool r = opt.optimize(); lbool r = opt.optimize();
switch (r) { switch (r) {
case l_true: std::cout << "sat\n"; break; case l_true: std::cout << "sat\n"; break;
case l_false: std::cout << "unsat\n"; break; case l_false: std::cout << "unsat\n"; break;
case l_undef: std::cout << "unknown\n"; break; case l_undef: std::cout << "unknown\n"; break;
} }
}
catch (z3_exception & ex) {
std::cerr << ex.msg() << "\n";
}
#pragma omp critical (g_display_stats) #pragma omp critical (g_display_stats)
{ {
display_statistics(); display_statistics();
@ -325,6 +330,7 @@ static unsigned parse_opt(std::istream& in, bool is_wcnf) {
} }
unsigned parse_opt(char const* file_name, bool is_wcnf) { unsigned parse_opt(char const* file_name, bool is_wcnf) {
g_first_interrupt = true;
g_start_time = static_cast<double>(clock()); g_start_time = static_cast<double>(clock());
register_on_timeout_proc(on_timeout); register_on_timeout_proc(on_timeout);
signal(SIGINT, on_ctrl_c); signal(SIGINT, on_ctrl_c);