From d4f46b5ad2d74960ee14c0f1b98107ab491636e2 Mon Sep 17 00:00:00 2001
From: Jonas Jongejan <jonas@picturestudio.ai>
Date: Sat, 19 Oct 2024 13:23:29 -0400
Subject: [PATCH] Add check for arg length

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

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<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(