added model methods to list which fixes Tree constructor proof reloading

KeYProject · Oct 27, 2023 · 879270e · 879270e
1 parent 4d525c7
commit 879270e
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/contract-order.txt b/contract-order.txt
@@ -8,6 +8,10 @@ de.wiesler.Functions[de.wiesler.Functions::fill([I,int,int,int)].JML normal_beha
 de.wiesler.Buffers[de.wiesler.Buffers::align_to_next_block(int)].JML normal_behavior operation contract.0
 de.wiesler.Buffers[de.wiesler.Buffers::blockAligned(int)].JML model_behavior operation contract.0
 
+de.wiesler.Tree[de.wiesler.Tree::piInRangeUpper(int,int)].JML model_behavior operation contract.0
+de.wiesler.Tree[de.wiesler.Tree::piInRangeLower(int,int)].JML model_behavior operation contract.0
+de.wiesler.Tree[de.wiesler.Tree::piLemmaUpperBound(int)].JML model_behavior operation contract.0
+
 # constructors here just to be safe that they don't use contracts proven in the final heap
 de.wiesler.Tree[de.wiesler.Tree::Tree([I,[I,int)].JML normal_behavior operation contract.0
 de.wiesler.Tree[de.wiesler.Tree::build(int,[I,int,int)].JML normal_behavior operation contract.0