From c351d58622547d2fb771a69ca872465e1b8a1698 Mon Sep 17 00:00:00 2001
From: Kwesi Rutledge <kwesir@csail.mit.edu>
Date: Wed, 8 Oct 2025 00:15:15 -0400
Subject: [PATCH 1/2] Added fix in the ImpliesThisIsAlsoSatisfied method

---
 symbolic/scalar_constraint.go              | 14 ++++-----
 testing/symbolic/scalar_constraint_test.go | 34 ++++++++++++++++++++++
 2 files changed, 39 insertions(+), 9 deletions(-)

diff --git a/symbolic/scalar_constraint.go b/symbolic/scalar_constraint.go
index 6177ea1..d6ea979 100644
--- a/symbolic/scalar_constraint.go
+++ b/symbolic/scalar_constraint.go
@@ -367,15 +367,11 @@ func (sc ScalarConstraint) ImpliesThisIsAlsoSatisfied(other Constraint) bool {
 			otherCCoeffVector := otherC.LeftHandSide.LinearCoeff(otherC.Variables())
 			otherCCoeff := otherCCoeffVector.AtVec(0)
 
-			// If the coefficient of scCoeff is < 0,
-			// then flip the signs of both sides of the constraint
-			if scCoeff < 0 {
-				sc = sc.ScaleBy(-1).(ScalarConstraint)
-			}
-
-			if otherCCoeff < 0 {
-				otherC = otherC.ScaleBy(-1).(ScalarConstraint)
-			}
+			// Scale both constraints
+			// Note: If the coefficient is negative, then the sense of the constraint will be flipped.
+			// This is handled in the ScaleBy method.
+			sc = sc.ScaleBy(1.0 / scCoeff).(ScalarConstraint)
+			otherC = otherC.ScaleBy(1.0 / otherCCoeff).(ScalarConstraint)
 
 			// The implication holds if all of the following are true:
 			// 1. The sense of sc and otherC are either the same (or one is equality)
diff --git a/testing/symbolic/scalar_constraint_test.go b/testing/symbolic/scalar_constraint_test.go
index 6321d33..6daad24 100644
--- a/testing/symbolic/scalar_constraint_test.go
+++ b/testing/symbolic/scalar_constraint_test.go
@@ -1918,6 +1918,40 @@ func TestScalarConstraint_ImpliesThisIsAlsoSatisfied10(t *testing.T) {
 	}
 }
 
+/*
+TestScalarConstraint_ImpliesThisIsAlsoSatisfied11
+Description:
+
+	Tests the ImpliesThisIsAlsoSatisfied() method of a scalar constraint.
+	This test attempts to catch a bug where the method would note that some
+	constraints imply others that they should not actually imply.
+	In this case, it seems like we have constraints where, if you compare
+	the constants on the right hand side, then they might seem to imply one
+	another: (1 <= 2), but when you consider the left hand side's
+	coefficients, you see that they do NOT actually imply one another.
+	In this case, we have:
+		2 x <= 1 and
+		10 x <= 2
+	as the input constraints. The first constraint does NOT imply the second.
+*/
+func TestScalarConstraint_ImpliesThisIsAlsoSatisfied11(t *testing.T) {
+	// Constants
+	x := symbolic.NewVariable()
+
+	// Create constraint
+	sc := x.Multiply(2).LessEq(1.0)
+
+	// Create a second constraint
+	sc2 := x.Multiply(10).LessEq(2.0)
+
+	// Verify that the first constraint does NOT imply the second
+	if sc.ImpliesThisIsAlsoSatisfied(sc2) {
+		t.Errorf(
+			"Expected sc.ImpliesThisIsAlsoSatisfied(sc2) to be false; received true",
+		)
+	}
+}
+
 /*
 TestScalarConstraint_AsSimplifiedConstraint1
 Description:

From a5884ae808f92a7bf9d77fba1a006c9f7271b3c2 Mon Sep 17 00:00:00 2001
From: Kwesi Rutledge <kwesir@csail.mit.edu>
Date: Wed, 8 Oct 2025 00:20:01 -0400
Subject: [PATCH 2/2] Added test for case with negative coefficients

---
 testing/symbolic/scalar_constraint_test.go | 34 ++++++++++++++++++++++
 1 file changed, 34 insertions(+)

diff --git a/testing/symbolic/scalar_constraint_test.go b/testing/symbolic/scalar_constraint_test.go
index 6daad24..155670f 100644
--- a/testing/symbolic/scalar_constraint_test.go
+++ b/testing/symbolic/scalar_constraint_test.go
@@ -1952,6 +1952,40 @@ func TestScalarConstraint_ImpliesThisIsAlsoSatisfied11(t *testing.T) {
 	}
 }
 
+/*
+TestScalarConstraint_ImpliesThisIsAlsoSatisfied12
+Description:
+
+	Tests the ImpliesThisIsAlsoSatisfied() method of a scalar constraint.
+	This test attempts to catch a bug where the method would note that some
+	constraints imply others that they should not actually imply.
+	In this case, it seems like we have constraints where, if you compare
+	the constants on the right hand side, then they might seem to imply one
+	another: (-2 >= -4), but when you consider the left hand side's
+	coefficients, you see that they do NOT actually imply one another.
+	In this case, we have:
+		-2 x <= 2 and
+		-10 x <= 4
+	as the input constraints. The first constraint does NOT imply the second.
+*/
+func TestScalarConstraint_ImpliesThisIsAlsoSatisfied12(t *testing.T) {
+	// Constants
+	x := symbolic.NewVariable()
+
+	// Create constraint
+	sc := x.Multiply(-2).LessEq(2.0)
+
+	// Create a second constraint
+	sc2 := x.Multiply(-10).LessEq(4.0)
+
+	// Verify that the first constraint does NOT imply the second
+	if sc.ImpliesThisIsAlsoSatisfied(sc2) {
+		t.Errorf(
+			"Expected sc.ImpliesThisIsAlsoSatisfied(sc2) to be false; received true",
+		)
+	}
+}
+
 /*
 TestScalarConstraint_AsSimplifiedConstraint1
 Description: