diff --git a/src/api/js/src/high-level/high-level.ts b/src/api/js/src/high-level/high-level.ts index c7990ae5d5f..583eec5a595 100644 --- a/src/api/js/src/high-level/high-level.ts +++ b/src/api/js/src/high-level/high-level.ts @@ -959,6 +959,9 @@ export function createApi(Z3: Z3Core): Z3HighLevel { function PbEq(args: [Bool, ...Bool[]], coeffs: [number, ...number[]], k: number): Bool { _assertContext(...args); + if (args.length !== coeffs.length) { + throw new Error('Number of arguments and coefficients must match'); + } return new BoolImpl( check( Z3.mk_pbeq( @@ -973,6 +976,9 @@ export function createApi(Z3: Z3Core): Z3HighLevel { function PbGe(args: [Bool, ...Bool[]], coeffs: [number, ...number[]], k: number): Bool { _assertContext(...args); + if (args.length !== coeffs.length) { + throw new Error('Number of arguments and coefficients must match'); + } return new BoolImpl( check( Z3.mk_pbge( @@ -987,6 +993,9 @@ export function createApi(Z3: Z3Core): Z3HighLevel { function PbLe(args: [Bool, ...Bool[]], coeffs: [number, ...number[]], k: number): Bool { _assertContext(...args); + if (args.length !== coeffs.length) { + throw new Error('Number of arguments and coefficients must match'); + } return new BoolImpl( check( Z3.mk_pble(