Do not assert in user code

src/assertBounds.ml

@@ -219,7 +219,16 @@ module Make(Core : CoreSig.S) : S with module Core = Core = struct
     let poly env p ?min ?max slk =
       debug "[entry of assert_poly]" env (Result.get None);
       check_invariants env (Result.get None);
-      assert (P.is_polynomial p);
+      (* Note: we should not convert the call to [poly] into a call to [var]
+         here because we introduce the equality [poly = slk] and then we set
+         the bounds for [slk] to [min] and [max].
+
+         If there is a single variable (i.e. [poly = k * x] for some
+         coefficient [k] and variable [x]), we do not want to add the useless
+         slack variable [slk = k * x]. *)
+      if not (P.is_polynomial p) then
+        invalid_arg
+          "poly: must have two variables or more, use var instead";
       let mini = update_min_bound env min in
       let maxi = update_max_bound env max in
       let env, is_fresh = register_slake slk p env in

src/assertBounds.mli

@@ -22,13 +22,21 @@ module type S = sig
     Core.Var.t ->
     Core.t * bool
 
-  (*  The returned bool is [true] if the asserted bounds are not trivial
-      (i.e. not implied by known bounds) *)
   (** [poly env poly min max x] returns a new environment obtained by changing
       the bounds of [poly] in [env] to [min] and [max].
       The polynomial is represented by the slack variable [x].
-      If the bounds were implied by other known bounds (in other words, if the
-      environment did not change) the associated boolean will be [false].
+
+      [poly] must be a polynomial (as tested by [Core.P.is_polynomial]), that
+      is, it must contain at least two distinct variables. Use [var] instead
+      for constraints that apply to a single variable.
+
+      The returned bool is [true] if the asserted bounds are not trivial (i.e.
+      not implied by known bounds). If the bounds were implied by other known
+      bounds (in other words, if the environment did not change) the associated
+      boolean will be [false].
+
+      @raise Invalid_argument if [poly] contains zero or one variables (use [var]
+      to add constraints to a single variable).
   *)
   val poly :
     Core.t ->