From c5842b7821204e6543f47efa744c6385e8b20535 Mon Sep 17 00:00:00 2001
From: Mikolaj Wielgus <wielgusmikolaj@gmail.com>
Date: Wed, 12 Jun 2024 14:42:06 +0200
Subject: [PATCH] drawing: fix contracts on placement failures

---
 src/drawing/drawing.rs | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/drawing/drawing.rs b/src/drawing/drawing.rs
index cedc195..526177a 100644
--- a/src/drawing/drawing.rs
+++ b/src/drawing/drawing.rs
@@ -148,7 +148,8 @@ impl<CW: Copy, R: RulesTrait> Drawing<CW, R> {
         }
     }
 
-    #[debug_ensures(self.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count() + 1))]
+    #[debug_ensures(ret.is_ok() -> self.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count() + 1))]
+    #[debug_ensures(ret.is_err() -> self.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count()))]
     #[debug_ensures(self.geometry_with_rtree.graph().edge_count() == old(self.geometry_with_rtree.graph().edge_count()))]
     pub fn add_fixed_dot(&mut self, weight: FixedDotWeight) -> Result<FixedDotIndex, Infringement> {
         self.add_dot_with_infringables(weight, Some(&[]))
@@ -188,7 +189,8 @@ impl<CW: Copy, R: RulesTrait> Drawing<CW, R> {
         self.geometry_with_rtree.add_dot(weight)
     }
 
-    #[debug_ensures(self.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count() + 1))]
+    #[debug_ensures(ret.is_ok() -> self.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count() + 1))]
+    #[debug_ensures(ret.is_err() -> self.geometry_with_rtree.graph().node_count() == old(self.geometry_with_rtree.graph().node_count()))]
     #[debug_ensures(self.geometry_with_rtree.graph().edge_count() == old(self.geometry_with_rtree.graph().edge_count()))]
     pub fn add_fixed_seg(
         &mut self,