Add check for arg length

Z3Prover · Oct 19, 2024 · d4f46b5 · d4f46b5
1 parent b28c861
commit d4f46b5
Showing 1 changed file with 9 additions and 0 deletions.
diff --git 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<Name>, ...Bool<Name>[]], coeffs: [number, ...number[]], k: number): Bool<Name> {
       _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<Name>, ...Bool<Name>[]], coeffs: [number, ...number[]], k: number): Bool<Name> {
       _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<Name>, ...Bool<Name>[]], coeffs: [number, ...number[]], k: number): Bool<Name> {
       _assertContext(...args);
+      if (args.length !== coeffs.length) {
+        throw new Error('Number of arguments and coefficients must match');
+      }
       return new BoolImpl(
         check(
           Z3.mk_pble(