mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
update unit test to be compatible with C++ vs C exception semantics #6537
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
8aa35f7fdb
commit
59b56f2ce7
|
@ -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 {
|
||||
|
|
Loading…
Reference in a new issue