1 files changed, 21 insertions, 0 deletions
diff --git a/Test/test0/SeparateVerification0.bpl b/Test/test0/SeparateVerification0.bpl
new file mode 100644
index 00000000..5a8ef283
--- /dev/null
+++ b/Test/test0/SeparateVerification0.bpl
@@ -0,0 +1,21 @@
+// need to include this file twice for it to include all necessary declarations
+
+#if FILE_0
+const x: int;
+#else
+const y: int;
+#endif
+
+#if FILE_1
+axiom x == 12;
+procedure Q();
+#else
+axiom y == 7;
+#endif
+
+// duplicates of :extern's are fine (Boogie keeps the non-:extern or chooses arbitrarily among the :extern's)
+type {:extern} T;
+const {:extern} C: int;
+function {:extern} F(): int;
+var {:extern} n: int;
+procedure {:extern} P(inconsistentParameterButThatIsOkayBecauseTheExternIsIgnored: int);