diff --git a/src/test/seq_rewriter.cpp b/src/test/seq_rewriter.cpp index bfdb3dc9d0..45ae1c47ec 100644 --- a/src/test/seq_rewriter.cpp +++ b/src/test/seq_rewriter.cpp @@ -56,7 +56,7 @@ static void test_seq_foldl_nth_model_validation() { Z3_del_context(ctx); } -static void test_seq_fold_scalar_model_validation() { +static void test_seq_foldl_foldli_scalar_model_validation() { Z3_context ctx = Z3_mk_context(nullptr); char const* result = Z3_eval_smtlib2_string(ctx, @@ -90,6 +90,7 @@ static void test_seq_fold_scalar_model_validation() { "(check-sat)\n" "(pop)\n"); ENSURE(std::strstr(result, "unknown") == nullptr); + ENSURE(std::strstr(result, "invalid model") == nullptr); unsigned sat_count = 0; std::istringstream in{std::string(result)}; for (std::string line; std::getline(in, line);) @@ -325,7 +326,7 @@ void tst_seq_rewriter() { } test_seq_foldl_nth_model_validation(); - test_seq_fold_scalar_model_validation(); + test_seq_foldl_foldli_scalar_model_validation(); std::cout << "tst_seq_rewriter: all tests passed\n"; }