Introduce unit tests which use NUnit. NUnit is now a dependency

so developers need to install it via NuGet.

There aren't many tests yet. Just a few for Core and Basetypes but
hopefully more will be added in the future.

More information can be found in Source/UnitTests/README.md

18 files changed, 1172 insertions, 0 deletions

diff --git a/Source/UnitTests/BasetypesTests/BasetypesTests.csproj b/Source/UnitTests/BasetypesTests/BasetypesTests.csproj
new file mode 100644
index 00000000..483c12c7
--- /dev/null
+++ b/Source/UnitTests/BasetypesTests/BasetypesTests.csproj
@@ -0,0 +1,69 @@
+<?xml version="1.0" encoding="utf-8"?>

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

+  <Import Project="$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props" Condition="Exists('$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props')" />

+  <PropertyGroup>

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

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

+    <ProjectGuid>{D00C3F22-1EDA-4781-8F0E-81991E9CB0D9}</ProjectGuid>

+    <OutputType>Library</OutputType>

+    <AppDesignerFolder>Properties</AppDesignerFolder>

+    <RootNamespace>BasetypesTests</RootNamespace>

+    <AssemblyName>BasetypesTests</AssemblyName>

+    <TargetFrameworkVersion>v4.5</TargetFrameworkVersion>

+    <FileAlignment>512</FileAlignment>

+  </PropertyGroup>

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

+    <DebugSymbols>true</DebugSymbols>

+    <DebugType>full</DebugType>

+    <Optimize>false</Optimize>

+    <OutputPath>bin\Debug\</OutputPath>

+    <DefineConstants>DEBUG;TRACE</DefineConstants>

+    <ErrorReport>prompt</ErrorReport>

+    <WarningLevel>4</WarningLevel>

+  </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>

+  <ItemGroup>

+    <Reference Include="nunit.framework">

+      <HintPath>..\..\packages\NUnit.2.6.3\lib\nunit.framework.dll</HintPath>

+    </Reference>

+    <Reference Include="System" />

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

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

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

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

+    <Reference Include="Microsoft.CSharp" />

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

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

+  </ItemGroup>

+  <ItemGroup>

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

+    <Compile Include="Properties\AssemblyInfo.cs" />

+  </ItemGroup>

+  <ItemGroup>

+    <None Include="packages.config" />

+  </ItemGroup>

+  <ItemGroup>

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

+      <Project>{43dfad18-3e35-4558-9be2-caff6b5ba8a0}</Project>

+      <Name>Basetypes</Name>

+    </ProjectReference>

+  </ItemGroup>

+  <ItemGroup>

+    <Service Include="{82A7F48D-3B50-4B1E-B82E-3ADA8210C358}" />

+  </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/UnitTests/BasetypesTests/BigDecTests.cs b/Source/UnitTests/BasetypesTests/BigDecTests.cs
new file mode 100644
index 00000000..cee80216
--- /dev/null
+++ b/Source/UnitTests/BasetypesTests/BigDecTests.cs
@@ -0,0 +1,29 @@
+using Microsoft.Basetypes;
+using NUnit.Framework;
+using System.Numerics;
+
+namespace BasetypesTests
+{
+  [TestFixture()]
+  public class BigDecTests {
+
+    [Test()]
+    public void FromStringNegative() {
+      // This tests for a Bug in Boogie that used to be present where BigDec
+      // would not parse strings with negative numbers correctly
+      //
+      // If this bug is present this test will fail when checking the mantissa
+      var v = BigDec.FromString("-1.5");
+      Assert.AreEqual(-1, v.Exponent);
+      Assert.AreEqual(new BigInteger(-15.0), v.Mantissa);
+    }
+
+    [Test()]
+    public void FromStringPositive() {
+      var v = BigDec.FromString("1.5");
+      Assert.AreEqual(-1, v.Exponent);
+      Assert.AreEqual(new BigInteger(15.0), v.Mantissa);
+    }
+  }
+}
+
diff --git a/Source/UnitTests/BasetypesTests/Properties/AssemblyInfo.cs b/Source/UnitTests/BasetypesTests/Properties/AssemblyInfo.cs
new file mode 100644
index 00000000..4ef7c05c
--- /dev/null
+++ b/Source/UnitTests/BasetypesTests/Properties/AssemblyInfo.cs
@@ -0,0 +1,36 @@
+using System.Reflection;

+using System.Runtime.CompilerServices;

+using System.Runtime.InteropServices;

+

+// General Information about an assembly is controlled through the following 

+// set of attributes. Change these attribute values to modify the information

+// associated with an assembly.

+[assembly: AssemblyTitle("BasetypesTests")]

+[assembly: AssemblyDescription("")]

+[assembly: AssemblyConfiguration("")]

+[assembly: AssemblyCompany("")]

+[assembly: AssemblyProduct("BasetypesTests")]

+[assembly: AssemblyCopyright("Copyright ©  2014")]

+[assembly: AssemblyTrademark("")]

+[assembly: AssemblyCulture("")]

+

+// Setting ComVisible to false makes the types in this assembly not visible 

+// to COM components.  If you need to access a type in this assembly from 

+// COM, set the ComVisible attribute to true on that type.

+[assembly: ComVisible(false)]

+

+// The following GUID is for the ID of the typelib if this project is exposed to COM

+[assembly: Guid("0cca79cc-3251-46d9-87c1-32bc782d9fdd")]

+

+// Version information for an assembly consists of the following four values:

+//

+//      Major Version

+//      Minor Version 

+//      Build Number

+//      Revision

+//

+// You can specify all the values or you can default the Build and Revision Numbers 

+// by using the '*' as shown below:

+// [assembly: AssemblyVersion("1.0.*")]

+[assembly: AssemblyVersion("1.0.0.0")]

+[assembly: AssemblyFileVersion("1.0.0.0")]

diff --git a/Source/UnitTests/BasetypesTests/packages.config b/Source/UnitTests/BasetypesTests/packages.config
new file mode 100644
index 00000000..d4e241a2
--- /dev/null
+++ b/Source/UnitTests/BasetypesTests/packages.config
@@ -0,0 +1,4 @@
+<?xml version="1.0" encoding="utf-8"?>

+<packages>

+  <package id="NUnit" version="2.6.3" targetFramework="net45" />

+</packages>
\ No newline at end of file
diff --git a/Source/UnitTests/CoreTests/AbsyMetadata.cs b/Source/UnitTests/CoreTests/AbsyMetadata.cs
new file mode 100644
index 00000000..156f38b5
--- /dev/null
+++ b/Source/UnitTests/CoreTests/AbsyMetadata.cs
@@ -0,0 +1,101 @@
+using Microsoft.Boogie;
+using NUnit.Framework;
+using System;
+
+namespace CoreTests
+{
+  [TestFixture ()]
+  public class AbsyMetadata {
+    private Absy GetAbsy() {
+      // The choice of Absy type here is arbitary
+      return new AssertCmd(Token.NoToken, Expr.True);
+    }
+
+    [Test(), ExpectedException(typeof(ArgumentOutOfRangeException))]
+    public void NoMetadata() {
+      var absy = GetAbsy();
+
+      Assert.AreEqual(0, absy.NumberedMetaDataCount);
+
+      string willFail = absy.GetMetadata<string>(0);
+      // use willFail in someway so the result is live
+      Assert.IsNotNullOrEmpty(willFail);
+    }
+
+    [Test(), ExpectedException(typeof(ArgumentOutOfRangeException))]
+    public void InvalidIndex() {
+      var absy = GetAbsy();
+
+      Assert.AreEqual(0, absy.NumberedMetaDataCount);
+      absy.SetMetadata(0, "hello");
+
+      string willFail = absy.GetMetadata<string>(1);
+      // use willFail in someway so the result is live
+      Assert.IsNotNullOrEmpty(willFail);
+    }
+
+    [Test()]
+    public void SimpleMetadata() {
+      var absy = GetAbsy();
+      Assert.AreEqual(0, absy.NumberedMetaDataCount);
+
+      var string1 = "hello";
+      var string2 = "hello2";
+      absy.SetMetadata(0, string1);
+      Assert.AreEqual(1, absy.NumberedMetaDataCount);
+      absy.SetMetadata(1, string2);
+      Assert.AreEqual(2, absy.NumberedMetaDataCount);
+
+      Assert.AreSame(string1, absy.GetMetadata<string>(0));
+      Assert.AreSame(string2, absy.GetMetadata<string>(1));
+
+      // Now try iterating over the metadata
+      int count = 0;
+      foreach (var o in absy.NumberedMetadata) {
+          Assert.AreEqual(count, o.Key);
+          Assert.IsNotNull(o.Value);
+          ++count;
+      }
+      Assert.AreEqual(2, count);
+    }
+
+    [Test(), ExpectedException(typeof(InvalidCastException))]
+    public void IncorrectType() {
+      var absy = GetAbsy();
+      Assert.AreEqual(0, absy.NumberedMetaDataCount);
+
+      var string0 = "hello world";
+      absy.SetMetadata(0, string0);
+
+      // Now try retrive wrong type
+      int wrongType = absy.GetMetadata<int>(0);
+      // use "wrongType" is someway so the variable is live
+      Assert.AreEqual(0, wrongType);
+    }
+
+    [Test()]
+    public void NullPadding() {
+      var absy = GetAbsy();
+      Assert.AreEqual(0, absy.NumberedMetaDataCount);
+
+      string foo = "foo";
+      absy.SetMetadata<string>(10, foo);
+      Assert.AreEqual(11, absy.NumberedMetaDataCount);
+
+      // Should nulls be made accessible? Right now its impossible to access
+      // them as we always throw an exception if the stored item is null
+      for (int i = 0; i <= 9 ; ++i) {
+        try {
+          absy.GetMetadata<String>(i);
+          Assert.Fail("Accesing unset metadata should of failed");
+        }
+        catch (InvalidCastException) {
+        }
+      }
+
+
+      Assert.AreSame(foo, absy.GetMetadata<String>(10));
+    }
+  }
+}
+    
diff --git a/Source/UnitTests/CoreTests/CoreTests.csproj b/Source/UnitTests/CoreTests/CoreTests.csproj
new file mode 100644
index 00000000..1bad6134
--- /dev/null
+++ b/Source/UnitTests/CoreTests/CoreTests.csproj
@@ -0,0 +1,82 @@
+<?xml version="1.0" encoding="utf-8"?>

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

+  <Import Project="$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props" Condition="Exists('$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props')" />

+  <PropertyGroup>

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

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

+    <ProjectGuid>{961B3BCA-2067-43B2-8E43-23C4293F21B9}</ProjectGuid>

+    <OutputType>Library</OutputType>

+    <AppDesignerFolder>Properties</AppDesignerFolder>

+    <RootNamespace>CoreTests</RootNamespace>

+    <AssemblyName>CoreTests</AssemblyName>

+    <TargetFrameworkVersion>v4.5</TargetFrameworkVersion>

+    <FileAlignment>512</FileAlignment>

+  </PropertyGroup>

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

+    <DebugSymbols>true</DebugSymbols>

+    <DebugType>full</DebugType>

+    <Optimize>false</Optimize>

+    <OutputPath>bin\Debug\</OutputPath>

+    <DefineConstants>DEBUG;TRACE</DefineConstants>

+    <ErrorReport>prompt</ErrorReport>

+    <WarningLevel>4</WarningLevel>

+  </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>

+  <ItemGroup>

+    <Reference Include="nunit.framework">

+      <HintPath>..\..\packages\NUnit.2.6.3\lib\nunit.framework.dll</HintPath>

+    </Reference>

+    <Reference Include="System" />

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

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

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

+    <Reference Include="Microsoft.CSharp" />

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

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

+  </ItemGroup>

+  <ItemGroup>

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

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

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

+    <Compile Include="Properties\AssemblyInfo.cs" />

+  </ItemGroup>

+  <ItemGroup>

+    <None Include="packages.config" />

+  </ItemGroup>

+  <ItemGroup>

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

+      <Project>{43dfad18-3e35-4558-9be2-caff6b5ba8a0}</Project>

+      <Name>Basetypes</Name>

+    </ProjectReference>

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

+      <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="..\TestUtil\TestUtil.csproj">

+      <Project>{59118e35-4236-495e-af6e-0d641302ed2c}</Project>

+      <Name>TestUtil</Name>

+    </ProjectReference>

+  </ItemGroup>

+  <ItemGroup>

+    <Service Include="{82A7F48D-3B50-4B1E-B82E-3ADA8210C358}" />

+  </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/UnitTests/CoreTests/Duplicator.cs b/Source/UnitTests/CoreTests/Duplicator.cs
new file mode 100644
index 00000000..978a041b
--- /dev/null
+++ b/Source/UnitTests/CoreTests/Duplicator.cs
@@ -0,0 +1,258 @@
+using Microsoft.Boogie.TestUtil;
+using Microsoft.Boogie;
+using Microsoft.Basetypes;
+using NUnit.Framework;
+using System;
+using System.Linq;
+
+
+namespace CoreTests
+{
+  [TestFixture ()]
+  public class DuplicatorTests : BoogieTestBase, IErrorSink {
+    Duplicator d;
+
+    public void Error(IToken tok, string msg) {
+      Assert.Fail(msg);
+    }
+
+    [SetUp]
+    public void Init() {
+      d = new Duplicator();
+    }
+
+    [Test()]
+    public void BVConcatExpr() {
+      var bv1_8 = new LiteralExpr(Token.NoToken, BigNum.FromInt(1), 8);
+      var bv2_8 = new LiteralExpr(Token.NoToken, BigNum.FromInt(2), 8);
+      var A = new BvConcatExpr(Token.NoToken, bv1_8, bv2_8);
+      var B = d.Visit(A);
+
+      // The duplicator should ensure we get new BVConcatExprs

+      Assert.AreNotSame(A, B);
+    }
+
+    [Test()]
+    public void BvExtractExpr() {
+      var bv2_8 = new LiteralExpr(Token.NoToken, BigNum.FromInt(2), 8);
+      var A = new BvExtractExpr(Token.NoToken, bv2_8, 6,0);
+      var B = d.Visit(A);
+
+      // The duplicator should ensure we get new BVExtractExprs

+      Assert.AreNotSame(A, B);
+    }
+
+    [Test()]
+    public void NaryExpr() {
+      var bv1_8 = new LiteralExpr(Token.NoToken, BigNum.FromInt(1), 8);
+      var bv2_8 = new LiteralExpr(Token.NoToken, BigNum.FromInt(2), 8);
+      var A = NAryExpr.Eq (bv1_8, bv2_8);
+      var B = d.Visit(A);

+

+      Assert.AreNotSame(A, B);
+    }
+
+    [Test()]
+    public void WholeProgram() {
+      var p = new Program();
+      var t = new TypedIdent(Token.NoToken, "foo", Microsoft.Boogie.Type.Bool);
+      var gv = new GlobalVariable(Token.NoToken, t);
+      p.AddTopLevelDeclaration(gv);
+      string metaDataString = "This is a test";
+      p.SetMetadata(0, metaDataString);
+
+      // Now try to clone
+      var p2 = (Program) d.Visit(p);
+
+      // Check global is a copy
+      int counter = 0;
+      GlobalVariable gv2 = null;
+      foreach (var g in p2.TopLevelDeclarations)
+      {
+        ++counter;
+        Assert.IsInstanceOf<GlobalVariable>(g);
+        gv2 = g as GlobalVariable;
+      }
+      Assert.AreEqual(1, counter);
+      Assert.AreNotSame(gv, gv2);
+      Assert.AreEqual(metaDataString, p2.GetMetadata<string>(0));
+
+
+      // Check Top level declarations list is duplicated properly
+      var t2 = new TypedIdent(Token.NoToken, "bar", Microsoft.Boogie.Type.Bool);
+      var gv3 = new GlobalVariable(Token.NoToken, t2);
+      p2.AddTopLevelDeclaration(gv3);
+
+      counter = 0;
+      foreach (var g in p2.TopLevelDeclarations) {
+        ++counter;
+        Assert.IsInstanceOf<GlobalVariable>(g);
+      }
+      Assert.AreEqual(2, counter);
+
+      // The original program should still only have one global variable
+      counter = 0;
+      foreach (var g in p.TopLevelDeclarations) {
+        ++counter;
+        Assert.IsInstanceOf<GlobalVariable>(g);
+        Assert.AreSame(g, gv);
+      }
+
+      Assert.AreEqual(1, counter);
+
+      // Change Metadata in p2, this shouldn't affect p
+      string newMetaDataString = "Another test";
+      p2.SetMetadata(0, newMetaDataString);
+
+      Assert.AreNotEqual(p2.GetMetadata<string>(0), p.GetMetadata<string>(0));
+    }
+
+    [Test()]
+    public void GotoTargets() {
+      Program p = TestUtil.ProgramLoader.LoadProgramFrom(@"
+        procedure main()
+        {
+            entry:
+                assume true;
+                goto thing1, thing2;
+
+            thing1:
+                assume true;
+                assume true;
+                goto entry, thing1;
+
+            thing2:
+                assume true;
+                assume true;
+                return;
+        }
+      ");
+
+      var main = p.TopLevelDeclarations.OfType<Implementation>().Where(x => x.Name == "main").First();
+
+      // Access blocks via their labels of gotocmds
+      var oldEntryBlock =  ( main.Blocks[1].TransferCmd as GotoCmd ).labelTargets[0];
+      Assert.AreEqual("entry", oldEntryBlock.Label);
+
+      var oldThing1Block = ( main.Blocks[1].TransferCmd as GotoCmd ).labelTargets[1];
+      Assert.AreEqual("thing1", oldThing1Block.Label);
+
+      var oldThing2Block = ( main.Blocks[0].TransferCmd as GotoCmd ).labelTargets[1];
+      Assert.AreEqual("thing2", oldThing2Block.Label);
+
+      // Now duplicate
+      var newProgram = (Program) d.Visit(p);
+
+      // First lets check blocks have been duplicated
+      var newMain= newProgram.TopLevelDeclarations.OfType<Implementation>().Where(x => x.Name == "main").First();
+      var newEntryBlock = newMain.Blocks[0];
+      Assert.AreEqual("entry", newEntryBlock.Label);
+      Assert.AreNotSame(newEntryBlock, oldEntryBlock);
+
+      var newThing1Block = newMain.Blocks[1];
+      Assert.AreEqual("thing1", newThing1Block.Label);
+      Assert.AreNotSame(newThing1Block, oldThing1Block);
+
+      var newThing2Block = newMain.Blocks[2];
+      Assert.AreEqual("thing2", newThing2Block.Label);
+      Assert.AreNotSame(newThing2Block, oldThing2Block);
+
+      // Now let's examine the gotos and make sure they point to the duplicated blocks.
+      var newEntryGotoCmd = newEntryBlock.TransferCmd as GotoCmd;
+      var newthing1GotoCmd = newThing1Block.TransferCmd as GotoCmd;
+
+      Assert.AreNotSame(newEntryGotoCmd.labelTargets[0], oldThing1Block);
+      Assert.AreSame(newEntryGotoCmd.labelTargets[0], newThing1Block);
+      Assert.AreNotSame(newEntryGotoCmd.labelTargets[1], oldThing2Block);
+      Assert.AreSame(newEntryGotoCmd.labelTargets[1], newThing2Block);
+
+      Assert.AreNotSame(newthing1GotoCmd.labelTargets[0], oldEntryBlock);
+      Assert.AreSame(newthing1GotoCmd.labelTargets[0], newEntryBlock);
+      Assert.AreNotSame(newthing1GotoCmd.labelTargets[1], oldThing1Block);
+      Assert.AreSame(newthing1GotoCmd.labelTargets[1], newThing1Block);
+
+    }
+
+    [Test()]
+    public void ImplementationProcedureResolving() {
+      Program p = TestUtil.ProgramLoader.LoadProgramFrom(@"
+        procedure main(a:int) returns (r:int);
+        requires a > 0;
+        ensures  r > a;
+
+        implementation main(a:int) returns (r:int)
+        {
+            r:= a + 1;
+        }
+      ");
+
+      // Check resolved
+      var oldMainImpl = p.TopLevelDeclarations.OfType<Implementation>().Where(i => i.Name == "main").First();
+      var oldMainProc = p.TopLevelDeclarations.OfType<Procedure>().Where(i => i.Name == "main").First();
+      Assert.AreSame(oldMainImpl.Proc, oldMainProc);
+
+      // Now duplicate the program
+      var newProgram = (Program) d.Visit(p);
+
+      // Resolving doesn't seem to fix this.
+      var rc = new ResolutionContext(this);
+      newProgram.Resolve(rc);
+
+      // Check resolved
+      var newMainImpl = newProgram.TopLevelDeclarations.OfType<Implementation>().Where(i => i.Name == "main").First();
+      var newMainProc = newProgram.TopLevelDeclarations.OfType<Procedure>().Where(i => i.Name == "main").First();
+      Assert.AreSame(newMainImpl.Proc, newMainProc);
+    }
+
+    [Test()]
+    public void CallCmdResolving() {
+      Program p = TestUtil.ProgramLoader.LoadProgramFrom(@"
+        procedure main()
+        {
+            var x:int;
+            call x := foo();
+            call x := bar();
+        }
+
+        procedure foo() returns(r:int)
+        {
+            r := 0;
+        }
+
+        procedure bar() returns(r:int);
+        ensures r == 0;
+      ");
+
+    // Get hold of the procedures that will be used with the CallCmd
+    var oldFoo = p.TopLevelDeclarations.OfType<Procedure>().Where(i => i.Name == "foo").First();
+    var oldBar = p.TopLevelDeclarations.OfType<Procedure>().Where(i => i.Name == "bar").First();
+
+    // Get the CallCmds to foo and bar
+    var oldCmdsInMain = p.TopLevelDeclarations.OfType<Implementation>().Where(i => i.Name == "main").SelectMany(i => i.Blocks).SelectMany(b => b.Cmds);
+    var oldCallToFoo = oldCmdsInMain.OfType<CallCmd>().Where(c => c.callee == "foo").First();
+    var oldCallToBar = oldCmdsInMain.OfType<CallCmd>().Where(c => c.callee == "bar").First();
+
+    // Check the Calls
+    Assert.AreSame(oldCallToFoo.Proc, oldFoo);
+    Assert.AreSame(oldCallToBar.Proc, oldBar);
+
+    // Now duplicate the program and check that the calls are resolved correctly
+    var newProgram = (Program) d.Visit(p);
+
+    var foo = newProgram.TopLevelDeclarations.OfType<Procedure>().Where(i => i.Name == "foo").First();
+    var bar = newProgram.TopLevelDeclarations.OfType<Procedure>().Where(i => i.Name == "bar").First();
+
+    // Get the call to Foo
+    var cmdsInMain = newProgram.TopLevelDeclarations.OfType<Implementation>().Where(i => i.Name == "main").SelectMany(i => i.Blocks).SelectMany(b => b.Cmds);
+    var callToFoo = cmdsInMain.OfType<CallCmd>().Where(c => c.callee == "foo").First();
+    var callToBar = cmdsInMain.OfType<CallCmd>().Where(c => c.callee == "bar").First();
+
+    // Check the Calls
+    Assert.AreNotSame(callToFoo.Proc, oldFoo);
+    Assert.AreSame(callToFoo.Proc, foo);
+    Assert.AreNotSame(callToBar.Proc, oldBar);
+    Assert.AreSame(callToBar.Proc, bar);
+    }
+  }
+}
+
diff --git a/Source/UnitTests/CoreTests/ExprEquality.cs b/Source/UnitTests/CoreTests/ExprEquality.cs
new file mode 100644
index 00000000..6bc049f5
--- /dev/null
+++ b/Source/UnitTests/CoreTests/ExprEquality.cs
@@ -0,0 +1,179 @@
+using Microsoft.Boogie;
+using Microsoft.Basetypes;
+using NUnit.Framework;
+using System.Collections.Generic;
+using System;
+
+namespace CoreTests
+{
+  [TestFixture()]
+  public class ExprEquality {
+
+    [Test()]
+    public void LiteralBool() {
+      var constant = new LiteralExpr(Token.NoToken, false);
+      var constant2 = new LiteralExpr(Token.NoToken, false);
+
+      Assert.AreNotSame(constant, constant2); // These are different references
+
+      Assert.IsTrue(constant.Equals(constant2)); // These are "structurally equal"
+      Assert.AreEqual(constant.GetHashCode(), constant2.GetHashCode()); // If the .Equals() is true then hash codes must be the same
+    }
+
+    [Test()]
+    public void LiteralBV() {
+      var constant = new LiteralExpr(Token.NoToken, BigNum.FromInt(5), 8); // 5bv8;
+      var constant2 = new LiteralExpr(Token.NoToken, BigNum.FromInt(5), 8); // 5bv8;
+
+      Assert.AreNotSame(constant, constant2); // These are different references
+
+      Assert.IsTrue(constant.Equals(constant2)); // These are "structurally equal"
+      Assert.AreEqual(constant.GetHashCode(), constant2.GetHashCode()); // If the .Equals() is true then hash codes must be the same
+    }
+
+    [Test()]
+    public void LiteralInt() {
+      var constant = new LiteralExpr(Token.NoToken, BigNum.FromInt(18)); // Integer
+      var constant2 = new LiteralExpr(Token.NoToken, BigNum.FromInt(18)); // Integer
+
+      Assert.AreNotSame(constant, constant2); // These are different references
+
+      Assert.IsTrue(constant.Equals(constant2)); // These are "structurally equal"
+      Assert.AreEqual(constant.GetHashCode(), constant2.GetHashCode()); // If the .Equals() is true then hash codes must be the same
+    }
+
+    [Test()]
+    public void LiteralReal() {
+      var constant = new LiteralExpr(Token.NoToken, BigDec.FromString("11.7")); // Real
+      var constant2 = new LiteralExpr(Token.NoToken, BigDec.FromString("11.7")); // Real
+
+      Assert.AreNotSame(constant, constant2); // These are different references
+
+      Assert.IsTrue(constant.Equals(constant2)); // These are "structurally equal"
+      Assert.AreEqual(constant.GetHashCode(), constant2.GetHashCode()); // If the .Equals() is true then hash codes must be the same
+    }
+
+    [Test()]
+    public void SimpleAdd() {
+      var constant = new LiteralExpr(Token.NoToken, BigNum.FromInt(18)); // Integer
+      var constant2 = new LiteralExpr(Token.NoToken, BigNum.FromInt(19)); // Integer
+      var add = Expr.Add(constant, constant2);
+
+      var add2 = Expr.Add(constant, constant2);
+
+      Assert.AreNotSame(constant, constant2); // These are different references
+      Assert.AreNotSame(add, add2); // These are different references
+
+      Assert.IsTrue(add.Equals(add2)); // These are "structurally equal"
+      Assert.AreEqual(add.GetHashCode(), add2.GetHashCode()); // If the .Equals() is true then hash codes must be the same
+    }
+
+    [Test()]
+    public void SimpleIdentifierExprs() {
+      var variable = new GlobalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "foo", Microsoft.Boogie.Type.GetBvType(8)));
+      var idVar = new IdentifierExpr(Token.NoToken, variable);
+      var idVar2 = new IdentifierExpr(Token.NoToken, variable);
+
+      Assert.AreNotSame(idVar, idVar2); // These are different references
+
+      Assert.IsTrue(idVar.Equals(idVar2)); // These are "structurally equal"
+      Assert.AreEqual(idVar.GetHashCode(), idVar2.GetHashCode()); // If the .Equals() is true then hash codes must be the same
+    }
+
+    [Test()]
+    public void SimpleIdentifierVariables() {
+      var variable = new GlobalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "foo", Microsoft.Boogie.Type.GetBvType(8)));
+      var variable2 = new GlobalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "foo", Microsoft.Boogie.Type.GetBvType(8)));
+      var idVar = new IdentifierExpr(Token.NoToken, variable);
+      var idVar2 = new IdentifierExpr(Token.NoToken, variable2);
+
+      Assert.AreNotSame(idVar, idVar2); // These are different references
+      // These are not "structurally equal" because the Variable references are different (even though they have the same name and type)
+      Assert.IsFalse(idVar.Equals(idVar2));
+    }
+
+    [Test()]
+    public void SimpleBVConcat() {
+      var variable = new GlobalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "foo", Microsoft.Boogie.Type.GetBvType(8)));
+      var id = new IdentifierExpr(Token.NoToken, variable);
+      var constant = new LiteralExpr(Token.NoToken, BigNum.FromInt(5), 8); // 5bv8;
+      var concat = new BvConcatExpr(Token.NoToken, id, constant);
+
+      // Don't trust the Boogie duplicator here. Do it ourselves
+      var constant2 = new LiteralExpr(Token.NoToken, BigNum.FromInt(5), 8); // 5bv8;
+      // We don't duplicate the variable because that is not an Expr and we require reference equality.
+      var id2 = new IdentifierExpr(Token.NoToken, variable);
+      var concat2 = new BvConcatExpr(Token.NoToken, id2, constant2);
+
+      Assert.AreNotSame(concat, concat2); // These are different references
+
+      Assert.IsTrue(concat.Equals(concat2)); // These are "structurally equal"
+      Assert.AreEqual(concat.GetHashCode(), concat2.GetHashCode()); // If the .Equals() is true then hash codes must be the same
+    }
+
+    [Test()]
+    public void SimpleBVExtract() {
+      var variable = new GlobalVariable(Token.NoToken, new TypedIdent(Token.NoToken, "foo", Microsoft.Boogie.Type.GetBvType(8)));
+      var id = new IdentifierExpr(Token.NoToken, variable);
+
+      var extract = new BvExtractExpr(Token.NoToken, id, 5, 0); // 4-bits
+
+      var id2 = new IdentifierExpr(Token.NoToken, variable);
+      var extract2 = new BvExtractExpr(Token.NoToken, id2, 5, 0);
+
+      Assert.AreNotSame(extract, extract2);
+
+      Assert.IsTrue(extract.Equals(extract2));
+      Assert.AreEqual(extract.GetHashCode(), extract2.GetHashCode()); // If the .Equals() is true then hash codes must be the same
+    }
+
+    [Test()]
+    public void SimpleForAll() {
+      var boundVar = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken,"foo",Microsoft.Boogie.Type.Bool));
+      var id = new IdentifierExpr(Token.NoToken, boundVar);
+      var forall = new ForallExpr(Token.NoToken, new List<Variable>() { boundVar }, id);
+
+      var id2 = new IdentifierExpr(Token.NoToken, boundVar);
+      var forall2 = new ForallExpr(Token.NoToken, new List<Variable>() { boundVar }, id2);
+
+      Assert.AreNotSame(forall, forall2); // These are different references
+
+      Assert.IsTrue(forall.Equals(forall2)); // These are "structurally equal"
+      Assert.AreEqual(forall.GetHashCode(), forall2.GetHashCode()); // If the .Equals() is true then hash codes must be the same
+    }
+
+
+    [Test()]
+    public void SimpleExists() {
+      var boundVar = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken,"foo",Microsoft.Boogie.Type.Bool));
+      var id = new IdentifierExpr(Token.NoToken, boundVar);
+      var exists = new ExistsExpr(Token.NoToken, new List<Variable>() { boundVar }, id);
+
+      var id2 = new IdentifierExpr(Token.NoToken, boundVar);
+      var exists2 = new ExistsExpr(Token.NoToken, new List<Variable>() { boundVar }, id2);
+
+      Assert.AreNotSame(exists, exists2); // These are different references
+
+      Assert.IsTrue(exists.Equals(exists2)); // These are "structurally equal"
+      Assert.AreEqual(exists.GetHashCode(), exists2.GetHashCode()); // If the .Equals() is true then hash codes must be the same
+    }
+
+    [Test()]
+    public void SimpleLambda() {
+      var boundVar = new BoundVariable(Token.NoToken, new TypedIdent(Token.NoToken,"foo",Microsoft.Boogie.Type.Bool));
+      var id = new IdentifierExpr(Token.NoToken, boundVar);
+
+      // This is basically an Identity Map
+      var lambdaExpr = new LambdaExpr(Token.NoToken, new List<TypeVariable>() , new List<Variable>() { boundVar }, null, id);
+
+      var id2 = new IdentifierExpr(Token.NoToken, boundVar);
+      var lambdaExpr2 = new LambdaExpr(Token.NoToken, new List<TypeVariable>() , new List<Variable>() { boundVar }, null, id2);
+
+      Assert.AreNotSame(lambdaExpr, lambdaExpr2); // These are different references
+
+      Assert.IsTrue(lambdaExpr.Equals(lambdaExpr2)); // These are "structurally equal"
+      Assert.AreEqual(lambdaExpr.GetHashCode(), lambdaExpr2.GetHashCode()); // If the .Equals() is true then hash codes must be the same
+    }
+  }
+}
+
diff --git a/Source/UnitTests/CoreTests/Properties/AssemblyInfo.cs b/Source/UnitTests/CoreTests/Properties/AssemblyInfo.cs
new file mode 100644
index 00000000..fb965517
--- /dev/null
+++ b/Source/UnitTests/CoreTests/Properties/AssemblyInfo.cs
@@ -0,0 +1,36 @@
+using System.Reflection;

+using System.Runtime.CompilerServices;

+using System.Runtime.InteropServices;

+

+// General Information about an assembly is controlled through the following 

+// set of attributes. Change these attribute values to modify the information

+// associated with an assembly.

+[assembly: AssemblyTitle("CoreTests")]

+[assembly: AssemblyDescription("")]

+[assembly: AssemblyConfiguration("")]

+[assembly: AssemblyCompany("")]

+[assembly: AssemblyProduct("CoreTests")]

+[assembly: AssemblyCopyright("Copyright ©  2014")]

+[assembly: AssemblyTrademark("")]

+[assembly: AssemblyCulture("")]

+

+// Setting ComVisible to false makes the types in this assembly not visible 

+// to COM components.  If you need to access a type in this assembly from 

+// COM, set the ComVisible attribute to true on that type.

+[assembly: ComVisible(false)]

+

+// The following GUID is for the ID of the typelib if this project is exposed to COM

+[assembly: Guid("5c6f8617-e212-4ab7-bce6-5b1a930fa2b8")]

+

+// Version information for an assembly consists of the following four values:

+//

+//      Major Version

+//      Minor Version 

+//      Build Number

+//      Revision

+//

+// You can specify all the values or you can default the Build and Revision Numbers 

+// by using the '*' as shown below:

+// [assembly: AssemblyVersion("1.0.*")]

+[assembly: AssemblyVersion("1.0.0.0")]

+[assembly: AssemblyFileVersion("1.0.0.0")]

diff --git a/Source/UnitTests/CoreTests/packages.config b/Source/UnitTests/CoreTests/packages.config
new file mode 100644
index 00000000..d4e241a2
--- /dev/null
+++ b/Source/UnitTests/CoreTests/packages.config
@@ -0,0 +1,4 @@
+<?xml version="1.0" encoding="utf-8"?>

+<packages>

+  <package id="NUnit" version="2.6.3" targetFramework="net45" />

+</packages>
\ No newline at end of file
diff --git a/Source/UnitTests/README.md b/Source/UnitTests/README.md
new file mode 100644
index 00000000..5e70bc18
--- /dev/null
+++ b/Source/UnitTests/README.md
@@ -0,0 +1,55 @@
+Unit testing infrastructure
+===========================
+
+Boogie uses [NUnit](http://www.nunit.org/) unit test framework.
+We currently use NUnit 2.6.3, which was the latest stable
+version available at the time of writing.
+
+
+Installing NUnit
+================
+
+NUnit should be installed via [NuGet](https://www.nuget.org/) package manager.
+
+The NuGet client is available as
+
+* An extension to Visual Studio
+* An add-in in Monodevelop
+* A command line utility from the NuGet website
+
+Note Mono ships with an old version of NUnit (2.4.8) which will cause
+compilation issues. To fix this you must install NUnit via NuGet.
+
+
+Running the tests
+=================
+
+Command line
+------------
+
+The ``run-unittests.py`` python script in the root directory of the project can be used to run the unit tests on the command line. This script is a simple wrapper for ``nunit-console.exe``.
+
+```
+$ python run-unittests.py Release
+```
+
+Run the following to see all the available options
+
+```
+$ python run-unittests.py --help
+```
+
+Monodevelop
+-----------
+
+Monodevelop has built in support for running NUnit tests. Goto the "Unit Tests"
+panel and click "Run All".
+
+Visual Studio
+-------------
+
+Visual studio needs the "NUnit Test Adapter for VS2012 and VS2013" add-in to be installed (Tools > Extensions and Updates). Once that is installed you can run unit tests by going 
+
+1. Going to the Test Explorer (TEST > Windows > Test Explorer)
+2. Clicking on "Run All" in the Test Explorer.
+
diff --git a/Source/UnitTests/TestUtil/AssertionTextWriterTraceListener.cs b/Source/UnitTests/TestUtil/AssertionTextWriterTraceListener.cs
new file mode 100644
index 00000000..961ed0df
--- /dev/null
+++ b/Source/UnitTests/TestUtil/AssertionTextWriterTraceListener.cs
@@ -0,0 +1,27 @@
+using NUnit.Framework;
+using System;
+using System.Diagnostics;
+
+namespace Microsoft.Boogie
+{
+  namespace TestUtil
+  {
+
+    public class AssertionTextWriterTraceListener : TextWriterTraceListener {
+      public AssertionTextWriterTraceListener(System.IO.Stream stream) : base(stream) { }
+
+      public AssertionTextWriterTraceListener(System.IO.TextWriter writer) : base(writer) { }
+
+      public override void Fail(string message) {
+        base.Fail(message);
+        Assert.Fail(message);
+      }
+
+      public override void Fail(string message, string detailMessage) {
+        base.Fail(message, detailMessage);
+        Assert.Fail(message + " : " + detailMessage);
+      }
+    }
+  }
+}
+
diff --git a/Source/UnitTests/TestUtil/BoogieTestBase.cs b/Source/UnitTests/TestUtil/BoogieTestBase.cs
new file mode 100644
index 00000000..2bac71a4
--- /dev/null
+++ b/Source/UnitTests/TestUtil/BoogieTestBase.cs
@@ -0,0 +1,24 @@
+using NUnit.Framework;
+using System;
+using System.Diagnostics;
+using Microsoft.Boogie;
+
+namespace Microsoft.Boogie
+{
+  namespace TestUtil
+  {
+    public class BoogieTestBase {
+
+      public BoogieTestBase() {
+        // Debug log output goes to standard error.
+        // Failing System.Diagnostics failures trigger NUnit assertion failures
+        Debug.Listeners.Add(new AssertionTextWriterTraceListener(Console.Error));
+
+        // FIXME: THIS IS A HACK. Boogie's methods
+        // depend on its command line parser being set!
+        CommandLineOptions.Install(new Microsoft.Boogie.CommandLineOptions());
+      }
+    }
+  }
+}
+
diff --git a/Source/UnitTests/TestUtil/ProgramLoader.cs b/Source/UnitTests/TestUtil/ProgramLoader.cs
new file mode 100644
index 00000000..bc5f647a
--- /dev/null
+++ b/Source/UnitTests/TestUtil/ProgramLoader.cs
@@ -0,0 +1,33 @@
+using NUnit.Framework;
+using System;
+using Microsoft.Boogie;
+
+namespace TestUtil
+{
+	public class ProgramLoader
+	{
+		public static Program LoadProgramFrom(string programText, string fileName="file.bpl")
+		{
+			Assert.IsNotNullOrEmpty (programText);
+			Assert.IsNotNullOrEmpty (fileName);
+
+
+			int errors = 0;
+			Program p = null;
+			errors = Parser.Parse(programText, fileName, out p, /*useBaseName=*/false);
+			Assert.AreEqual(0, errors);
+			Assert.IsNotNull(p);
+
+			// Resolve
+			errors = p.Resolve();
+			Assert.AreEqual(0, errors);
+
+			// Type check
+			errors = p.Typecheck();
+			Assert.AreEqual(0, errors);
+
+			return p;
+		}
+	}
+}
+
diff --git a/Source/UnitTests/TestUtil/Properties/AssemblyInfo.cs b/Source/UnitTests/TestUtil/Properties/AssemblyInfo.cs
new file mode 100644
index 00000000..05c9fee5
--- /dev/null
+++ b/Source/UnitTests/TestUtil/Properties/AssemblyInfo.cs
@@ -0,0 +1,36 @@
+using System.Reflection;

+using System.Runtime.CompilerServices;

+using System.Runtime.InteropServices;

+

+// General Information about an assembly is controlled through the following 

+// set of attributes. Change these attribute values to modify the information

+// associated with an assembly.

+[assembly: AssemblyTitle("TestUtil")]

+[assembly: AssemblyDescription("")]

+[assembly: AssemblyConfiguration("")]

+[assembly: AssemblyCompany("")]

+[assembly: AssemblyProduct("TestUtil")]

+[assembly: AssemblyCopyright("Copyright ©  2014")]

+[assembly: AssemblyTrademark("")]

+[assembly: AssemblyCulture("")]

+

+// Setting ComVisible to false makes the types in this assembly not visible 

+// to COM components.  If you need to access a type in this assembly from 

+// COM, set the ComVisible attribute to true on that type.

+[assembly: ComVisible(false)]

+

+// The following GUID is for the ID of the typelib if this project is exposed to COM

+[assembly: Guid("5630b725-b802-4f97-9e46-6cdfd6819269")]

+

+// Version information for an assembly consists of the following four values:

+//

+//      Major Version

+//      Minor Version 

+//      Build Number

+//      Revision

+//

+// You can specify all the values or you can default the Build and Revision Numbers 

+// by using the '*' as shown below:

+// [assembly: AssemblyVersion("1.0.*")]

+[assembly: AssemblyVersion("1.0.0.0")]

+[assembly: AssemblyFileVersion("1.0.0.0")]

diff --git a/Source/UnitTests/TestUtil/TestUtil.csproj b/Source/UnitTests/TestUtil/TestUtil.csproj
new file mode 100644
index 00000000..7642b134
--- /dev/null
+++ b/Source/UnitTests/TestUtil/TestUtil.csproj
@@ -0,0 +1,71 @@
+<?xml version="1.0" encoding="utf-8"?>

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

+  <Import Project="$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props" Condition="Exists('$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props')" />

+  <PropertyGroup>

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

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

+    <ProjectGuid>{59118E35-4236-495E-AF6E-0D641302ED2C}</ProjectGuid>

+    <OutputType>Library</OutputType>

+    <AppDesignerFolder>Properties</AppDesignerFolder>

+    <RootNamespace>TestUtil</RootNamespace>

+    <AssemblyName>TestUtil</AssemblyName>

+    <TargetFrameworkVersion>v4.5</TargetFrameworkVersion>

+    <FileAlignment>512</FileAlignment>

+  </PropertyGroup>

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

+    <DebugSymbols>true</DebugSymbols>

+    <DebugType>full</DebugType>

+    <Optimize>false</Optimize>

+    <OutputPath>bin\Debug\</OutputPath>

+    <DefineConstants>DEBUG;TRACE</DefineConstants>

+    <ErrorReport>prompt</ErrorReport>

+    <WarningLevel>4</WarningLevel>

+  </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>

+  <ItemGroup>

+    <Reference Include="nunit.framework">

+      <HintPath>..\..\packages\NUnit.2.6.3\lib\nunit.framework.dll</HintPath>

+    </Reference>

+    <Reference Include="System" />

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

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

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

+    <Reference Include="Microsoft.CSharp" />

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

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

+  </ItemGroup>

+  <ItemGroup>

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

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

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

+    <Compile Include="Properties\AssemblyInfo.cs" />

+  </ItemGroup>

+  <ItemGroup>

+    <None Include="packages.config" />

+  </ItemGroup>

+  <ItemGroup>

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

+      <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>

+  <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/UnitTests/TestUtil/packages.config b/Source/UnitTests/TestUtil/packages.config
new file mode 100644
index 00000000..d4e241a2
--- /dev/null
+++ b/Source/UnitTests/TestUtil/packages.config
@@ -0,0 +1,4 @@
+<?xml version="1.0" encoding="utf-8"?>

+<packages>

+  <package id="NUnit" version="2.6.3" targetFramework="net45" />

+</packages>
\ No newline at end of file
diff --git a/Source/UnitTests/run-unittests.py b/Source/UnitTests/run-unittests.py
new file mode 100644
index 00000000..be906edd
--- /dev/null
+++ b/Source/UnitTests/run-unittests.py
@@ -0,0 +1,124 @@
+#!/usr/bin/env python

+"""

+This is a simple script to invoke nunit-console.exe

+on Windows or Linux on all UnitTest libraries.

+"""

+import argparse

+import logging

+import os

+import subprocess

+import sys

+

+class ReturnCode:

+  SUCCESS = 0

+  CONFIG_ERROR = 1

+  RUN_ERROR = 2

+

+

+def main(args):

+  parser = argparse.ArgumentParser(description=__doc__)

+  parser.add_argument('BuildType', choices=['Release', 'Debug'],

+                      help='Build type of unit test libraries')

+  parser.add_argument('-l','--log-level',

+                      choices=['critical', 'error', 'warning', 'info', 'debug'],

+                      default='info',

+                      dest='log_level',

+                      help='Logging level. Default %(default)s')

+  parser.add_argument('--nunit-console-path', default='',

+                      help='Path to nunit-console tool. If not set the script will try to guess its location',

+                      dest='nunit_console_path'

+                     )

+  parser.add_argument('-e', '--nunit-console-extra-args', action='append',

+                      help='Pass extra arguments to nunit-console. This can be used multiple times',

+                      default=[],

+                      dest='nunit_console_extra_args'

+                     )

+  parser.add_argument('--no-progress',

+                      action='store_true',

+                      dest='no_progress',

+                      help='Suppress nunit-console progress information')

+

+

+  parsedArgs = parser.parse_args(args)

+  logging.basicConfig(level=getattr(logging, parsedArgs.log_level.upper()))

+  buildType=parsedArgs.BuildType

+

+  logging.info('Build type is {}'.format(buildType))

+

+  if parsedArgs.no_progress:

+    parsedArgs.nunit_console_extra_args.append('-nodots')

+

+  logging.info('Extra arguments to nunit-console "{}"'.format(parsedArgs.nunit_console_extra_args))

+

+  UnitTestDirRoot = os.path.dirname(os.path.abspath(__file__))

+

+  # Find nunit-console.exe

+  if parsedArgs.nunit_console_path == "":

+    # Try to guess where the tool is

+    nunitConsolePath = os.path.join(os.path.join(UnitTestDirRoot,'..'),

+                                    "packages",

+                                    "NUnit.Runners.2.6.3",

+                                    "tools",

+                                    "nunit-console.exe"

+                                   )

+    # Mono needs the path to be absolute

+    nunitConsolePath = os.path.abspath(nunitConsolePath)

+  else:

+    nunitConsolePath = parsedArgs.nunit_console_path

+

+  logging.info('Looking for NUnit console at "{}"'.format(nunitConsolePath))

+  if not os.path.exists(nunitConsolePath):

+    logging.error('Could not find NUnit console tool')

+    return ReturnCode.CONFIG_ERROR

+

+  # Find unit test libraries

+  unitTestLibraries = [ ]

+  logging.info('Searching for Unit test libraries in "{}"'.format(UnitTestDirRoot))

+  for (dirpath, dirnames, filenames) in os.walk(UnitTestDirRoot):

+

+    # Search current directory for dll with correct suffix

+    for filename in filenames:

+      if filename.endswith('Tests.dll'):

+        logging.debug('Found "{}" checking build type'.format(filename))

+

+        pathComponents = dirpath.split(os.path.sep)

+        fullPath = os.path.join(dirpath, filename)

+        try:

+          buildTypeIndex = pathComponents.index(buildType)

+          if buildTypeIndex == 0 or pathComponents[buildTypeIndex -1] != 'bin':

+            continue

+

+          logging.info('Using "{}"'.format(fullPath))

+          unitTestLibraries.append(fullPath)

+        except ValueError:

+          pass

+

+  # Run Unit tests

+  if len(unitTestLibraries) == 0:

+    logging.error('No Unit test libraries were found')

+    return ReturnCode.CONFIG_ERROR

+

+  cmd = []

+

+  if os.name == 'posix':

+    cmd.append('mono')

+

+  cmd.extend([nunitConsolePath, '-nologo'])

+

+  if len(parsedArgs.nunit_console_extra_args) > 0:

+    cmd.extend(parsedArgs.nunit_console_extra_args)

+

+  cmd.extend(unitTestLibraries)

+  logging.info('Running "{}"'.format(cmd))

+  exitCode = subprocess.call(cmd)

+  if exitCode != 0:

+    logging.error('FAILED!')

+    return ReturnCode.RUN_ERROR

+  else:

+    logging.info('Succeeded')

+

+  return ReturnCode.SUCCESS

+

+

+if __name__ == '__main__':

+  sys.exit(main(sys.argv[1:]))