mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 03:15:50 +00:00
Code Activity

fix #6535

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-01-12 19:06:30 -08:00
parent 0d46787fcf
commit d289434b65
1 changed files with 20 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

30
src/test/smt2print_parse.cpp
View file

@ -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";