From bd26f5fef83108399ac1bc929533af7c71abe89e Mon Sep 17 00:00:00 2001 From: Mikolaj Wielgus Date: Tue, 25 Jun 2024 00:40:53 +0200 Subject: [PATCH] layout: fix via placement contract for number of nodes --- src/layout/layout.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/layout/layout.rs b/src/layout/layout.rs index 4685ce7..15ca6a3 100644 --- a/src/layout/layout.rs +++ b/src/layout/layout.rs @@ -63,7 +63,7 @@ impl Layout { self.drawing.remove_cane(cane, face) } - #[debug_ensures(ret.is_ok() -> self.drawing.node_count() == old(self.drawing.node_count()) + weight.to_layer - weight.from_layer)] + #[debug_ensures(ret.is_ok() -> self.drawing.node_count() == old(self.drawing.node_count()) + weight.to_layer - weight.from_layer + 2)] #[debug_ensures(ret.is_err() -> self.drawing.node_count() == old(self.drawing.node_count()))] pub fn add_via(&mut self, weight: ViaWeight) -> Result, Infringement> { let compound = self.drawing.add_compound(weight.into());