From b26420ed997a6a064b8fdb243e7d2d07541a321a Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 19 Aug 2022 18:15:54 -0700
Subject: [PATCH] #6285

---
 src/api/js/src/high-level/high-level.ts | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/api/js/src/high-level/high-level.ts b/src/api/js/src/high-level/high-level.ts
index 78012c50259..797d3a0cec4 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<Name> | IntNum<Name> | RatNum<Name> | Arith<Name> | Expr<Name> {
       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)));