diff --git a/src/test/smt2print_parse.cpp b/src/test/smt2print_parse.cpp index 765a78060..da4badf3e 100644 --- a/src/test/smt2print_parse.cpp +++ b/src/test/smt2print_parse.cpp @@ -64,26 +64,22 @@ void test_parseprint(char const* spec) { Z3_del_context(ctx); } +static bool is_error = false; +void setError(Z3_context c, Z3_error_code e) { + is_error = true; +} + void test_eval(Z3_context ctx, Z3_string spec, bool shouldFail) { std::cout << "spec:\n" << spec << "\n"; std::string resp; - bool failed = false; - try { - resp = Z3_eval_smtlib2_string(ctx, spec); - } - catch (std::runtime_error& e) { - resp = e.what(); - failed = true; - } - catch (...) { - resp = "unknown exception"; - failed = true; - } + is_error = false; + resp = Z3_eval_smtlib2_string(ctx, spec); - std::cout << "response:\n" << resp << "\n"; + if (!is_error) + std::cout << "response:\n" << resp << "\n"; - if (shouldFail != failed) { + if (shouldFail != is_error) { if (shouldFail) throw std::runtime_error("should have failed"); else @@ -91,9 +87,6 @@ void test_eval(Z3_context ctx, Z3_string spec, bool shouldFail) { } } -void throwError(Z3_context c, Z3_error_code e) { - throw std::runtime_error(Z3_get_error_msg(c, e)); -} void test_repeated_eval() { // Z3_eval_smtlib2_string reuses the parser and the scanner @@ -142,7 +135,7 @@ void test_repeated_eval() { "(pop)\n"; Z3_context ctx = Z3_mk_context(nullptr); - Z3_set_error_handler(ctx, throwError); + Z3_set_error_handler(ctx, setError); std::cout << "testing Z3_eval_smtlib2_string\n"; try {