diff --git a/colibri2/theories/LRA/simplex.ml b/colibri2/theories/LRA/simplex.ml index af6b211b6177d8db1d12a0e94e1179bc31ea01c6..3673a8f9eb0a7dd6e43cb39aea53b17b40c072da 100644 --- a/colibri2/theories/LRA/simplex.ml +++ b/colibri2/theories/LRA/simplex.ml @@ -177,6 +177,8 @@ let make_equations d (eqs, vars) n = let sign = Dom_product.SolveSign.get_repr d n in match (abs, sign) with | Some abs, Some sign -> + (* The restriction is not for soundness, any node can be added as + equation using {!addition} since it uses the domains of the node *) Debug.dprintf6 debug "[Simplex] %a: %a --- %a" Node.pp n Product.pp abs Sign_product.pp sign; if Sign_product.(equal one sign) then