Skip to content

Commit 69db378

Browse files
committed
Merge branch 'topic/389-dross-remove-proj-axiom' into 'master'
Remove the axiom used for the model projection of arrays Issue: eng/spark/spark2014#389 See merge request eng/spark/why3!61
2 parents 3a1bb28 + df0200c commit 69db378

File tree

3 files changed

+12
-0
lines changed

3 files changed

+12
-0
lines changed

drivers/alt-ergo_gnatprove.drv

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -60,6 +60,10 @@ theory for_drivers.ComputerOfEuclideanDivision
6060

6161
end
6262

63+
theory _gnatprove_standard.Array__1
64+
remove prop get_proj
65+
end
66+
6367
(*
6468
Local Variables:
6569
mode: why

drivers/cvc5_gnatprove.drv

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -66,3 +66,7 @@ theory real.Real
6666
remove prop assoc_div_div
6767
remove prop CompatOrderMult
6868
end
69+
70+
theory _gnatprove_standard.Array__1
71+
remove prop get_proj
72+
end

drivers/z3_gnatprove.drv

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -72,3 +72,7 @@ end
7272
theory int.MinMax
7373
remove allprops
7474
end
75+
76+
theory _gnatprove_standard.Array__1
77+
remove prop get_proj
78+
end

0 commit comments

Comments
 (0)