layout: fix via placement contract for number of nodes

This commit is contained in:
Mikolaj Wielgus 2024-06-25 00:40:53 +02:00
parent e2552a156b
commit bd26f5fef8
1 changed files with 1 additions and 1 deletions

View File

@ -63,7 +63,7 @@ impl<R: RulesTrait> Layout<R> {
self.drawing.remove_cane(cane, face) 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()))] #[debug_ensures(ret.is_err() -> self.drawing.node_count() == old(self.drawing.node_count()))]
pub fn add_via(&mut self, weight: ViaWeight) -> Result<GenericIndex<ViaWeight>, Infringement> { pub fn add_via(&mut self, weight: ViaWeight) -> Result<GenericIndex<ViaWeight>, Infringement> {
let compound = self.drawing.add_compound(weight.into()); let compound = self.drawing.add_compound(weight.into());