diff --git a/src/api/js/src/high-level/high-level.ts b/src/api/js/src/high-level/high-level.ts index 78012c502..797d3a0ce 100644 --- a/src/api/js/src/high-level/high-level.ts +++ b/src/api/js/src/high-level/high-level.ts @@ -224,6 +224,12 @@ export function createApi(Z3: Z3Core): Z3HighLevel { function _toExpr(ast: Z3_ast): Bool | IntNum | RatNum | Arith | Expr { const kind = check(Z3.get_ast_kind(contextPtr, ast)); if (kind === Z3_ast_kind.Z3_QUANTIFIER_AST) { + if (Z3.is_quantifier_forall(contextPtr, ast)) + return BoolImpl(ast); + if (Z3.is_quantifier_exists(contextPtr, ast)) + return BoolImpl(ast); + if (Z3.is_quantifier_lambda(contextPtr, ast)) + return ExprImpl(ast); assert(false); } const sortKind = check(Z3.get_sort_kind(contextPtr, Z3.get_sort(contextPtr, ast)));