Fixes too much pruning when using monomorphization.

boogie-org · Aug 3, 2023 · 2f21837 · 2f21837
1 parent 41d2e86
commit 2f21837
Show file tree

Hide file tree

Showing 3 changed files with 226 additions and 49 deletions.
diff --git a/Source/Core/AST/Absy.cs b/Source/Core/AST/Absy.cs
@@ -1429,7 +1429,23 @@ public class Constant : Variable
     // from all other constants.
     public readonly bool Unique;
 
-    public IList<Axiom> DefinitionAxioms { get; }
+    public IList<Axiom> DefinitionAxioms => definitionAxioms;
+
+    private IList<Axiom> definitionAxioms = new List<Axiom>();
+
+    public bool RemoveDefinitionAxiom(Axiom axiom)
+    {
+      Contract.Requires(axiom != null);
+
+      return definitionAxioms.Remove(axiom);
+    }
+
+    public void AddDefinitionAxiom(Axiom axiom)
+    {
+      Contract.Requires(axiom != null);
+
+      DefinitionAxioms.Add(axiom);
+    }
 
     public Constant(IToken /*!*/ tok, TypedIdent /*!*/ typedIdent)
       : this(tok, typedIdent, true)
@@ -1452,7 +1468,7 @@ public Constant(IToken /*!*/ tok, TypedIdent /*!*/ typedIdent,
       Contract.Requires(typedIdent.Name != null && typedIdent.Name.Length > 0);
       Contract.Requires(typedIdent.WhereExpr == null);
       this.Unique = unique;
-      this.DefinitionAxioms = definitionAxioms ?? new List<Axiom>();
+      this.definitionAxioms = definitionAxioms ?? new List<Axiom>();
     }
 
     public override bool IsMutable => false;
@@ -2058,6 +2074,13 @@ public void AddOtherDefinitionAxiom(Axiom axiom)
       otherDefinitionAxioms.Add(axiom);
     }
 
+    public bool RemoveOtherDefinitionAxiom(Axiom axiom)
+    {
+      Contract.Requires(axiom != null);
+
+      return otherDefinitionAxioms.Remove(axiom);
+    }
+
     private bool neverTrigger;
     private bool neverTriggerComputed;