From 546c70128307063ce88a1901e55df1ea7dea72f4 Mon Sep 17 00:00:00 2001
From: Jonas Hansen <ganymed92@gmail.com>
Date: Wed, 27 Apr 2022 17:20:50 +0200
Subject: [PATCH] Do not copy preconditions of base spec to constrained spec

---
 prusti-interface/src/specs/typed.rs | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/prusti-interface/src/specs/typed.rs b/prusti-interface/src/specs/typed.rs
index f0e4c15728c..fb293080f65 100644
--- a/prusti-interface/src/specs/typed.rs
+++ b/prusti-interface/src/specs/typed.rs
@@ -247,7 +247,16 @@ impl SpecGraph<ProcedureSpecification> {
     ) -> &mut ProcedureSpecification {
         self.specs_with_constraints
             .entry(constraint)
-            .or_insert_with(|| self.base_spec.clone())
+            .or_insert_with(|| {
+                let mut base = self.base_spec.clone();
+
+                // Preconditions of the base spec do not appear in the constrained spec
+                // Any preconditions that exist on the base spec are thus pruned
+                // (see comment on impl block)
+                base.pres = SpecificationItem::Empty;
+
+                base
+            })
     }
 
     /// Gets the constraint of a spec function `spec`.