Adapt OctagonRelationTest (changed due to normalization)

schuessf · schuessf · commit 8c0edc411842 · 2023-01-18T11:17:13.000+01:00
diff --git a/trunk/source/Library-ModelCheckerUtilsTest/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/smt/linearterms/OctagonRelationTest.java b/trunk/source/Library-ModelCheckerUtilsTest/src/de/uni_freiburg/informatik/ultimate/modelcheckerutils/smt/linearterms/OctagonRelationTest.java
@@ -90,7 +90,7 @@ public void testOneVarInt() {
 		Assert.assertEquals("(+a) - (-a) > 14", octRelAsString("(> a 7)"));
 		Assert.assertEquals("(+a) - (-a) <= 4", octRelAsString("(<= (* 3 a) 7)"));
 
-		Assert.assertEquals("(-a) - (+a) = 5", octRelAsString("(= (- 5) (* a 2))"));
+		Assert.assertEquals("(-a) - (+a) = 6", octRelAsString("(= (- 6) (* a 2))"));
 	}
 
 	@Test
@@ -127,6 +127,7 @@ public void testTwoVarReal() {
 	@Test
 	public void testNoCommonCoefficient() {
 		Assert.assertNull(octRelAsString("(<= (+ (* 3 a) (* 4 b)) 5)"));
+		Assert.assertNull(octRelAsString("(= (- 5) (* a 2))"));
 	}
 
 	@Test

Original file line number	Diff line number	Diff line change
`@@ -90,7 +90,7 @@ public void testOneVarInt() {`
`90`	`90`	`Assert.assertEquals("(+a) - (-a) > 14", octRelAsString("(> a 7)"));`
`91`	`91`	`Assert.assertEquals("(+a) - (-a) <= 4", octRelAsString("(<= (* 3 a) 7)"));`
`92`	`92`
`93`		`- Assert.assertEquals("(-a) - (+a) = 5", octRelAsString("(= (- 5) (* a 2))"));`
	`93`	`+ Assert.assertEquals("(-a) - (+a) = 6", octRelAsString("(= (- 6) (* a 2))"));`
`94`	`94`	`}`
`95`	`95`
`96`	`96`	`@Test`
`@@ -127,6 +127,7 @@ public void testTwoVarReal() {`
`127`	`127`	`@Test`
`128`	`128`	`public void testNoCommonCoefficient() {`
`129`	`129`	`Assert.assertNull(octRelAsString("(<= (+ (* 3 a) (* 4 b)) 5)"));`
	`130`	`+ Assert.assertNull(octRelAsString("(= (- 5) (* a 2))"));`
`130`	`131`	`}`
`131`	`132`
`132`	`133`	`@Test`