Octagon

.vscode/settings.json

@@ -0,0 +1,3 @@
+{
+    "java.configuration.updateBuildConfiguration": "interactive"
+}

lisa/lisa-analyses/imp-testcases/numeric/octagon.imp

@@ -0,0 +1,159 @@
+class octagon_tests {
+
+	assign_relations()
+	{
+		def x = 5;
+		def y = 10;
+		y = -y;
+		y = 8;
+		return 0;
+	}
+
+	assign_relations2()
+	{
+		def x = 10;
+		def y = x + 50;
+		def z = y + 100;
+		return z;
+	}
+
+	assign_relations3()
+	{
+		def x = 10;
+		x = -x - 30;
+
+		def y = 100;
+
+		return x;
+	}
+
+	assign_relations4()
+	{
+		def x = 10;
+		def y = -x + 20;
+
+		return x;
+	}
+
+	loopInfinite() {
+		def x=0;
+
+		while(x<10) {
+			x = x - 1;
+		}
+
+		def z = 10;
+		return x;
+	}
+
+	backward() {
+		def x = 100;
+
+		while(x >= 1) {
+			x = x - 1;
+		}
+		return x; // expected 0
+	}
+
+
+	// Forward increasing loop, terminates when x >= 10
+	forward() {
+		def x = 0;
+		while (x < 10) {
+			x = x + 1;
+		}
+		return x; // expected 10
+	}
+
+	// Backward decreasing loop that terminates (guard x > -5)
+	backward_terminating() {
+		def x = 3;
+		while (x > -5) {
+			x = x - 2;
+		}
+		return x;
+	} 
+
+	// Zero-iteration loop: guard false at entry
+	zero_iterations() {
+		def x = 5;
+		while (x < 0) {
+			x = x + 1;
+		}
+		return x; // expected 5 
+	}
+
+	// Loop with step of 2 (even progression)
+	step2() {
+		def x = 1;
+		while (x - 100 < 0) {
+			x = x + 2;
+		}
+		return x; // expected 100 
+	}
+
+	branches() {
+    	def x = 0;
+    	if (x > 0) {
+			x = 10;
+		} 
+		return x; 
+ 	}
+
+	// Loop with condition depending on two variables
+	mixed_guard() {
+		def x = 0;
+		def y = 3;
+		while (x < y) {
+			x = x + 1; 
+			y = y + 1; 
+		}
+		return x;  
+	}
+
+	//Increasing loop counter
+	example1() {
+		def x = 0;
+
+		while(x < 5) {
+			x=x+1;
+		}
+
+		def z = 100;
+		return x;
+	}
+
+	//Decreasing loop counter
+	example2() {
+		def i=16;
+		def x=1;
+
+		while(i > 0) {
+			x=x+1;
+			i=i-1;
+		}
+
+		def z = 10;
+		return x;
+	}
+
+	//Absolute value
+	example3() {
+		def x=50;
+		def y=x;
+
+		y=-y;
+
+		if(y<=0) {
+			y=-y;
+		} else {
+			y=y+0;
+		}
+
+		if(y<=69) {
+			y=y+0;
+		}
+
+		return y;
+	}
+}

lisa/lisa-analyses/imp-testcases/numeric/octagon/report.json

@@ -0,0 +1,38 @@
+{
+  "warnings" : [ ],
+  "files" : [ "report.json", "untyped_octagon_tests.assign_relations(octagon_tests__this).json", "untyped_octagon_tests.assign_relations2(octagon_tests__this).json", "untyped_octagon_tests.assign_relations3(octagon_tests__this).json", "untyped_octagon_tests.assign_relations4(octagon_tests__this).json", "untyped_octagon_tests.backward(octagon_tests__this).json", "untyped_octagon_tests.backward_terminating(octagon_tests__this).json", "untyped_octagon_tests.branches(octagon_tests__this).json", "untyped_octagon_tests.example1(octagon_tests__this).json", "untyped_octagon_tests.example2(octagon_tests__this).json", "untyped_octagon_tests.example3(octagon_tests__this).json", "untyped_octagon_tests.forward(octagon_tests__this).json", "untyped_octagon_tests.loopInfinite(octagon_tests__this).json", "untyped_octagon_tests.mixed_guard(octagon_tests__this).json", "untyped_octagon_tests.step2(octagon_tests__this).json", "untyped_octagon_tests.zero_iterations(octagon_tests__this).json" ],
+  "info" : {
+    "cfgs" : "15",
+    "duration" : "418ms",
+    "end" : "2025-10-31T20:52:53.683+01:00",
+    "expressions" : "170",
+    "files" : "15",
+    "globals" : "0",
+    "members" : "15",
+    "programs" : "1",
+    "start" : "2025-10-31T20:52:53.265+01:00",
+    "statements" : "72",
+    "units" : "1",
+    "version" : "0.1",
+    "warnings" : "0"
+  },
+  "configuration" : {
+    "analysisGraphs" : "NONE",
+    "descendingPhaseType" : "NONE",
+    "dumpForcesUnwinding" : "false",
+    "fixpointWorkingSet" : "OrderBasedWorkingSet",
+    "glbThreshold" : "5",
+    "hotspots" : "unset",
+    "jsonOutput" : "true",
+    "openCallPolicy" : "WorstCasePolicy",
+    "optimize" : "false",
+    "recursionWideningThreshold" : "5",
+    "semanticChecks" : "",
+    "serializeInputs" : "false",
+    "serializeResults" : "true",
+    "syntacticChecks" : "",
+    "useWideningPoints" : "true",
+    "wideningThreshold" : "5",
+    "workdir" : "test-outputs/numeric/octagon"
+  }
+}

lisa/lisa-analyses/imp-testcases/numeric/octagon/untyped_octagon_tests.assign_relations(octagon_tests__this).json

@@ -0,0 +1 @@
+{"name":"untyped octagon_tests::assign_relations(octagon_tests* this)","description":null,"nodes":[{"id":0,"subNodes":[1,2],"text":"x = 5"},{"id":1,"text":"x"},{"id":2,"text":"5"},{"id":3,"subNodes":[4,5],"text":"y = 10"},{"id":4,"text":"y"},{"id":5,"text":"10"},{"id":6,"subNodes":[7,8],"text":"y = -(y)"},{"id":7,"text":"y"},{"id":8,"subNodes":[9],"text":"-(y)"},{"id":9,"text":"y"},{"id":10,"subNodes":[11,12],"text":"y = 8"},{"id":11,"text":"y"},{"id":12,"text":"8"},{"id":13,"subNodes":[14],"text":"return 0"},{"id":14,"text":"0"}],"edges":[{"sourceId":0,"destId":3,"kind":"SequentialEdge"},{"sourceId":3,"destId":6,"kind":"SequentialEdge"},{"sourceId":6,"destId":10,"kind":"SequentialEdge"},{"sourceId":10,"destId":13,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["octagon_tests*"],"x":["int32"]},"value":"<br>{x -(-x) <= 10.0}<br>{-x -x <= -10.0}<br>"}}},{"nodeId":1,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["octagon_tests*"]},"value":"<br>"}}},{"nodeId":2,"description":{"expressions":["5"],"state":{"heap":"monolith","type":{"this":["octagon_tests*"]},"value":"<br>"}}},{"nodeId":3,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["octagon_tests*"],"x":["int32"],"y":["int32"]},"value":"<br>{y -(-y) <= 20.0}<br>{-y -y <= -20.0}<br>{x -(-x) <= 10.0}<br>{-x -x <= -10.0}<br>{y - x <= 5}<br>{-y -(-x) <= -15}<br>{y -(-x) <= 15}<br>{-y - x <= -15}<br>{x - y <= -5}<br>{-x -(-y) <= -15}<br>{x -(-y) <= 15}<br>{-x - y <= -15}<br>"}}},{"nodeId":4,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["octagon_tests*"],"x":["int32"]},"value":"<br>{x -(-x) <= 10.0}<br>{-x -x <= -10.0}<br>"}}},{"nodeId":5,"description":{"expressions":["10"],"state":{"heap":"monolith","type":{"this":["octagon_tests*"],"x":["int32"]},"value":"<br>{x -(-x) <= 10.0}<br>{-x -x <= -10.0}<br>"}}},{"nodeId":6,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["octagon_tests*"],"x":["int32"],"y":["int32"]},"value":"<br>{y -(-y) <= -20.0}<br>{-y -y <= 20.0}<br>{x -(-x) <= 10.0}<br>{-x -x <= -10.0}<br>{y - x <= -15}<br>{-y -(-x) <= 5}<br>{y -(-x) <= -5}<br>{-y - x <= 5}<br>{x - y <= 15}<br>{-x -(-y) <= 5}<br>{x -(-y) <= -5}<br>{-x - y <= 5}<br>"}}},{"nodeId":7,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["octagon_tests*"],"x":["int32"],"y":["int32"]},"value":"<br>{y -(-y) <= 20.0}<br>{-y -y <= -20.0}<br>{x -(-x) <= 10.0}<br>{-x -x <= -10.0}<br>{y - x <= 5}<br>{-y -(-x) <= -15}<br>{y -(-x) <= 15}<br>{-y - x <= -15}<br>{x - y <= -5}<br>{-x -(-y) <= -15}<br>{x -(-y) <= 15}<br>{-x - y <= -15}<br>"}}},{"nodeId":8,"description":{"expressions":["- y"],"state":{"heap":"monolith","type":{"this":["octagon_tests*"],"x":["int32"],"y":["int32"]},"value":"<br>{y -(-y) <= 20.0}<br>{-y -y <= -20.0}<br>{x -(-x) <= 10.0}<br>{-x -x <= -10.0}<br>{y - x <= 5}<br>{-y -(-x) <= -15}<br>{y -(-x) <= 15}<br>{-y - x <= -15}<br>{x - y <= -5}<br>{-x -(-y) <= -15}<br>{x -(-y) <= 15}<br>{-x - y <= -15}<br>"}}},{"nodeId":9,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["octagon_tests*"],"x":["int32"],"y":["int32"]},"value":"<br>{y -(-y) <= 20.0}<br>{-y -y <= -20.0}<br>{x -(-x) <= 10.0}<br>{-x -x <= -10.0}<br>{y - x <= 5}<br>{-y -(-x) <= -15}<br>{y -(-x) <= 15}<br>{-y - x <= -15}<br>{x - y <= -5}<br>{-x -(-y) <= -15}<br>{x -(-y) <= 15}<br>{-x - y <= -15}<br>"}}},{"nodeId":10,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["octagon_tests*"],"x":["int32"],"y":["int32"]},"value":"<br>{y -(-y) <= 16.0}<br>{-y -y <= -16.0}<br>{x -(-x) <= 10.0}<br>{-x -x <= -10.0}<br>{y - x <= 3}<br>{-y -(-x) <= -13}<br>{y -(-x) <= 13}<br>{-y - x <= -13}<br>{x - y <= -3}<br>{-x -(-y) <= -13}<br>{x -(-y) <= 13}<br>{-x - y <= -13}<br>"}}},{"nodeId":11,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["octagon_tests*"],"x":["int32"],"y":["int32"]},"value":"<br>{y -(-y) <= -20.0}<br>{-y -y <= 20.0}<br>{x -(-x) <= 10.0}<br>{-x -x <= -10.0}<br>{y - x <= -15}<br>{-y -(-x) <= 5}<br>{y -(-x) <= -5}<br>{-y - x <= 5}<br>{x - y <= 15}<br>{-x -(-y) <= 5}<br>{x -(-y) <= -5}<br>{-x - y <= 5}<br>"}}},{"nodeId":12,"description":{"expressions":["8"],"state":{"heap":"monolith","type":{"this":["octagon_tests*"],"x":["int32"],"y":["int32"]},"value":"<br>{y -(-y) <= -20.0}<br>{-y -y <= 20.0}<br>{x -(-x) <= 10.0}<br>{-x -x <= -10.0}<br>{y - x <= -15}<br>{-y -(-x) <= 5}<br>{y -(-x) <= -5}<br>{-y - x <= 5}<br>{x - y <= 15}<br>{-x -(-y) <= 5}<br>{x -(-y) <= -5}<br>{-x - y <= 5}<br>"}}},{"nodeId":13,"description":{"expressions":["ret_value@assign_relations"],"state":{"heap":"monolith","type":{"ret_value@assign_relations":["int32"],"this":["octagon_tests*"],"x":["int32"],"y":["int32"]},"value":"<br>{y -(-y) <= 16.0}<br>{-y -y <= -16.0}<br>{ret_value@assign_relations -(-ret_value@assign_relations) <= 0}<br>{-ret_value@assign_relations -ret_value@assign_relations <= 0}<br>{x -(-x) <= 10.0}<br>{-x -x <= -10.0}<br>{y - ret_value@assign_relations <= 8}<br>{-y -(-ret_value@assign_relations) <= -8}<br>{y -(-ret_value@assign_relations) <= 8}<br>{-y - ret_value@assign_relations <= -8}<br>{y - x <= 3}<br>{-y -(-x) <= -13}<br>{y -(-x) <= 13}<br>{-y - x <= -13}<br>{ret_value@assign_relations - y <= -8}<br>{-ret_value@assign_relations -(-y) <= -8}<br>{ret_value@assign_relations -(-y) <= 8}<br>{-ret_value@assign_relations - y <= -8}<br>{ret_value@assign_relations - x <= -5}<br>{-ret_value@assign_relations -(-x) <= -5}<br>{ret_value@assign_relations -(-x) <= 5}<br>{-ret_value@assign_relations - x <= -5}<br>{x - y <= -3}<br>{-x -(-y) <= -13}<br>{x -(-y) <= 13}<br>{-x - y <= -13}<br>{x - ret_value@assign_relations <= 5}<br>{-x -(-ret_value@assign_relations) <= -5}<br>{x -(-ret_value@assign_relations) <= 5}<br>{-x - ret_value@assign_relations <= -5}<br>"}}},{"nodeId":14,"description":{"expressions":["0"],"state":{"heap":"monolith","type":{"this":["octagon_tests*"],"x":["int32"],"y":["int32"]},"value":"<br>{y -(-y) <= 16.0}<br>{-y -y <= -16.0}<br>{x -(-x) <= 10.0}<br>{-x -x <= -10.0}<br>{y - x <= 3}<br>{-y -(-x) <= -13}<br>{y -(-x) <= 13}<br>{-y - x <= -13}<br>{x - y <= -3}<br>{-x -(-y) <= -13}<br>{x -(-y) <= 13}<br>{-x - y <= -13}<br>"}}}]}

lisa/lisa-analyses/imp-testcases/numeric/octagon/untyped_octagon_tests.assign_relations2(octagon_tests__this).json

@@ -0,0 +1 @@
+{"name":"untyped octagon_tests::assign_relations2(octagon_tests* this)","description":null,"nodes":[{"id":0,"subNodes":[1,2],"text":"x = 10"},{"id":1,"text":"x"},{"id":2,"text":"10"},{"id":3,"subNodes":[4,5],"text":"y = +(x, 50)"},{"id":4,"text":"y"},{"id":5,"subNodes":[6,7],"text":"+(x, 50)"},{"id":6,"text":"x"},{"id":7,"text":"50"},{"id":8,"subNodes":[9,10],"text":"z = +(y, 100)"},{"id":9,"text":"z"},{"id":10,"subNodes":[11,12],"text":"+(y, 100)"},{"id":11,"text":"y"},{"id":12,"text":"100"},{"id":13,"subNodes":[14],"text":"return z"},{"id":14,"text":"z"}],"edges":[{"sourceId":0,"destId":3,"kind":"SequentialEdge"},{"sourceId":3,"destId":8,"kind":"SequentialEdge"},{"sourceId":8,"destId":13,"kind":"SequentialEdge"}],"descriptions":[{"nodeId":0,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["octagon_tests*"],"x":["int32"]},"value":"<br>{x -(-x) <= 20.0}<br>{-x -x <= -20.0}<br>"}}},{"nodeId":1,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["octagon_tests*"]},"value":"<br>"}}},{"nodeId":2,"description":{"expressions":["10"],"state":{"heap":"monolith","type":{"this":["octagon_tests*"]},"value":"<br>"}}},{"nodeId":3,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["octagon_tests*"],"x":["int32"],"y":["int32"]},"value":"<br>{y -(-y) <= 120.0}<br>{-y -y <= -120.0}<br>{x -(-x) <= 20.0}<br>{-x -x <= -20.0}<br>{y - x <= 50.0}<br>{-y -(-x) <= -70.0}<br>{y -(-x) <= 70.0}<br>{-y - x <= -70.0}<br>{x - y <= -50.0}<br>{-x -(-y) <= -70.0}<br>{x -(-y) <= 70.0}<br>{-x - y <= -70.0}<br>"}}},{"nodeId":4,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["octagon_tests*"],"x":["int32"]},"value":"<br>{x -(-x) <= 20.0}<br>{-x -x <= -20.0}<br>"}}},{"nodeId":5,"description":{"expressions":["x + 50"],"state":{"heap":"monolith","type":{"this":["octagon_tests*"],"x":["int32"]},"value":"<br>{x -(-x) <= 20.0}<br>{-x -x <= -20.0}<br>"}}},{"nodeId":6,"description":{"expressions":["x"],"state":{"heap":"monolith","type":{"this":["octagon_tests*"],"x":["int32"]},"value":"<br>{x -(-x) <= 20.0}<br>{-x -x <= -20.0}<br>"}}},{"nodeId":7,"description":{"expressions":["50"],"state":{"heap":"monolith","type":{"this":["octagon_tests*"],"x":["int32"]},"value":"<br>{x -(-x) <= 20.0}<br>{-x -x <= -20.0}<br>"}}},{"nodeId":8,"description":{"expressions":["z"],"state":{"heap":"monolith","type":{"this":["octagon_tests*"],"x":["int32"],"y":["int32"],"z":["int32"]},"value":"<br>{y -(-y) <= 120.0}<br>{-y -y <= -120.0}<br>{z -(-z) <= 320.0}<br>{-z -z <= -320.0}<br>{x -(-x) <= 20.0}<br>{-x -x <= -20.0}<br>{y - z <= -100.0}<br>{-y -(-z) <= -220.0}<br>{y -(-z) <= 220.0}<br>{-y - z <= -220.0}<br>{y - x <= 50.0}<br>{-y -(-x) <= -70.0}<br>{y -(-x) <= 70.0}<br>{-y - x <= -70.0}<br>{z - y <= 100.0}<br>{-z -(-y) <= -220.0}<br>{z -(-y) <= 220.0}<br>{-z - y <= -220.0}<br>{z - x <= 150.0}<br>{-z -(-x) <= -170.0}<br>{z -(-x) <= 170.0}<br>{-z - x <= -170.0}<br>{x - y <= -50.0}<br>{-x -(-y) <= -70.0}<br>{x -(-y) <= 70.0}<br>{-x - y <= -70.0}<br>{x - z <= -150.0}<br>{-x -(-z) <= -170.0}<br>{x -(-z) <= 170.0}<br>{-x - z <= -170.0}<br>"}}},{"nodeId":9,"description":{"expressions":["z"],"state":{"heap":"monolith","type":{"this":["octagon_tests*"],"x":["int32"],"y":["int32"]},"value":"<br>{y -(-y) <= 120.0}<br>{-y -y <= -120.0}<br>{x -(-x) <= 20.0}<br>{-x -x <= -20.0}<br>{y - x <= 50.0}<br>{-y -(-x) <= -70.0}<br>{y -(-x) <= 70.0}<br>{-y - x <= -70.0}<br>{x - y <= -50.0}<br>{-x -(-y) <= -70.0}<br>{x -(-y) <= 70.0}<br>{-x - y <= -70.0}<br>"}}},{"nodeId":10,"description":{"expressions":["y + 100"],"state":{"heap":"monolith","type":{"this":["octagon_tests*"],"x":["int32"],"y":["int32"]},"value":"<br>{y -(-y) <= 120.0}<br>{-y -y <= -120.0}<br>{x -(-x) <= 20.0}<br>{-x -x <= -20.0}<br>{y - x <= 50.0}<br>{-y -(-x) <= -70.0}<br>{y -(-x) <= 70.0}<br>{-y - x <= -70.0}<br>{x - y <= -50.0}<br>{-x -(-y) <= -70.0}<br>{x -(-y) <= 70.0}<br>{-x - y <= -70.0}<br>"}}},{"nodeId":11,"description":{"expressions":["y"],"state":{"heap":"monolith","type":{"this":["octagon_tests*"],"x":["int32"],"y":["int32"]},"value":"<br>{y -(-y) <= 120.0}<br>{-y -y <= -120.0}<br>{x -(-x) <= 20.0}<br>{-x -x <= -20.0}<br>{y - x <= 50.0}<br>{-y -(-x) <= -70.0}<br>{y -(-x) <= 70.0}<br>{-y - x <= -70.0}<br>{x - y <= -50.0}<br>{-x -(-y) <= -70.0}<br>{x -(-y) <= 70.0}<br>{-x - y <= -70.0}<br>"}}},{"nodeId":12,"description":{"expressions":["100"],"state":{"heap":"monolith","type":{"this":["octagon_tests*"],"x":["int32"],"y":["int32"]},"value":"<br>{y -(-y) <= 120.0}<br>{-y -y <= -120.0}<br>{x -(-x) <= 20.0}<br>{-x -x <= -20.0}<br>{y - x <= 50.0}<br>{-y -(-x) <= -70.0}<br>{y -(-x) <= 70.0}<br>{-y - x <= -70.0}<br>{x - y <= -50.0}<br>{-x -(-y) <= -70.0}<br>{x -(-y) <= 70.0}<br>{-x - y <= -70.0}<br>"}}},{"nodeId":13,"description":{"expressions":["ret_value@assign_relations2"],"state":{"heap":"monolith","type":{"ret_value@assign_relations2":["int32"],"this":["octagon_tests*"],"x":["int32"],"y":["int32"],"z":["int32"]},"value":"<br>{y -(-y) <= 120.0}<br>{-y -y <= -120.0}<br>{z -(-z) <= 320.0}<br>{-z -z <= -320.0}<br>{x -(-x) <= 20.0}<br>{-x -x <= -20.0}<br>{ret_value@assign_relations2 -(-ret_value@assign_relations2) <= 320.0}<br>{-ret_value@assign_relations2 -ret_value@assign_relations2 <= -320.0}<br>{y - z <= -100.0}<br>{-y -(-z) <= -220.0}<br>{y -(-z) <= 220.0}<br>{-y - z <= -220.0}<br>{y - x <= 50.0}<br>{-y -(-x) <= -70.0}<br>{y -(-x) <= 70.0}<br>{-y - x <= -70.0}<br>{y - ret_value@assign_relations2 <= -100.0}<br>{-y -(-ret_value@assign_relations2) <= -220.0}<br>{y -(-ret_value@assign_relations2) <= 220.0}<br>{-y - ret_value@assign_relations2 <= -220.0}<br>{z - y <= 100.0}<br>{-z -(-y) <= -220.0}<br>{z -(-y) <= 220.0}<br>{-z - y <= -220.0}<br>{z - x <= 150.0}<br>{-z -(-x) <= -170.0}<br>{z -(-x) <= 170.0}<br>{-z - x <= -170.0}<br>{z - ret_value@assign_relations2 <= 0}<br>{-z -(-ret_value@assign_relations2) <= -320.0}<br>{z -(-ret_value@assign_relations2) <= 320.0}<br>{-z - ret_value@assign_relations2 <= -320.0}<br>{x - y <= -50.0}<br>{-x -(-y) <= -70.0}<br>{x -(-y) <= 70.0}<br>{-x - y <= -70.0}<br>{x - z <= -150.0}<br>{-x -(-z) <= -170.0}<br>{x -(-z) <= 170.0}<br>{-x - z <= -170.0}<br>{x - ret_value@assign_relations2 <= -150.0}<br>{-x -(-ret_value@assign_relations2) <= -170.0}<br>{x -(-ret_value@assign_relations2) <= 170.0}<br>{-x - ret_value@assign_relations2 <= -170.0}<br>{ret_value@assign_relations2 - y <= 100.0}<br>{-ret_value@assign_relations2 -(-y) <= -220.0}<br>{ret_value@assign_relations2 -(-y) <= 220.0}<br>{-ret_value@assign_relations2 - y <= -220.0}<br>{ret_value@assign_relations2 - z <= 0}<br>{-ret_value@assign_relations2 -(-z) <= -320.0}<br>{ret_value@assign_relations2 -(-z) <= 320.0}<br>{-ret_value@assign_relations2 - z <= -320.0}<br>{ret_value@assign_relations2 - x <= 150.0}<br>{-ret_value@assign_relations2 -(-x) <= -170.0}<br>{ret_value@assign_relations2 -(-x) <= 170.0}<br>{-ret_value@assign_relations2 - x <= -170.0}<br>"}}},{"nodeId":14,"description":{"expressions":["z"],"state":{"heap":"monolith","type":{"this":["octagon_tests*"],"x":["int32"],"y":["int32"],"z":["int32"]},"value":"<br>{y -(-y) <= 120.0}<br>{-y -y <= -120.0}<br>{z -(-z) <= 320.0}<br>{-z -z <= -320.0}<br>{x -(-x) <= 20.0}<br>{-x -x <= -20.0}<br>{y - z <= -100.0}<br>{-y -(-z) <= -220.0}<br>{y -(-z) <= 220.0}<br>{-y - z <= -220.0}<br>{y - x <= 50.0}<br>{-y -(-x) <= -70.0}<br>{y -(-x) <= 70.0}<br>{-y - x <= -70.0}<br>{z - y <= 100.0}<br>{-z -(-y) <= -220.0}<br>{z -(-y) <= 220.0}<br>{-z - y <= -220.0}<br>{z - x <= 150.0}<br>{-z -(-x) <= -170.0}<br>{z -(-x) <= 170.0}<br>{-z - x <= -170.0}<br>{x - y <= -50.0}<br>{-x -(-y) <= -70.0}<br>{x -(-y) <= 70.0}<br>{-x - y <= -70.0}<br>{x - z <= -150.0}<br>{-x -(-z) <= -170.0}<br>{x -(-z) <= 170.0}<br>{-x - z <= -170.0}<br>"}}}]}