From 621f1f8a850f8875b511e35a03b80634f041f4cc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 30 May 2023 09:44:06 +0200 Subject: [PATCH] sanity check parameters #6737 Signed-off-by: Nikolaj Bjorner --- src/api/api_quant.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/api/api_quant.cpp b/src/api/api_quant.cpp index 885cf6598..0da5c5a92 100644 --- a/src/api/api_quant.cpp +++ b/src/api/api_quant.cpp @@ -249,7 +249,10 @@ extern "C" { expr_abstract(mk_c(c)->m(), 0, num_bound, bound_asts.data(), pat, result); SASSERT(result.get()->get_kind() == AST_APP); pinned.push_back(result.get()); - SASSERT(mk_c(c)->m().is_pattern(result.get())); + if (!mk_c(c)->m().is_pattern(result.get())) { + SET_ERROR_CODE(Z3_INVALID_ARG, "invalid pattern"); + RETURN_Z3(nullptr); + } _patterns.push_back(of_pattern(result.get())); } svector _no_patterns;