Factored out the ParserHelper class into a separate project and updated the files generated by Coco/R.

This was done to support sharing of the Coco/R .frame files with Spec#.

21 files changed, 315 insertions, 150 deletions

diff --git a/Binaries/..svnbridge/Microsoft.Contracts.dll b/Binaries/..svnbridge/Microsoft.Contracts.dll
new file mode 100644
index 00000000..08149303
--- /dev/null
+++ b/Binaries/..svnbridge/Microsoft.Contracts.dll
@@ -0,0 +1 @@
+<?xml version="1.0" encoding="utf-8"?><ItemProperties xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema"><Properties><Property><Name>svn:mime-type</Name><Value>application/octet-stream</Value></Property></Properties></ItemProperties>
\ No newline at end of file
diff --git a/Binaries/Microsoft.Contracts.dll b/Binaries/Microsoft.Contracts.dll
new file mode 100644
index 00000000..fac85ccf
--- /dev/null
+++ b/Binaries/Microsoft.Contracts.dll
diff --git a/Source/AbsInt/AbsInt.csproj b/Source/AbsInt/AbsInt.csproj
index 433195a6..1c416a97 100644
--- a/Source/AbsInt/AbsInt.csproj
+++ b/Source/AbsInt/AbsInt.csproj
@@ -130,6 +130,10 @@
       <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>

       <Name>Core</Name>

     </ProjectReference>

+    <ProjectReference Include="..\ParserHelper\ParserHelper.csproj">

+      <Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project>

+      <Name>ParserHelper</Name>

+    </ProjectReference>

   </ItemGroup>

   <ItemGroup>

     <Folder Include="Properties\" />

diff --git a/Source/Boogie.sln b/Source/Boogie.sln
index afcb1262..3f459d16 100644
--- a/Source/Boogie.sln
+++ b/Source/Boogie.sln
@@ -35,6 +35,8 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ModelViewer", "ModelViewer\
 EndProject

 Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Model", "Model\Model.csproj", "{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}"

 EndProject

+Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ParserHelper", "ParserHelper\ParserHelper.csproj", "{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}"

+EndProject

 Global

 	GlobalSection(SolutionConfigurationPlatforms) = preSolution

 		Debug|.NET = Debug|.NET

@@ -345,6 +347,24 @@ Global
 		{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU

 		{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU

 		{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}.z3apidebug|x86.ActiveCfg = Release|Any CPU

+		{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Debug|.NET.ActiveCfg = Debug|Any CPU

+		{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Debug|Any CPU.ActiveCfg = Debug|Any CPU

+		{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Debug|Any CPU.Build.0 = Debug|Any CPU

+		{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Debug|Mixed Platforms.ActiveCfg = Debug|Any CPU

+		{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Debug|Mixed Platforms.Build.0 = Debug|Any CPU

+		{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Debug|x86.ActiveCfg = Debug|Any CPU

+		{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Release|.NET.ActiveCfg = Release|Any CPU

+		{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Release|Any CPU.ActiveCfg = Release|Any CPU

+		{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Release|Any CPU.Build.0 = Release|Any CPU

+		{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Release|Mixed Platforms.ActiveCfg = Release|Any CPU

+		{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Release|Mixed Platforms.Build.0 = Release|Any CPU

+		{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.Release|x86.ActiveCfg = Release|Any CPU

+		{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|.NET.ActiveCfg = Release|Any CPU

+		{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|Any CPU.ActiveCfg = Release|Any CPU

+		{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|Any CPU.Build.0 = Release|Any CPU

+		{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|Mixed Platforms.ActiveCfg = Release|Any CPU

+		{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|Mixed Platforms.Build.0 = Release|Any CPU

+		{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}.z3apidebug|x86.ActiveCfg = Release|Any CPU

 	EndGlobalSection

 	GlobalSection(SolutionProperties) = preSolution

 		HideSolutionNode = FALSE

diff --git a/Source/BoogieDriver/BoogieDriver.csproj b/Source/BoogieDriver/BoogieDriver.csproj
index df548f1a..1becfe9e 100644
--- a/Source/BoogieDriver/BoogieDriver.csproj
+++ b/Source/BoogieDriver/BoogieDriver.csproj
@@ -132,6 +132,10 @@
       <Project>{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}</Project>

       <Name>Graph</Name>

     </ProjectReference>

+    <ProjectReference Include="..\ParserHelper\ParserHelper.csproj">

+      <Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project>

+      <Name>ParserHelper</Name>

+    </ProjectReference>

     <ProjectReference Include="..\Provers\Isabelle\Isabelle.csproj">

       <Project>{435D5BD0-6F62-49F8-BB24-33E2257519AD}</Project>

       <Name>Isabelle</Name>

diff --git a/Source/CodeContractsExtender/CodeContractsExtender.csproj b/Source/CodeContractsExtender/CodeContractsExtender.csproj
index 48c5821e..d957cec7 100644
--- a/Source/CodeContractsExtender/CodeContractsExtender.csproj
+++ b/Source/CodeContractsExtender/CodeContractsExtender.csproj
@@ -10,7 +10,7 @@
     <AppDesignerFolder>Properties</AppDesignerFolder>

     <RootNamespace>CodeContractsExtender</RootNamespace>

     <AssemblyName>CodeContractsExtender</AssemblyName>

-    <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>

+    <TargetFrameworkVersion>v3.5</TargetFrameworkVersion>

     <FileAlignment>512</FileAlignment>

     <SignAssembly>true</SignAssembly>

     <AssemblyOriginatorKeyFile>..\InterimKey.snk</AssemblyOriginatorKeyFile>

@@ -99,6 +99,10 @@
     <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>

   </PropertyGroup>

   <ItemGroup>

+    <Reference Include="Microsoft.Contracts, Version=1.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

+      <SpecificVersion>False</SpecificVersion>

+      <HintPath>..\..\Binaries\Microsoft.Contracts.dll</HintPath>

+    </Reference>

     <Reference Include="System" />

     <Reference Include="System.Core">

       <RequiredTargetFramework>3.5</RequiredTargetFramework>

diff --git a/Source/Core/Core.csproj b/Source/Core/Core.csproj
index 625ab9b6..145d56e3 100644
--- a/Source/Core/Core.csproj
+++ b/Source/Core/Core.csproj
@@ -118,7 +118,6 @@
     <Compile Include="LoopUnroll.cs" />

     <Compile Include="OOLongUtil.cs" />

     <Compile Include="Parser.cs" />

-    <Compile Include="ParserHelper.cs" />

     <Compile Include="PureCollections.cs" />

     <Compile Include="ResolutionContext.cs" />

     <Compile Include="Scanner.cs" />

@@ -146,6 +145,10 @@
       <Project>{69A2B0B8-BCAC-4101-AE7A-556FCC58C06E}</Project>

       <Name>Graph</Name>

     </ProjectReference>

+    <ProjectReference Include="..\ParserHelper\ParserHelper.csproj">

+      <Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project>

+      <Name>ParserHelper</Name>

+    </ProjectReference>

   </ItemGroup>

   <ItemGroup>

     <Folder Include="Properties\" />

diff --git a/Source/Core/Makefile b/Source/Core/Makefile
index a5061138..192a16db 100644
--- a/Source/Core/Makefile
+++ b/Source/Core/Makefile
@@ -1,11 +1,11 @@
-COCO = ..\..\Binaries\Coco.exe

+COCO = Coco.exe

 

 # ###############################################################################

 # The frame files are no longer in this directory. They must be downloaded

 # from http://boogiepartners.codeplex.com/. Update the FRAME_DIR variable to

 # point to whatever directory you install that into.

 # ###############################################################################

-FRAME_DIR = c:\BoogiePartners\CocoR\Modified

+FRAME_DIR = ..\..\..\boogiepartners\CocoR\Modified

 

 # "all" depends on 2 files, really (Parser.cs and Scanner.cs), but they

 # are both generated in one go and I don't know a better way to tell

diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs
index 0d906de4..7898e26f 100644
--- a/Source/Core/Parser.cs
+++ b/Source/Core/Parser.cs
@@ -30,7 +30,7 @@ public class Parser {
 	const bool T = true;

 	const bool x = false;

 	const int minErrDist = 2;

-	

+

 	public Scanner/*!*/ scanner;

 	public Errors/*!*/  errors;

 

@@ -140,10 +140,10 @@ private class BvBounds : Expr {
 		if (errDist >= minErrDist) errors.SemErr(t, msg);

 		errDist = 0;

 	}

-	

-    public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {

-      Contract.Requires(tok != null);

-      Contract.Requires(msg != null);

+

+	public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {

+	  Contract.Requires(tok != null);

+	  Contract.Requires(msg != null);

 	  errors.SemErr(tok, msg);

 	}

 

@@ -156,15 +156,15 @@ private class BvBounds : Expr {
 			la = t;

 		}

 	}

-	

+

 	void Expect (int n) {

 		if (la.kind==n) Get(); else { SynErr(n); }

 	}

-	

+

 	bool StartOf (int s) {

 		return set[s, la.kind];

 	}

-	

+

 	void ExpectWeak (int n, int follow) {

 		if (la.kind == n) Get();

 		else {

@@ -188,7 +188,7 @@ private class BvBounds : Expr {
 		}

 	}

 

-	

+

 	void BoogiePL() {

 		VariableSeq/*!*/ vs;

 		DeclarationSeq/*!*/ ds;

@@ -2004,13 +2004,13 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
 

 	public void Parse() {

 		la = new Token();

-		la.val = "";		

+		la.val = "";

 		Get();

 		BoogiePL();

 

-    Expect(0);

+		Expect(0);

 	}

-	

+

 	static readonly bool[,]/*!*/ set = {

 		{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

 		{x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,T, T,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

@@ -2035,18 +2035,20 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) {
 public class Errors {

 	public int count = 0;                                    // number of errors detected

 	public System.IO.TextWriter/*!*/ errorStream = Console.Out;   // error messages go to this stream

-  public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text

-  public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text

-  

+	public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text

+	public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text

+

 	public void SynErr(string filename, int line, int col, int n) {

-    SynErr(filename, line, col, GetSyntaxErrorString(n));

-  }

-	public virtual void SynErr(string filename, int line, int col, string msg) {

-	  Contract.Requires(msg != null);

+		SynErr(filename, line, col, GetSyntaxErrorString(n));

+	}

+

+	public virtual void SynErr(string filename, int line, int col, string/*!*/ msg) {

+		Contract.Requires(msg != null);

 		errorStream.WriteLine(errMsgFormat, filename, line, col, msg);

 		count++;

-  }

-  string GetSyntaxErrorString(int n) {

+	}

+

+	string GetSyntaxErrorString(int n) {

 		string s;

 		switch (n) {

 			case 0: s = "EOF expected"; break;

@@ -2181,7 +2183,7 @@ public class Errors {
 

 			default: s = "error " + n; break;

 		}

-    return s;

+		return s;

 	}

 

 	public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {  // semantic errors

@@ -2189,8 +2191,9 @@ public class Errors {
 		Contract.Requires(msg != null);

 		SemErr(tok.filename, tok.line, tok.col, msg);

 	}

+

 	public virtual void SemErr(string filename, int line, int col, string/*!*/ msg) {

-	  Contract.Requires(msg != null);

+		Contract.Requires(msg != null);

 		errorStream.WriteLine(errMsgFormat, filename, line, col, msg);

 		count++;

 	}

diff --git a/Source/Core/Scanner.cs b/Source/Core/Scanner.cs
index faab5837..7c3522ca 100644
--- a/Source/Core/Scanner.cs
+++ b/Source/Core/Scanner.cs
@@ -19,7 +19,7 @@ public class Buffer {
 	//    a) whole stream in buffer

 	//    b) part of stream in buffer

 	// 2) non seekable stream (network, console)

-  

+

 	public const int EOF = 65535 + 1; // char.MaxValue + 1;

 	const int MIN_BUFFER_LENGTH = 1024; // 1KB

 	const int MAX_BUFFER_LENGTH = MIN_BUFFER_LENGTH * 64; // 64KB

@@ -31,15 +31,17 @@ public class Buffer {
 	Stream/*!*/ stream;      // input stream (seekable)

 	bool isUserStream;  // was the stream opened by the user?

 

-[ContractInvariantMethod]

-void ObjectInvariant(){

-  Contract.Invariant(buf != null);

-  Contract.Invariant(stream != null);}

-    [NotDelayed]

-	public Buffer (Stream/*!*/ s, bool isUserStream) :base() {

+	[ContractInvariantMethod]

+	void ObjectInvariant(){

+		Contract.Invariant(buf != null);

+		Contract.Invariant(stream != null);

+	}

+

+//  [NotDelayed]

+	public Buffer (Stream/*!*/ s, bool isUserStream) : base() {

 	  Contract.Requires(s != null);

 		stream = s; this.isUserStream = isUserStream;

-		

+

 		int fl, bl;

 		if (s.CanSeek) {

 			fl = (int) s.Length;

@@ -51,12 +53,12 @@ void ObjectInvariant(){
 

 		buf = new byte[(bl>0) ? bl : MIN_BUFFER_LENGTH];

 		fileLen = fl;  bufLen = bl;

-		

+

 		if (fileLen > 0) Pos = 0; // setup buffer to position 0 (start)

 		else bufPos = 0; // index 0 is already after the file, thus Pos = 0 is invalid

 		if (bufLen == fileLen && s.CanSeek) Close();

 	}

-	

+

 	protected Buffer(Buffer/*!*/ b) { // called in UTF8Buffer constructor

 	  Contract.Requires(b != null);

 		buf = b.buf;

@@ -73,14 +75,14 @@ void ObjectInvariant(){
 	}

 

 	~Buffer() { Close(); }

-	

+

 	protected void Close() {

 		if (!isUserStream && stream != null) {

 			stream.Close();

 			//stream = null;

 		}

 	}

-	

+

 	public virtual int Read () {

 		if (bufPos < bufLen) {

 			return buf[bufPos++];

@@ -100,7 +102,7 @@ void ObjectInvariant(){
 		Pos = curPos;

 		return ch;

 	}

-	

+

 	public string/*!*/ GetString (int beg, int end) {

 	  Contract.Ensures(Contract.Result<string>() != null);

 		int len = 0;

@@ -139,7 +141,7 @@ void ObjectInvariant(){
 			}

 		}

 	}

-	

+

 	// Read the next chunk of bytes from the stream, increases the buffer

 	// if needed and updates the fields fileLen and bufLen.

 	// Returns the number of bytes read.

@@ -213,19 +215,20 @@ public class Scanner {
 	const int noSym = 88;

 

 

-[ContractInvariantMethod]

-void objectInvariant(){

-  Contract.Invariant(buffer!=null);

-  Contract.Invariant(t != null);

-  Contract.Invariant(start != null);

-  Contract.Invariant(tokens != null);

-  Contract.Invariant(pt != null);

-  Contract.Invariant(tval != null);

-  Contract.Invariant(Filename != null);

-  Contract.Invariant(errorHandler != null);

-}

+	[ContractInvariantMethod]

+	void objectInvariant(){

+		Contract.Invariant(buffer!=null);

+		Contract.Invariant(t != null);

+		Contract.Invariant(start != null);

+		Contract.Invariant(tokens != null);

+		Contract.Invariant(pt != null);

+		Contract.Invariant(tval != null);

+		Contract.Invariant(Filename != null);

+		Contract.Invariant(errorHandler != null);

+	}

+

 	public Buffer/*!*/ buffer; // scanner buffer

-	

+

 	Token/*!*/ t;          // current token

 	int ch;           // current input character

 	int pos;          // byte position of current character

@@ -236,13 +239,13 @@ void objectInvariant(){
 

 	Token/*!*/ tokens;     // list of tokens already peeked (first token is a dummy)

 	Token/*!*/ pt;         // current peek token

-	

+

 	char[]/*!*/ tval = new char[128]; // text of current token

 	int tlen;         // length of current token

-	

+

 	private string/*!*/ Filename;

 	private Errors/*!*/ errorHandler;

-	

+

 	static Scanner() {

 		start = new Hashtable(128);

 		for (int i = 35; i <= 36; ++i) start[i] = 2;

@@ -291,9 +294,9 @@ void objectInvariant(){
 		start[Buffer.EOF] = -1;

 

 	}

-	

-	[NotDelayed]

-	public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) :base(){

+

+//	[NotDelayed]

+	public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) : base() {

 	  Contract.Requires(fileName != null);

 	  Contract.Requires(errorHandler != null);

 		this.errorHandler = errorHandler;

@@ -303,15 +306,14 @@ void objectInvariant(){
 			Stream stream = new FileStream(fileName, FileMode.Open, FileAccess.Read, FileShare.Read);

 			buffer = new Buffer(stream, false);

 			Filename = fileName;

-			

 			Init();

 		} catch (IOException) {

 			throw new FatalError("Cannot open file " + fileName);

 		}

 	}

-	

-	[NotDelayed]

-	public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) :base(){

+

+//	[NotDelayed]

+	public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) : base() {

 	  Contract.Requires(s != null);

 	  Contract.Requires(errorHandler != null);

 	  Contract.Requires(fileName != null);

@@ -320,10 +322,9 @@ void objectInvariant(){
 		buffer = new Buffer(s, true);

 		this.errorHandler = errorHandler;

 		this.Filename = fileName;

-		

 		Init();

 	}

-	

+

 	void Init() {

 		pos = -1; line = 1; col = 0;

 		oldEols = 0;

@@ -344,11 +345,11 @@ void objectInvariant(){
 	Contract.Ensures(Contract.Result<string>() != null);

 	  int p = buffer.Pos;

 	  int ch = buffer.Read();

-      // replace isolated '\r' by '\n' in order to make

+	  // replace isolated '\r' by '\n' in order to make

 	  // eol handling uniform across Windows, Unix and Mac

 	  if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;

 	  while (ch != EOL && ch != Buffer.EOF){

-	    ch = buffer.Read();

+		ch = buffer.Read();

 		// replace isolated '\r' by '\n' in order to make

 		// eol handling uniform across Windows, Unix and Mac

 		if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;

@@ -359,7 +360,7 @@ void objectInvariant(){
 	}

 

 	void NextCh() {

-		if (oldEols > 0) { ch = EOL; oldEols--; } 

+		if (oldEols > 0) { ch = EOL; oldEols--; }

 		else {

 //			pos = buffer.Pos;

 //			ch = buffer.Read(); col++;

@@ -367,9 +368,9 @@ void objectInvariant(){
 //			// eol handling uniform across Windows, Unix and Mac

 //			if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;

 //			if (ch == EOL) { line++; col = 0; }

-			

+

 			while (true) {

-			    pos = buffer.Pos;

+				pos = buffer.Pos;

 				ch = buffer.Read(); col++;

 				// replace isolated '\r' by '\n' in order to make

 				// eol handling uniform across Windows, Unix and Mac

@@ -419,7 +420,7 @@ void objectInvariant(){
 				return;

 			  }

 

-			

+

 		}

 

 	}

@@ -539,10 +540,13 @@ void objectInvariant(){
 		t.pos = pos; t.col = col; t.line = line;

 		t.filename = this.Filename;

 		int state;

-		if (start.ContainsKey(ch)) { state = (int) cce.NonNull( start[ch]); }

+		if (start.ContainsKey(ch)) {

+			Contract.Assert(start[ch] != null);

+			state = (int) start[ch];

+		}

 		else { state = 0; }

 		tlen = 0; AddCh();

-		

+

 		switch (state) {

 			case -1: { t.kind = eofSym; break; } // NextCh already done

 			case 0: {

@@ -711,14 +715,14 @@ void objectInvariant(){
 		t.val = new String(tval, 0, tlen);

 		return t;

 	}

-	

+

 	private void SetScannerBehindT() {

 		buffer.Pos = t.pos;

 		NextCh();

 		line = t.line; col = t.col;

 		for (int i = 0; i < tlen; i++) NextCh();

 	}

-	

+

 	// get the next token (possibly a token already seen during peeking)

 	public Token/*!*/ Scan () {

 	 Contract.Ensures(Contract.Result<Token>() != null);

@@ -739,7 +743,7 @@ void objectInvariant(){
 			}

 			pt = pt.next;

 		} while (pt.kind > maxT); // skip pragmas

-	

+

 		return pt;

 	}

 

diff --git a/Source/Dafny/DafnyPipeline.csproj b/Source/Dafny/DafnyPipeline.csproj
index a4206998..7f063c2c 100644
--- a/Source/Dafny/DafnyPipeline.csproj
+++ b/Source/Dafny/DafnyPipeline.csproj
@@ -98,6 +98,9 @@
       <SpecificVersion>False</SpecificVersion>

       <HintPath>..\..\Binaries\Core.dll</HintPath>

     </Reference>

+    <Reference Include="ParserHelper">

+      <HintPath>..\..\Binaries\ParserHelper.dll</HintPath>

+    </Reference>

     <Reference Include="System" />

     <Reference Include="System.Core">

       <RequiredTargetFramework>3.5</RequiredTargetFramework>

diff --git a/Source/Dafny/Makefile b/Source/Dafny/Makefile
index 3fc283a0..cc36590c 100644
--- a/Source/Dafny/Makefile
+++ b/Source/Dafny/Makefile
@@ -1,11 +1,11 @@
-COCO = ..\..\Binaries\Coco.exe

+COCO = Coco.exe

 

 # ###############################################################################

 # The frame files are no longer in this directory. They must be downloaded

 # from http://boogiepartners.codeplex.com/. Update the FRAME_DIR variable to

 # point to whatever directory you install that into.

 # ###############################################################################

-FRAME_DIR = c:\BoogiePartners\CocoR\Modified

+FRAME_DIR = ..\..\..\boogiepartners\CocoR\Modified

 

 # "all" depends on 2 files, really (Parser.cs and Scanner.cs), but they

 # are both generated in one go and I don't know a better way to tell

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 2dc77103..ff6f2690 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -25,7 +25,7 @@ public class Parser {
 	const bool T = true;

 	const bool x = false;

 	const int minErrDist = 2;

-	

+

 	public Scanner/*!*/ scanner;

 	public Errors/*!*/  errors;

 

@@ -161,10 +161,10 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		if (errDist >= minErrDist) errors.SemErr(t, msg);

 		errDist = 0;

 	}

-	

-    public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {

-      Contract.Requires(tok != null);

-      Contract.Requires(msg != null);

+

+	public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {

+	  Contract.Requires(tok != null);

+	  Contract.Requires(msg != null);

 	  errors.SemErr(tok, msg);

 	}

 

@@ -177,15 +177,15 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			la = t;

 		}

 	}

-	

+

 	void Expect (int n) {

 		if (la.kind==n) Get(); else { SynErr(n); }

 	}

-	

+

 	bool StartOf (int s) {

 		return set[s, la.kind];

 	}

-	

+

 	void ExpectWeak (int n, int follow) {

 		if (la.kind == n) Get();

 		else {

@@ -209,7 +209,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		}

 	}

 

-	

+

 	void Dafny() {

 		ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt;

 		Attributes attrs;  IToken/*!*/ id;  List<string/*!*/> theImports;

@@ -2052,13 +2052,13 @@ List<Expression/*!*/>/*!*/ decreases) {
 

 	public void Parse() {

 		la = new Token();

-		la.val = "";		

+		la.val = "";

 		Get();

 		Dafny();

 

-    Expect(0);

+		Expect(0);

 	}

-	

+

 	static readonly bool[,]/*!*/ set = {

 		{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

 		{x,x,x,x, x,T,x,x, x,T,T,T, T,T,T,x, T,x,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

@@ -2086,18 +2086,20 @@ List<Expression/*!*/>/*!*/ decreases) {
 public class Errors {

 	public int count = 0;                                    // number of errors detected

 	public System.IO.TextWriter/*!*/ errorStream = Console.Out;   // error messages go to this stream

-  public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text

-  public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text

-  

+	public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text

+	public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text

+

 	public void SynErr(string filename, int line, int col, int n) {

-    SynErr(filename, line, col, GetSyntaxErrorString(n));

-  }

-	public virtual void SynErr(string filename, int line, int col, string msg) {

-	  Contract.Requires(msg != null);

+		SynErr(filename, line, col, GetSyntaxErrorString(n));

+	}

+

+	public virtual void SynErr(string filename, int line, int col, string/*!*/ msg) {

+		Contract.Requires(msg != null);

 		errorStream.WriteLine(errMsgFormat, filename, line, col, msg);

 		count++;

-  }

-  string GetSyntaxErrorString(int n) {

+	}

+

+	string GetSyntaxErrorString(int n) {

 		string s;

 		switch (n) {

 			case 0: s = "EOF expected"; break;

@@ -2249,7 +2251,7 @@ public class Errors {
 

 			default: s = "error " + n; break;

 		}

-    return s;

+		return s;

 	}

 

 	public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {  // semantic errors

@@ -2257,8 +2259,9 @@ public class Errors {
 		Contract.Requires(msg != null);

 		SemErr(tok.filename, tok.line, tok.col, msg);

 	}

+

 	public virtual void SemErr(string filename, int line, int col, string/*!*/ msg) {

-	  Contract.Requires(msg != null);

+		Contract.Requires(msg != null);

 		errorStream.WriteLine(errMsgFormat, filename, line, col, msg);

 		count++;

 	}

diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs
index de87c6ad..42c4f661 100644
--- a/Source/Dafny/Scanner.cs
+++ b/Source/Dafny/Scanner.cs
@@ -19,7 +19,7 @@ public class Buffer {
 	//    a) whole stream in buffer

 	//    b) part of stream in buffer

 	// 2) non seekable stream (network, console)

-  

+

 	public const int EOF = 65535 + 1; // char.MaxValue + 1;

 	const int MIN_BUFFER_LENGTH = 1024; // 1KB

 	const int MAX_BUFFER_LENGTH = MIN_BUFFER_LENGTH * 64; // 64KB

@@ -31,15 +31,17 @@ public class Buffer {
 	Stream/*!*/ stream;      // input stream (seekable)

 	bool isUserStream;  // was the stream opened by the user?

 

-[ContractInvariantMethod]

-void ObjectInvariant(){

-  Contract.Invariant(buf != null);

-  Contract.Invariant(stream != null);}

-    [NotDelayed]

-	public Buffer (Stream/*!*/ s, bool isUserStream) :base() {

+	[ContractInvariantMethod]

+	void ObjectInvariant(){

+		Contract.Invariant(buf != null);

+		Contract.Invariant(stream != null);

+	}

+

+//  [NotDelayed]

+	public Buffer (Stream/*!*/ s, bool isUserStream) : base() {

 	  Contract.Requires(s != null);

 		stream = s; this.isUserStream = isUserStream;

-		

+

 		int fl, bl;

 		if (s.CanSeek) {

 			fl = (int) s.Length;

@@ -51,12 +53,12 @@ void ObjectInvariant(){
 

 		buf = new byte[(bl>0) ? bl : MIN_BUFFER_LENGTH];

 		fileLen = fl;  bufLen = bl;

-		

+

 		if (fileLen > 0) Pos = 0; // setup buffer to position 0 (start)

 		else bufPos = 0; // index 0 is already after the file, thus Pos = 0 is invalid

 		if (bufLen == fileLen && s.CanSeek) Close();

 	}

-	

+

 	protected Buffer(Buffer/*!*/ b) { // called in UTF8Buffer constructor

 	  Contract.Requires(b != null);

 		buf = b.buf;

@@ -73,14 +75,14 @@ void ObjectInvariant(){
 	}

 

 	~Buffer() { Close(); }

-	

+

 	protected void Close() {

 		if (!isUserStream && stream != null) {

 			stream.Close();

 			//stream = null;

 		}

 	}

-	

+

 	public virtual int Read () {

 		if (bufPos < bufLen) {

 			return buf[bufPos++];

@@ -100,7 +102,7 @@ void ObjectInvariant(){
 		Pos = curPos;

 		return ch;

 	}

-	

+

 	public string/*!*/ GetString (int beg, int end) {

 	  Contract.Ensures(Contract.Result<string>() != null);

 		int len = 0;

@@ -139,7 +141,7 @@ void ObjectInvariant(){
 			}

 		}

 	}

-	

+

 	// Read the next chunk of bytes from the stream, increases the buffer

 	// if needed and updates the fields fileLen and bufLen.

 	// Returns the number of bytes read.

@@ -213,19 +215,20 @@ public class Scanner {
 	const int noSym = 103;

 

 

-[ContractInvariantMethod]

-void objectInvariant(){

-  Contract.Invariant(buffer!=null);

-  Contract.Invariant(t != null);

-  Contract.Invariant(start != null);

-  Contract.Invariant(tokens != null);

-  Contract.Invariant(pt != null);

-  Contract.Invariant(tval != null);

-  Contract.Invariant(Filename != null);

-  Contract.Invariant(errorHandler != null);

-}

+	[ContractInvariantMethod]

+	void objectInvariant(){

+		Contract.Invariant(buffer!=null);

+		Contract.Invariant(t != null);

+		Contract.Invariant(start != null);

+		Contract.Invariant(tokens != null);

+		Contract.Invariant(pt != null);

+		Contract.Invariant(tval != null);

+		Contract.Invariant(Filename != null);

+		Contract.Invariant(errorHandler != null);

+	}

+

 	public Buffer/*!*/ buffer; // scanner buffer

-	

+

 	Token/*!*/ t;          // current token

 	int ch;           // current input character

 	int pos;          // byte position of current character

@@ -236,13 +239,13 @@ void objectInvariant(){
 

 	Token/*!*/ tokens;     // list of tokens already peeked (first token is a dummy)

 	Token/*!*/ pt;         // current peek token

-	

+

 	char[]/*!*/ tval = new char[128]; // text of current token

 	int tlen;         // length of current token

-	

+

 	private string/*!*/ Filename;

 	private Errors/*!*/ errorHandler;

-	

+

 	static Scanner() {

 		start = new Hashtable(128);

 		for (int i = 39; i <= 39; ++i) start[i] = 1;

@@ -291,9 +294,9 @@ void objectInvariant(){
 		start[Buffer.EOF] = -1;

 

 	}

-	

-	[NotDelayed]

-	public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) :base(){

+

+//	[NotDelayed]

+	public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) : base() {

 	  Contract.Requires(fileName != null);

 	  Contract.Requires(errorHandler != null);

 		this.errorHandler = errorHandler;

@@ -303,15 +306,14 @@ void objectInvariant(){
 			Stream stream = new FileStream(fileName, FileMode.Open, FileAccess.Read, FileShare.Read);

 			buffer = new Buffer(stream, false);

 			Filename = fileName;

-			

 			Init();

 		} catch (IOException) {

 			throw new FatalError("Cannot open file " + fileName);

 		}

 	}

-	

-	[NotDelayed]

-	public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) :base(){

+

+//	[NotDelayed]

+	public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) : base() {

 	  Contract.Requires(s != null);

 	  Contract.Requires(errorHandler != null);

 	  Contract.Requires(fileName != null);

@@ -320,10 +322,9 @@ void objectInvariant(){
 		buffer = new Buffer(s, true);

 		this.errorHandler = errorHandler;

 		this.Filename = fileName;

-		

 		Init();

 	}

-	

+

 	void Init() {

 		pos = -1; line = 1; col = 0;

 		oldEols = 0;

@@ -344,11 +345,11 @@ void objectInvariant(){
 	Contract.Ensures(Contract.Result<string>() != null);

 	  int p = buffer.Pos;

 	  int ch = buffer.Read();

-      // replace isolated '\r' by '\n' in order to make

+	  // replace isolated '\r' by '\n' in order to make

 	  // eol handling uniform across Windows, Unix and Mac

 	  if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;

 	  while (ch != EOL && ch != Buffer.EOF){

-	    ch = buffer.Read();

+		ch = buffer.Read();

 		// replace isolated '\r' by '\n' in order to make

 		// eol handling uniform across Windows, Unix and Mac

 		if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;

@@ -359,7 +360,7 @@ void objectInvariant(){
 	}

 

 	void NextCh() {

-		if (oldEols > 0) { ch = EOL; oldEols--; } 

+		if (oldEols > 0) { ch = EOL; oldEols--; }

 		else {

 //			pos = buffer.Pos;

 //			ch = buffer.Read(); col++;

@@ -367,9 +368,9 @@ void objectInvariant(){
 //			// eol handling uniform across Windows, Unix and Mac

 //			if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;

 //			if (ch == EOL) { line++; col = 0; }

-			

+

 			while (true) {

-			    pos = buffer.Pos;

+				pos = buffer.Pos;

 				ch = buffer.Read(); col++;

 				// replace isolated '\r' by '\n' in order to make

 				// eol handling uniform across Windows, Unix and Mac

@@ -419,7 +420,7 @@ void objectInvariant(){
 				return;

 			  }

 

-			

+

 		}

 

 	}

@@ -555,10 +556,13 @@ void objectInvariant(){
 		t.pos = pos; t.col = col; t.line = line;

 		t.filename = this.Filename;

 		int state;

-		if (start.ContainsKey(ch)) { state = (int) cce.NonNull( start[ch]); }

+		if (start.ContainsKey(ch)) {

+			Contract.Assert(start[ch] != null);

+			state = (int) start[ch];

+		}

 		else { state = 0; }

 		tlen = 0; AddCh();

-		

+

 		switch (state) {

 			case -1: { t.kind = eofSym; break; } // NextCh already done

 			case 0: {

@@ -765,14 +769,14 @@ void objectInvariant(){
 		t.val = new String(tval, 0, tlen);

 		return t;

 	}

-	

+

 	private void SetScannerBehindT() {

 		buffer.Pos = t.pos;

 		NextCh();

 		line = t.line; col = t.col;

 		for (int i = 0; i < tlen; i++) NextCh();

 	}

-	

+

 	// get the next token (possibly a token already seen during peeking)

 	public Token/*!*/ Scan () {

 	 Contract.Ensures(Contract.Result<Token>() != null);

@@ -793,7 +797,7 @@ void objectInvariant(){
 			}

 			pt = pt.next;

 		} while (pt.kind > maxT); // skip pragmas

-	

+

 		return pt;

 	}

 

diff --git a/Source/DafnyDriver/DafnyDriver.csproj b/Source/DafnyDriver/DafnyDriver.csproj
index 1ec5abb0..d577c048 100644
--- a/Source/DafnyDriver/DafnyDriver.csproj
+++ b/Source/DafnyDriver/DafnyDriver.csproj
@@ -97,6 +97,10 @@
       <SpecificVersion>False</SpecificVersion>

       <HintPath>..\Core\bin\Debug\Core.dll</HintPath>

     </Reference>

+    <Reference Include="ParserHelper, Version=0.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

+      <SpecificVersion>False</SpecificVersion>

+      <HintPath>..\..\Binaries\ParserHelper.dll</HintPath>

+    </Reference>

     <Reference Include="System" />

     <Reference Include="System.Data" />

     <Reference Include="System.Xml" />

diff --git a/Source/Core/ParserHelper.cs b/Source/ParserHelper/ParserHelper.cs
index 465b9245..465b9245 100644
--- a/Source/Core/ParserHelper.cs
+++ b/Source/ParserHelper/ParserHelper.cs
diff --git a/Source/ParserHelper/ParserHelper.csproj b/Source/ParserHelper/ParserHelper.csproj
new file mode 100644
index 00000000..405a3d75
--- /dev/null
+++ b/Source/ParserHelper/ParserHelper.csproj
@@ -0,0 +1,92 @@
+<?xml version="1.0" encoding="utf-8"?>

+<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">

+  <PropertyGroup>

+    <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>

+    <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>

+    <ProductVersion>8.0.30703</ProductVersion>

+    <SchemaVersion>2.0</SchemaVersion>

+    <ProjectGuid>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</ProjectGuid>

+    <OutputType>Library</OutputType>

+    <AppDesignerFolder>Properties</AppDesignerFolder>

+    <RootNamespace>ParserHelper</RootNamespace>

+    <AssemblyName>ParserHelper</AssemblyName>

+    <TargetFrameworkVersion>v3.5</TargetFrameworkVersion>

+    <FileAlignment>512</FileAlignment>

+    <TargetFrameworkProfile />

+    <CodeContractsAssemblyMode>1</CodeContractsAssemblyMode>

+  </PropertyGroup>

+  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">

+    <DebugSymbols>true</DebugSymbols>

+    <DebugType>full</DebugType>

+    <Optimize>false</Optimize>

+    <OutputPath>..\..\Binaries\</OutputPath>

+    <DefineConstants>TRACE;DEBUG</DefineConstants>

+    <ErrorReport>prompt</ErrorReport>

+    <WarningLevel>4</WarningLevel>

+    <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>

+    <CodeContractsRuntimeOnlyPublicSurface>True</CodeContractsRuntimeOnlyPublicSurface>

+    <CodeContractsRuntimeThrowOnFailure>False</CodeContractsRuntimeThrowOnFailure>

+    <CodeContractsRuntimeCallSiteRequires>True</CodeContractsRuntimeCallSiteRequires>

+    <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>

+    <CodeContractsNonNullObligations>True</CodeContractsNonNullObligations>

+    <CodeContractsBoundsObligations>True</CodeContractsBoundsObligations>

+    <CodeContractsArithmeticObligations>True</CodeContractsArithmeticObligations>

+    <CodeContractsContainerAnalysis>True</CodeContractsContainerAnalysis>

+    <CodeContractsRedundantAssumptions>True</CodeContractsRedundantAssumptions>

+    <CodeContractsRunInBackground>True</CodeContractsRunInBackground>

+    <CodeContractsShowSquigglies>True</CodeContractsShowSquigglies>

+    <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>

+    <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>

+    <CodeContractsCustomRewriterAssembly />

+    <CodeContractsCustomRewriterClass />

+    <CodeContractsLibPaths />

+    <CodeContractsExtraRewriteOptions />

+    <CodeContractsExtraAnalysisOptions />

+    <CodeContractsBaseLineFile>..\..\baseline.xml</CodeContractsBaseLineFile>

+    <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>

+    <CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>

+  </PropertyGroup>

+  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">

+    <DebugType>pdbonly</DebugType>

+    <Optimize>true</Optimize>

+    <OutputPath>bin\Release\</OutputPath>

+    <DefineConstants>TRACE</DefineConstants>

+    <ErrorReport>prompt</ErrorReport>

+    <WarningLevel>4</WarningLevel>

+  </PropertyGroup>

+  <PropertyGroup>

+    <SignAssembly>true</SignAssembly>

+  </PropertyGroup>

+  <PropertyGroup>

+    <AssemblyOriginatorKeyFile>..\InterimKey.snk</AssemblyOriginatorKeyFile>

+  </PropertyGroup>

+  <ItemGroup>

+    <Reference Include="Microsoft.Contracts, Version=1.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

+      <SpecificVersion>False</SpecificVersion>

+      <HintPath>..\..\Binaries\Microsoft.Contracts.dll</HintPath>

+    </Reference>

+    <Reference Include="System" />

+    <Reference Include="System.Core" />

+    <Reference Include="System.Xml.Linq" />

+    <Reference Include="System.Data.DataSetExtensions" />

+    <Reference Include="System.Data" />

+    <Reference Include="System.Xml" />

+  </ItemGroup>

+  <ItemGroup>

+    <Compile Include="ParserHelper.cs" />

+  </ItemGroup>

+  <ItemGroup>

+    <ProjectReference Include="..\CodeContractsExtender\CodeContractsExtender.csproj">

+      <Project>{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}</Project>

+      <Name>CodeContractsExtender</Name>

+    </ProjectReference>

+  </ItemGroup>

+  <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />

+  <!-- To modify your build process, add your task inside one of the targets below and uncomment it. 

+       Other similar extension points exist, see Microsoft.Common.targets.

+  <Target Name="BeforeBuild">

+  </Target>

+  <Target Name="AfterBuild">

+  </Target>

+  -->

+</Project>
\ No newline at end of file
diff --git a/Source/Provers/Isabelle/Isabelle.csproj b/Source/Provers/Isabelle/Isabelle.csproj
index b4087878..5279883a 100644
--- a/Source/Provers/Isabelle/Isabelle.csproj
+++ b/Source/Provers/Isabelle/Isabelle.csproj
@@ -124,6 +124,10 @@
       <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>

       <Name>Core</Name>

     </ProjectReference>

+    <ProjectReference Include="..\..\ParserHelper\ParserHelper.csproj">

+      <Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project>

+      <Name>ParserHelper</Name>

+    </ProjectReference>

     <ProjectReference Include="..\..\VCExpr\VCExpr.csproj">

       <Project>{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}</Project>

       <Name>VCExpr</Name>

diff --git a/Source/Provers/Z3/Z3.csproj b/Source/Provers/Z3/Z3.csproj
index 33b8ba7b..e67d7fb2 100644
--- a/Source/Provers/Z3/Z3.csproj
+++ b/Source/Provers/Z3/Z3.csproj
@@ -130,6 +130,10 @@
       <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>

       <Name>Core</Name>

     </ProjectReference>

+    <ProjectReference Include="..\..\ParserHelper\ParserHelper.csproj">

+      <Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project>

+      <Name>ParserHelper</Name>

+    </ProjectReference>

     <ProjectReference Include="..\..\VCExpr\VCExpr.csproj">

       <Project>{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}</Project>

       <Name>VCExpr</Name>

diff --git a/Source/VCExpr/VCExpr.csproj b/Source/VCExpr/VCExpr.csproj
index 116112a0..c712d6a1 100644
--- a/Source/VCExpr/VCExpr.csproj
+++ b/Source/VCExpr/VCExpr.csproj
@@ -135,6 +135,10 @@
       <Project>{B230A69C-C466-4065-B9C1-84D80E76D802}</Project>

       <Name>Core</Name>

     </ProjectReference>

+    <ProjectReference Include="..\ParserHelper\ParserHelper.csproj">

+      <Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project>

+      <Name>ParserHelper</Name>

+    </ProjectReference>

   </ItemGroup>

   <ItemGroup>

     <Folder Include="Properties\" />

diff --git a/Source/VCGeneration/VCGeneration.csproj b/Source/VCGeneration/VCGeneration.csproj
index 9906070a..1697156f 100644
--- a/Source/VCGeneration/VCGeneration.csproj
+++ b/Source/VCGeneration/VCGeneration.csproj
@@ -141,6 +141,10 @@
       <Project>{ACEF88D5-DADD-46DA-BAE1-2144D63F4C83}</Project>

       <Name>Model</Name>

     </ProjectReference>

+    <ProjectReference Include="..\ParserHelper\ParserHelper.csproj">

+      <Project>{FCD3AC7F-9DFD-46C8-AB1E-09F0B0F16DC5}</Project>

+      <Name>ParserHelper</Name>

+    </ProjectReference>

     <ProjectReference Include="..\VCExpr\VCExpr.csproj">

       <Project>{56FFDBCA-7D14-43B8-A6CA-22A20E417EE1}</Project>

       <Name>VCExpr</Name>