Boogie build succeeded

author: codeplexbot <unknown> 2010-07-31 05:30:53 +0000
committer: codeplexbot <unknown> 2010-07-31 05:30:53 +0000
commit: 1679c064cdb5c667d9f8e46eaac58a65c66d8b11 (patch)
tree: c3cb0e7adac224b4d1c83023dd7003971b2cd2f4 /_admin
parent: f513d6f3716b7c963e30ca3d004cf6a40d2f68c5 (diff)
1 files changed, 32 insertions, 277 deletions
diff --git a/_admin/Boogie/aste/summary.log b/_admin/Boogie/aste/summary.log
index 9a418c2f..e1d7d3cd 100644
--- a/_admin/Boogie/aste/summary.log
+++ b/_admin/Boogie/aste/summary.log
@@ -1,13 +1,13 @@
-# Aste started: 2010-07-29 07:00:05
+# Aste started: 2010-07-31 07:00:05
 # Host id: Boogiebox
-# [2010-07-29 07:02:19] SpecSharp revision: 55320
-# [2010-07-29 07:03:12] Boogie revision: 55810
-# [2010-07-29 07:03:36] SscBoogie revision: 55325
-[2010-07-29 07:04:06] C:\Program Files (x86)\Microsoft Visual Studio 9.0\Common7\IDE\devenv.com SpecSharp.sln /Build DebugCommandLine
+# [2010-07-31 07:02:13] SpecSharp revision: 55320
+# [2010-07-31 07:03:06] Boogie revision: 55909
+# [2010-07-31 07:03:27] SscBoogie revision: 55325
+[2010-07-31 07:03:54] C:\Program Files (x86)\Microsoft Visual Studio 9.0\Common7\IDE\devenv.com SpecSharp.sln /Build DebugCommandLine
 
     warning CS1668
     warning CS1668
-[2010-07-29 07:05:40] C:\Program Files (x86)\Microsoft Visual Studio 9.0\Common7\IDE\devenv.com Boogie.sln /Build Debug
+[2010-07-31 07:05:29] C:\Program Files (x86)\Microsoft Visual Studio 9.0\Common7\IDE\devenv.com Boogie.sln /Build Debug
 
     D:\Temp\aste\Boogie\Source\VCGeneration\VC.cs(4223,7): warning CS0162: Unreachable code detected
     D:\Temp\aste\Boogie\Source\VCGeneration\VC.cs(720,15): warning CS0162: Unreachable code detected
@@ -18,156 +18,26 @@
     D:\Temp\aste\Boogie\Source\VCGeneration\Check.cs(445,7): warning CS0162: Unreachable code detected
     D:\Temp\aste\Boogie\Source\VCGeneration\VC.cs(856,29): warning CS0649: Field 'VC.VCGen.Split.first_assert' is never assigned to, and will always have its default value null
     D:\Temp\aste\Boogie\Source\VCGeneration\DoomCheck.cs(177,22): warning CS0169: The field 'VC.DoomCheck._tmpUseFreshBVars' is never used
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\Prover.cs(29,6): warning CS0436: The type 'RepAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'RepAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\Prover.cs(32,6): warning CS0436: The type 'RepAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'RepAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\Prover.cs(34,6): warning CS0436: The type 'RepAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'RepAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\Prover.cs(36,6): warning CS0436: The type 'RepAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'RepAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\Prover.cs(115,6): warning CS0436: The type 'NoDefaultContractAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'NoDefaultContractAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\Prover.cs(116,6): warning CS0436: The type 'VerifyAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'VerifyAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\Prover.cs(255,6): warning CS0436: The type 'RepAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'RepAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\Prover.cs(451,6): warning CS0436: The type 'NotDelayedAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'NotDelayedAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\Prover.cs(454,6): warning CS0436: The type 'VerifyAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'VerifyAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\ProverInterface.cs(21,6): warning CS0436: The type 'NotDelayedAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'NotDelayedAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\ProverInterface.cs(52,6): warning CS0436: The type 'StrictReadonlyAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'StrictReadonlyAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\ProverInterface.cs(53,6): warning CS0436: The type 'AdditiveAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'AdditiveAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\ProverInterface.cs(57,6): warning CS0436: The type 'StrictReadonlyAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'StrictReadonlyAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\ProverInterface.cs(59,6): warning CS0436: The type 'StrictReadonlyAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'StrictReadonlyAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\ProverInterface.cs(61,6): warning CS0436: The type 'StrictReadonlyAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'StrictReadonlyAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\ProverInterface.cs(63,6): warning CS0436: The type 'StrictReadonlyAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'StrictReadonlyAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\ProverInterface.cs(65,6): warning CS0436: The type 'StrictReadonlyAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'StrictReadonlyAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\ProverInterface.cs(67,6): warning CS0436: The type 'StrictReadonlyAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'StrictReadonlyAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\ProverInterface.cs(286,6): warning CS0436: The type 'RepAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'RepAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\ProverInterface.cs(295,6): warning CS0436: The type 'NotDelayedAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'NotDelayedAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\ProverInterface.cs(358,6): warning CS0436: The type 'NoDefaultContractAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'NoDefaultContractAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\ProverInterface.cs(519,6): warning CS0436: The type 'NoDefaultContractAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'NoDefaultContractAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\ProverInterface.cs(602,6): warning CS0436: The type 'NotDelayedAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'NotDelayedAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\ProverInterface.cs(609,6): warning CS0436: The type 'NotDelayedAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'NotDelayedAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\Prover.cs(51,8): warning CS0436: The type 'NoDefaultContractAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'NoDefaultContractAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\Let2ImpliesVisitor.cs(83,24): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\Prover.cs(29,6): warning CS0436: The type 'RepAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'RepAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\Prover.cs(32,6): warning CS0436: The type 'RepAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'RepAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\Prover.cs(34,6): warning CS0436: The type 'RepAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'RepAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\Prover.cs(36,6): warning CS0436: The type 'RepAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'RepAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\Prover.cs(51,8): warning CS0436: The type 'NoDefaultContractAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'NoDefaultContractAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\Prover.cs(55,27): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
     D:\Temp\aste\Boogie\Source\Provers\Simplify\Prover.cs(65,9): warning CS0162: Unreachable code detected
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\Prover.cs(102,7): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\Prover.cs(115,6): warning CS0436: The type 'NoDefaultContractAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'NoDefaultContractAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\Prover.cs(116,6): warning CS0436: The type 'VerifyAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'VerifyAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\Prover.cs(139,7): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\Prover.cs(152,7): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\Prover.cs(164,7): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\Prover.cs(174,7): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\Prover.cs(233,9): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\Prover.cs(255,6): warning CS0436: The type 'RepAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'RepAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\Prover.cs(287,11): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\Prover.cs(295,11): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\Prover.cs(335,7): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
     D:\Temp\aste\Boogie\Source\Provers\Simplify\Prover.cs(339,7): warning CS0162: Unreachable code detected
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\Prover.cs(343,7): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\Prover.cs(355,7): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
     D:\Temp\aste\Boogie\Source\Provers\Simplify\Prover.cs(364,7): warning CS0162: Unreachable code detected
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\Prover.cs(371,7): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
     D:\Temp\aste\Boogie\Source\Provers\Simplify\Prover.cs(380,7): warning CS0162: Unreachable code detected
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\Prover.cs(388,7): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
     D:\Temp\aste\Boogie\Source\Provers\Simplify\Prover.cs(403,7): warning CS0162: Unreachable code detected
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\Prover.cs(410,7): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\Prover.cs(451,6): warning CS0436: The type 'NotDelayedAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'NotDelayedAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\Prover.cs(454,6): warning CS0436: The type 'VerifyAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'VerifyAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\ProverInterface.cs(21,6): warning CS0436: The type 'NotDelayedAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'NotDelayedAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\ProverInterface.cs(52,6): warning CS0436: The type 'StrictReadonlyAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'StrictReadonlyAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\ProverInterface.cs(53,6): warning CS0436: The type 'AdditiveAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'AdditiveAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\ProverInterface.cs(57,6): warning CS0436: The type 'StrictReadonlyAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'StrictReadonlyAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\ProverInterface.cs(59,6): warning CS0436: The type 'StrictReadonlyAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'StrictReadonlyAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\ProverInterface.cs(61,6): warning CS0436: The type 'StrictReadonlyAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'StrictReadonlyAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\ProverInterface.cs(63,6): warning CS0436: The type 'StrictReadonlyAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'StrictReadonlyAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\ProverInterface.cs(65,6): warning CS0436: The type 'StrictReadonlyAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'StrictReadonlyAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\ProverInterface.cs(67,6): warning CS0436: The type 'StrictReadonlyAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'StrictReadonlyAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\ProverInterface.cs(77,26): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\ProverInterface.cs(177,16): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\ProverInterface.cs(206,36): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\ProverInterface.cs(211,26): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\ProverInterface.cs(232,14): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\ProverInterface.cs(286,6): warning CS0436: The type 'RepAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'RepAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\ProverInterface.cs(295,6): warning CS0436: The type 'NotDelayedAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'NotDelayedAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\ProverInterface.cs(358,6): warning CS0436: The type 'NoDefaultContractAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'NoDefaultContractAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\ProverInterface.cs(371,9): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\ProverInterface.cs(468,7): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\ProverInterface.cs(478,7): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\ProverInterface.cs(519,6): warning CS0436: The type 'NoDefaultContractAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'NoDefaultContractAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\ProverInterface.cs(522,32): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\ProverInterface.cs(602,6): warning CS0436: The type 'NotDelayedAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'NotDelayedAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\ProverInterface.cs(609,6): warning CS0436: The type 'NotDelayedAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'NotDelayedAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\ProverInterface.cs(821,40): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Simplify\ProverInterface.cs(835,23): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Simplify\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Z3\Inspector.cs(52,6): warning CS0436: The type 'RepAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs' conflicts with the imported type 'RepAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Z3\Inspector.cs(53,6): warning CS0436: The type 'RepAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs' conflicts with the imported type 'RepAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Z3\Inspector.cs(54,6): warning CS0436: The type 'RepAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs' conflicts with the imported type 'RepAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Z3\Prover.cs(22,6): warning CS0436: The type 'PeerAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs' conflicts with the imported type 'PeerAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Z3\Prover.cs(23,6): warning CS0436: The type 'PeerAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs' conflicts with the imported type 'PeerAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Z3\Prover.cs(63,6): warning CS0436: The type 'CapturedAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs' conflicts with the imported type 'CapturedAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Z3\ProverInterface.cs(36,6): warning CS0436: The type 'NotDelayedAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs' conflicts with the imported type 'NotDelayedAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Z3\Inspector.cs(25,38): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Z3\Inspector.cs(31,86): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Z3\Inspector.cs(52,6): warning CS0436: The type 'RepAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs' conflicts with the imported type 'RepAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Z3\Inspector.cs(53,6): warning CS0436: The type 'RepAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs' conflicts with the imported type 'RepAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Z3\Inspector.cs(54,6): warning CS0436: The type 'RepAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs' conflicts with the imported type 'RepAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Z3\Prover.cs(22,6): warning CS0436: The type 'PeerAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs' conflicts with the imported type 'PeerAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Z3\Prover.cs(23,6): warning CS0436: The type 'PeerAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs' conflicts with the imported type 'PeerAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Z3\Prover.cs(33,26): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Z3\Prover.cs(54,25): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Z3\Prover.cs(63,6): warning CS0436: The type 'CapturedAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs' conflicts with the imported type 'CapturedAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Z3\Prover.cs(68,44): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Z3\Prover.cs(317,24): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Z3\Prover.cs(329,26): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Z3\Prover.cs(428,11): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Z3\Prover.cs(465,27): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Z3\Prover.cs(533,7): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Z3\Prover.cs(566,25): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Z3\Prover.cs(699,54): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Z3\Prover.cs(745,52): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Z3\Prover.cs(890,54): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Z3\Prover.cs(948,25): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Z3\Prover.cs(992,14): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Z3\Prover.cs(1004,25): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Z3\TypeDeclCollector.cs(32,26): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Z3\TypeDeclCollector.cs(96,24): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Z3\TypeDeclCollector.cs(104,24): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Z3\ProverInterface.cs(36,6): warning CS0436: The type 'NotDelayedAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs' conflicts with the imported type 'NotDelayedAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Z3\ProverInterface.cs(165,25): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Z3\ProverInterface.cs(199,24): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Z3\ProverInterface.cs(383,32): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\Z3\ProverInterface.cs(397,32): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\Z3\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\SMTLib\ProverInterface.cs(42,6): warning CS0436: The type 'NotDelayedAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\cce.cs' conflicts with the imported type 'NotDelayedAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\SMTLib\ProverInterface.cs(158,6): warning CS0436: The type 'NoDefaultContractAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\cce.cs' conflicts with the imported type 'NoDefaultContractAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\SMTLib\SMTLibLineariser.cs(65,14): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\SMTLib\SMTLibLineariser.cs(119,19): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\SMTLib\SMTLibLineariser.cs(249,21): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\SMTLib\SMTLibLineariser.cs(261,46): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\SMTLib\SMTLibLineariser.cs(290,23): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\SMTLib\SMTLibLineariser.cs(474,25): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\SMTLib\SMTLibLineariser.cs(482,25): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\SMTLib\SMTLibLineariser.cs(490,25): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\SMTLib\SMTLibLineariser.cs(500,25): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\SMTLib\SMTLibLineariser.cs(511,25): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\SMTLib\SMTLibLineariser.cs(540,27): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\SMTLib\SMTLibLineariser.cs(580,50): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\SMTLib\SMTLibLineariser.cs(682,44): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\SMTLib\SMTLibLineariser.cs(689,44): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\SMTLib\ProverInterface.cs(35,26): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\SMTLib\ProverInterface.cs(42,6): warning CS0436: The type 'NotDelayedAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\cce.cs' conflicts with the imported type 'NotDelayedAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\SMTLib\ProverInterface.cs(147,62): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\SMTLib\ProverInterface.cs(158,6): warning CS0436: The type 'NoDefaultContractAttribute' in 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\cce.cs' conflicts with the imported type 'NoDefaultContractAttribute' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\SMTLib\ProverInterface.cs(249,11): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\SMTLib\ProverInterface.cs(271,31): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\SMTLib\TypeDeclCollector.cs(52,24): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\cce.cs'.
-    D:\Temp\aste\Boogie\Source\Provers\SMTLib\TypeDeclCollector.cs(60,24): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\Provers\SMTLib\cce.cs'.
     D:\Temp\aste\Boogie\Source\AbsInt\ExprFactories.cs(111,7): warning CS0162: Unreachable code detected
     D:\Temp\aste\Boogie\Source\AbsInt\ExprFactories.cs(290,7): warning CS0162: Unreachable code detected
     D:\Temp\aste\Boogie\Source\AbsInt\ExprFactories.cs(308,7): warning CS0162: Unreachable code detected
     D:\Temp\aste\Boogie\Source\AbsInt\LoopInvariantsOnDemand.cs(44,7): warning CC1032: Method 'Microsoft.Boogie.AbstractInterpretation.FreeVariablesVisitor.Default(optional(Microsoft.Contracts.NonNullType) Microsoft.AbstractInterpretationFramework.IExpr)' overrides 'Microsoft.AbstractInterpretationFramework.ExprVisitor.Default(optional(Microsoft.Contracts.NonNullType) Microsoft.AbstractInterpretationFramework.IExpr)', thus cannot add Requires.
     D:\Temp\aste\Boogie\Source\AbsInt\LoopInvariantsOnDemand.cs(65,7): warning CC1032: Method 'Microsoft.Boogie.AbstractInterpretation.FreeVariablesVisitor.VisitFunApp(optional(Microsoft.Contracts.NonNullType) Microsoft.AbstractInterpretationFramework.IFunApp)' overrides 'Microsoft.AbstractInterpretationFramework.ExprVisitor.VisitFunApp(optional(Microsoft.Contracts.NonNullType) Microsoft.AbstractInterpretationFramework.IFunApp)', thus cannot add Requires.
     D:\Temp\aste\Boogie\Source\AbsInt\LoopInvariantsOnDemand.cs(74,7): warning CC1032: Method 'Microsoft.Boogie.AbstractInterpretation.FreeVariablesVisitor.VisitFunction(optional(Microsoft.Contracts.NonNullType) Microsoft.AbstractInterpretationFramework.IFunction)' overrides 'Microsoft.AbstractInterpretationFramework.ExprVisitor.VisitFunction(optional(Microsoft.Contracts.NonNullType) Microsoft.AbstractInterpretationFramework.IFunction)', thus cannot add Requires.
+    D:\Temp\aste\Boogie\Source\BoogieDriver\BoogieDriver.cs(38,25): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\BoogieDriver\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\BoogieDriver\cce.cs'.
+    D:\Temp\aste\Boogie\Source\BoogieDriver\BoogieDriver.cs(190,73): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\BoogieDriver\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\BoogieDriver\cce.cs'.
+    D:\Temp\aste\Boogie\Source\BoogieDriver\BoogieDriver.cs(226,25): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\BoogieDriver\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\BoogieDriver\cce.cs'.
+    D:\Temp\aste\Boogie\Source\BoogieDriver\BoogieDriver.cs(283,13): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\BoogieDriver\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\BoogieDriver\cce.cs'.
+    D:\Temp\aste\Boogie\Source\BoogieDriver\BoogieDriver.cs(357,25): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\BoogieDriver\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\BoogieDriver\cce.cs'.
+    D:\Temp\aste\Boogie\Source\BoogieDriver\BoogieDriver.cs(470,48): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\BoogieDriver\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\BoogieDriver\cce.cs'.
+    D:\Temp\aste\Boogie\Source\BoogieDriver\BoogieDriver.cs(571,76): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\BoogieDriver\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\BoogieDriver\cce.cs'.
+    D:\Temp\aste\Boogie\Source\BoogieDriver\BoogieDriver.cs(614,25): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\BoogieDriver\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\BoogieDriver\cce.cs'.
+    D:\Temp\aste\Boogie\Source\BoogieDriver\BoogieDriver.cs(732,7): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\BoogieDriver\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\BoogieDriver\cce.cs'.
     warning CS0162
     warning CS0162
     warning CS0162
@@ -177,58 +47,13 @@
     warning CS0162
     warning CS0649
     warning CS0169
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
     warning CS0162
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
     warning CS0162
-    warning CS0436
-    warning CS0436
     warning CS0162
-    warning CS0436
     warning CS0162
-    warning CS0436
+    warning CS0162
+    warning CS0162
+    warning CS0162
     warning CS0162
     warning CS0436
     warning CS0436
@@ -239,6 +64,18 @@
     warning CS0436
     warning CS0436
     warning CS0436
+[2010-07-31 07:05:52] C:\Program Files (x86)\Microsoft Visual Studio 9.0\Common7\IDE\devenv.com Dafny.sln /Build Debug
+
+    D:\Temp\aste\Boogie\Source\DafnyDriver\DafnyDriver.cs(39,24): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\DafnyDriver\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\DafnyDriver\cce.cs'.
+    D:\Temp\aste\Boogie\Source\DafnyDriver\DafnyDriver.cs(187,73): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\DafnyDriver\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\DafnyDriver\cce.cs'.
+    D:\Temp\aste\Boogie\Source\DafnyDriver\DafnyDriver.cs(220,21): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\DafnyDriver\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\DafnyDriver\cce.cs'.
+    D:\Temp\aste\Boogie\Source\DafnyDriver\DafnyDriver.cs(302,13): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\DafnyDriver\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\DafnyDriver\cce.cs'.
+    D:\Temp\aste\Boogie\Source\DafnyDriver\DafnyDriver.cs(371,25): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\DafnyDriver\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\DafnyDriver\cce.cs'.
+    D:\Temp\aste\Boogie\Source\DafnyDriver\DafnyDriver.cs(426,23): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\DafnyDriver\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\DafnyDriver\cce.cs'.
+    D:\Temp\aste\Boogie\Source\DafnyDriver\DafnyDriver.cs(457,44): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\DafnyDriver\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\DafnyDriver\cce.cs'.
+    D:\Temp\aste\Boogie\Source\DafnyDriver\DafnyDriver.cs(572,76): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\DafnyDriver\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\DafnyDriver\cce.cs'.
+    D:\Temp\aste\Boogie\Source\DafnyDriver\DafnyDriver.cs(617,48): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\DafnyDriver\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\DafnyDriver\cce.cs'.
+    D:\Temp\aste\Boogie\Source\DafnyDriver\DafnyDriver.cs(735,7): warning CS0436: The type 'cce' in 'D:\Temp\aste\Boogie\Source\DafnyDriver\cce.cs' conflicts with the imported type 'cce' in 'd:\temp\aste\Boogie\Source\VCGeneration\bin\Debug\VCGeneration.dll'. Using the type defined in 'D:\Temp\aste\Boogie\Source\DafnyDriver\cce.cs'.
     warning CS0436
     warning CS0436
     warning CS0436
@@ -249,87 +86,5 @@
     warning CS0436
     warning CS0436
     warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0436
-    warning CS0162
-    warning CS0162
-    warning CS0162
-[2010-07-29 07:06:02] [Error] C:\Program Files (x86)\Microsoft Visual Studio 9.0\Common7\IDE\devenv.com Dafny.sln /Build Debug
-
-    C:\Windows\Microsoft.NET\Framework\v3.5\Microsoft.Common.targets : warning MSB3245: Could not resolve this reference. Could not locate the assembly "System.Compiler, Version=1.0.21125.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL". Check to make sure the assembly exists on disk. If this reference is required by your code, you may get compilation errors.
-    C:\Windows\Microsoft.NET\Framework\v3.5\Microsoft.Common.targets : warning MSB3245: Could not resolve this reference. Could not locate the assembly "Microsoft.SpecSharp, Version=1.0.21125.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL". Check to make sure the assembly exists on disk. If this reference is required by your code, you may get compilation errors.
-    C:\Windows\Microsoft.NET\Framework\v3.5\Microsoft.Common.targets : warning MSB3245: Could not resolve this reference. Could not locate the assembly "System.Compiler.Runtime, Version=1.0.21125.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL". Check to make sure the assembly exists on disk. If this reference is required by your code, you may get compilation errors.
-    C:\Windows\Microsoft.NET\Framework\v3.5\Microsoft.Common.targets : warning MSB3247: Found conflicts between different versions of the same dependent assembly.
-    D:\Temp\aste\Boogie\Source\DafnyDriver\DafnyDriver.cs(23,22): error CS0234: The type or namespace name 'Compiler' does not exist in the namespace 'System' (are you missing an assembly reference?)
-    1 error
-    1 failed
+[2010-07-31 07:29:19] 0 out of 26 test(s) in D:\Temp\aste\Boogie\Test\alltests.txt failed
+# [2010-07-31 07:31:03] Released nightly of Boogie
author	codeplexbot <unknown>	2010-07-31 05:30:53 +0000
committer	codeplexbot <unknown>	2010-07-31 05:30:53 +0000
commit	1679c064cdb5c667d9f8e46eaac58a65c66d8b11 (patch)
tree	c3cb0e7adac224b4d1c83023dd7003971b2cd2f4 /_admin
parent	f513d6f3716b7c963e30ca3d004cf6a40d2f68c5 (diff)