mirror of
https://github.com/Z3Prover/z3
synced 2025-06-15 02:16:16 +00:00
add missing new
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
bb5d81195c
commit
665ef2c6ba
1 changed files with 3 additions and 3 deletions
|
@ -225,11 +225,11 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
|
||||||
const kind = check(Z3.get_ast_kind(contextPtr, ast));
|
const kind = check(Z3.get_ast_kind(contextPtr, ast));
|
||||||
if (kind === Z3_ast_kind.Z3_QUANTIFIER_AST) {
|
if (kind === Z3_ast_kind.Z3_QUANTIFIER_AST) {
|
||||||
if (Z3.is_quantifier_forall(contextPtr, ast))
|
if (Z3.is_quantifier_forall(contextPtr, ast))
|
||||||
return BoolImpl(ast);
|
return new BoolImpl(ast);
|
||||||
if (Z3.is_quantifier_exists(contextPtr, ast))
|
if (Z3.is_quantifier_exists(contextPtr, ast))
|
||||||
return BoolImpl(ast);
|
return new BoolImpl(ast);
|
||||||
if (Z3.is_quantifier_lambda(contextPtr, ast))
|
if (Z3.is_quantifier_lambda(contextPtr, ast))
|
||||||
return ExprImpl(ast);
|
return new ExprImpl(ast);
|
||||||
assert(false);
|
assert(false);
|
||||||
}
|
}
|
||||||
const sortKind = check(Z3.get_sort_kind(contextPtr, Z3.get_sort(contextPtr, ast)));
|
const sortKind = check(Z3.get_sort_kind(contextPtr, Z3.get_sort(contextPtr, ast)));
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue