From 1679c064cdb5c667d9f8e46eaac58a65c66d8b11 Mon Sep 17 00:00:00 2001 From: codeplexbot Date: Sat, 31 Jul 2010 05:30:53 +0000 Subject: Boogie build succeeded --- _admin/Boogie/aste/summary.log | 309 +++++------------------------------------ 1 file changed, 32 insertions(+), 277 deletions(-) (limited to '_admin') 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 -- cgit v1.2.3