From d289434b6589160f8840caf6c174bd5f9f161806 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 12 Jan 2023 19:06:30 -0800 Subject: [PATCH] fix #6535 --- src/test/smt2print_parse.cpp | 30 ++++++++++++++++++++---------- 1 file changed, 20 insertions(+), 10 deletions(-) diff --git a/src/test/smt2print_parse.cpp b/src/test/smt2print_parse.cpp index ed674de8b..765a78060 100644 --- a/src/test/smt2print_parse.cpp +++ b/src/test/smt2print_parse.cpp @@ -67,7 +67,7 @@ void test_parseprint(char const* spec) { void test_eval(Z3_context ctx, Z3_string spec, bool shouldFail) { std::cout << "spec:\n" << spec << "\n"; - Z3_string resp; + std::string resp; bool failed = false; try { resp = Z3_eval_smtlib2_string(ctx, spec); @@ -76,6 +76,10 @@ void test_eval(Z3_context ctx, Z3_string spec, bool shouldFail) { resp = e.what(); failed = true; } + catch (...) { + resp = "unknown exception"; + failed = true; + } std::cout << "response:\n" << resp << "\n"; @@ -141,15 +145,21 @@ void test_repeated_eval() { Z3_set_error_handler(ctx, throwError); std::cout << "testing Z3_eval_smtlib2_string\n"; - test_eval(ctx, spec1, false); - std::cout << "successful call after successful call\n"; - test_eval(ctx, spec2, false); - std::cout << "failing call after successful call\n"; - test_eval(ctx, spec3, true); - std::cout << "failing call after failing call\n"; - test_eval(ctx, spec4, true); - std::cout << "successful call after failing call\n"; - test_eval(ctx, spec1, false); + try { + test_eval(ctx, spec1, false); + std::cout << "successful call after successful call\n"; + test_eval(ctx, spec2, false); + std::cout << "failing call after successful call\n"; + test_eval(ctx, spec3, true); + std::cout << "failing call after failing call\n"; + test_eval(ctx, spec4, true); + std::cout << "successful call after failing call\n"; + test_eval(ctx, spec1, false); + } + catch(...) { + std::cout << "Error: uncaught exception\n"; + throw; + } std::cout << "done evaluating\n";