6 files changed, 1669 insertions, 1669 deletions

diff --git a/Source/Basetypes/Basetypes.csproj b/Source/Basetypes/Basetypes.csproj
index 4ecdee8d..5b425bc5 100644
--- a/Source/Basetypes/Basetypes.csproj
+++ b/Source/Basetypes/Basetypes.csproj
@@ -1,204 +1,204 @@
-<?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>9.0.21022</ProductVersion>

-    <SchemaVersion>2.0</SchemaVersion>

-    <ProjectGuid>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</ProjectGuid>

-    <OutputType>Library</OutputType>

-    <AppDesignerFolder>Properties</AppDesignerFolder>

-    <RootNamespace>Basetypes</RootNamespace>

-    <AssemblyName>Basetypes</AssemblyName>

-    <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>

-    <FileAlignment>512</FileAlignment>

-    <CodeContractsAssemblyMode>1</CodeContractsAssemblyMode>

-    <SignAssembly>true</SignAssembly>

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

-    <FileUpgradeFlags>

-    </FileUpgradeFlags>

-    <OldToolsVersion>3.5</OldToolsVersion>

-    <UpgradeBackupLocation />

-    <PublishUrl>publish\</PublishUrl>

-    <Install>true</Install>

-    <InstallFrom>Disk</InstallFrom>

-    <UpdateEnabled>false</UpdateEnabled>

-    <UpdateMode>Foreground</UpdateMode>

-    <UpdateInterval>7</UpdateInterval>

-    <UpdateIntervalUnits>Days</UpdateIntervalUnits>

-    <UpdatePeriodically>false</UpdatePeriodically>

-    <UpdateRequired>false</UpdateRequired>

-    <MapFileExtensions>true</MapFileExtensions>

-    <ApplicationRevision>0</ApplicationRevision>

-    <ApplicationVersion>1.0.0.%2a</ApplicationVersion>

-    <IsWebBootstrapper>false</IsWebBootstrapper>

-    <UseApplicationTrust>false</UseApplicationTrust>

-    <BootstrapperEnabled>true</BootstrapperEnabled>

-    <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'">Client</TargetFrameworkProfile>

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

-    <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>

-    <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>

-    <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>

-    <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>

-    <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>

-    <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>

-    <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>

-    <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>

-    <CodeContractsPointerObligations>False</CodeContractsPointerObligations>

-    <CodeContractsContainerAnalysis>False</CodeContractsContainerAnalysis>

-    <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>

-    <CodeContractsRunInBackground>True</CodeContractsRunInBackground>

-    <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>

-    <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>

-    <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>

-    <CodeContractsCustomRewriterAssembly>

-    </CodeContractsCustomRewriterAssembly>

-    <CodeContractsCustomRewriterClass>

-    </CodeContractsCustomRewriterClass>

-    <CodeContractsLibPaths>

-    </CodeContractsLibPaths>

-    <CodeContractsExtraRewriteOptions>

-    </CodeContractsExtraRewriteOptions>

-    <CodeContractsExtraAnalysisOptions>

-    </CodeContractsExtraAnalysisOptions>

-    <CodeContractsBaseLineFile>

-    </CodeContractsBaseLineFile>

-    <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>

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

-    <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>

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

-    <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>

-  </PropertyGroup>

-  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'z3apidebug|AnyCPU' ">

-    <DebugSymbols>true</DebugSymbols>

-    <OutputPath>bin\z3apidebug\</OutputPath>

-    <DefineConstants>DEBUG;TRACE</DefineConstants>

-    <DebugType>full</DebugType>

-    <PlatformTarget>AnyCPU</PlatformTarget>

-    <CodeAnalysisRuleAssemblies>

-    </CodeAnalysisRuleAssemblies>

-    <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>

-    <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>

-    <ErrorReport>prompt</ErrorReport>

-    <CodeAnalysisRuleSet>Migrated rules for Basetypes.ruleset</CodeAnalysisRuleSet>

-    <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>

-    <WarningLevel>4</WarningLevel>

-    <Optimize>false</Optimize>

-  </PropertyGroup>

-  <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|AnyCPU'">

-    <DebugSymbols>true</DebugSymbols>

-    <OutputPath>bin\Checked\</OutputPath>

-    <DefineConstants>DEBUG;TRACE</DefineConstants>

-    <DebugType>full</DebugType>

-    <PlatformTarget>AnyCPU</PlatformTarget>

-    <CodeAnalysisLogFile>bin\Debug\Basetypes.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>

-    <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>

-    <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>

-    <ErrorReport>prompt</ErrorReport>

-    <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>

-    <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>

-    <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>

-    <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>

-    <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>

-    <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>

-    <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>

-    <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>

-    <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>

-    <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>

-    <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>

-    <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>

-    <CodeContractsEnumObligations>False</CodeContractsEnumObligations>

-    <CodeContractsPointerObligations>False</CodeContractsPointerObligations>

-    <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>

-    <CodeContractsRunInBackground>True</CodeContractsRunInBackground>

-    <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>

-    <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>

-    <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>

-    <CodeContractsCustomRewriterAssembly />

-    <CodeContractsCustomRewriterClass />

-    <CodeContractsLibPaths />

-    <CodeContractsExtraRewriteOptions />

-    <CodeContractsExtraAnalysisOptions />

-    <CodeContractsBaseLineFile />

-    <CodeContractsCacheAnalysisResults>False</CodeContractsCacheAnalysisResults>

-    <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>

-    <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>

-    <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>

-    <WarningLevel>4</WarningLevel>

-    <Optimize>false</Optimize>

-  </PropertyGroup>

-  <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'QED|AnyCPU'">

-    <DebugSymbols>true</DebugSymbols>

-    <OutputPath>bin\QED\</OutputPath>

-    <DefineConstants>DEBUG;TRACE</DefineConstants>

-    <DebugType>full</DebugType>

-    <PlatformTarget>AnyCPU</PlatformTarget>

-    <ErrorReport>prompt</ErrorReport>

-    <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>

-  </PropertyGroup>

-  <ItemGroup>

-    <Reference Include="System" />

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

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

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

-  </ItemGroup>

-  <ItemGroup>

-    <Compile Include="..\version.cs">

-      <Link>version.cs</Link>

-    </Compile>

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

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

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

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

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

-  </ItemGroup>

-  <ItemGroup>

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

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

-      <Name>CodeContractsExtender</Name>

-    </ProjectReference>

-  </ItemGroup>

-  <ItemGroup>

-    <Folder Include="Properties\" />

-  </ItemGroup>

-  <ItemGroup>

-    <BootstrapperPackage Include="Microsoft.Net.Client.3.5">

-      <Visible>False</Visible>

-      <ProductName>.NET Framework 3.5 SP1 Client Profile</ProductName>

-      <Install>false</Install>

-    </BootstrapperPackage>

-    <BootstrapperPackage Include="Microsoft.Net.Framework.3.5.SP1">

-      <Visible>False</Visible>

-      <ProductName>.NET Framework 3.5 SP1</ProductName>

-      <Install>true</Install>

-    </BootstrapperPackage>

-    <BootstrapperPackage Include="Microsoft.Windows.Installer.3.1">

-      <Visible>False</Visible>

-      <ProductName>Windows Installer 3.1</ProductName>

-      <Install>true</Install>

-    </BootstrapperPackage>

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

-  -->

+<?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>9.0.21022</ProductVersion>
+    <SchemaVersion>2.0</SchemaVersion>
+    <ProjectGuid>{43DFAD18-3E35-4558-9BE2-CAFF6B5BA8A0}</ProjectGuid>
+    <OutputType>Library</OutputType>
+    <AppDesignerFolder>Properties</AppDesignerFolder>
+    <RootNamespace>Basetypes</RootNamespace>
+    <AssemblyName>BoogieBasetypes</AssemblyName>
+    <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
+    <FileAlignment>512</FileAlignment>
+    <CodeContractsAssemblyMode>1</CodeContractsAssemblyMode>
+    <SignAssembly>true</SignAssembly>
+    <AssemblyOriginatorKeyFile>..\InterimKey.snk</AssemblyOriginatorKeyFile>
+    <FileUpgradeFlags>
+    </FileUpgradeFlags>
+    <OldToolsVersion>3.5</OldToolsVersion>
+    <UpgradeBackupLocation />
+    <PublishUrl>publish\</PublishUrl>
+    <Install>true</Install>
+    <InstallFrom>Disk</InstallFrom>
+    <UpdateEnabled>false</UpdateEnabled>
+    <UpdateMode>Foreground</UpdateMode>
+    <UpdateInterval>7</UpdateInterval>
+    <UpdateIntervalUnits>Days</UpdateIntervalUnits>
+    <UpdatePeriodically>false</UpdatePeriodically>
+    <UpdateRequired>false</UpdateRequired>
+    <MapFileExtensions>true</MapFileExtensions>
+    <ApplicationRevision>0</ApplicationRevision>
+    <ApplicationVersion>1.0.0.%2a</ApplicationVersion>
+    <IsWebBootstrapper>false</IsWebBootstrapper>
+    <UseApplicationTrust>false</UseApplicationTrust>
+    <BootstrapperEnabled>true</BootstrapperEnabled>
+    <TargetFrameworkProfile Condition=" '$(OS)' == 'Windows_NT'">Client</TargetFrameworkProfile>
+  </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>
+    <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>
+    <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
+    <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
+    <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
+    <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
+    <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>
+    <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>
+    <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
+    <CodeContractsPointerObligations>False</CodeContractsPointerObligations>
+    <CodeContractsContainerAnalysis>False</CodeContractsContainerAnalysis>
+    <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
+    <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
+    <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>
+    <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
+    <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
+    <CodeContractsCustomRewriterAssembly>
+    </CodeContractsCustomRewriterAssembly>
+    <CodeContractsCustomRewriterClass>
+    </CodeContractsCustomRewriterClass>
+    <CodeContractsLibPaths>
+    </CodeContractsLibPaths>
+    <CodeContractsExtraRewriteOptions>
+    </CodeContractsExtraRewriteOptions>
+    <CodeContractsExtraAnalysisOptions>
+    </CodeContractsExtraAnalysisOptions>
+    <CodeContractsBaseLineFile>
+    </CodeContractsBaseLineFile>
+    <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
+    <CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>
+    <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
+  </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>
+    <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
+  </PropertyGroup>
+  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'z3apidebug|AnyCPU' ">
+    <DebugSymbols>true</DebugSymbols>
+    <OutputPath>bin\z3apidebug\</OutputPath>
+    <DefineConstants>DEBUG;TRACE</DefineConstants>
+    <DebugType>full</DebugType>
+    <PlatformTarget>AnyCPU</PlatformTarget>
+    <CodeAnalysisRuleAssemblies>
+    </CodeAnalysisRuleAssemblies>
+    <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
+    <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
+    <ErrorReport>prompt</ErrorReport>
+    <CodeAnalysisRuleSet>Migrated rules for Basetypes.ruleset</CodeAnalysisRuleSet>
+    <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
+    <WarningLevel>4</WarningLevel>
+    <Optimize>false</Optimize>
+  </PropertyGroup>
+  <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Checked|AnyCPU'">
+    <DebugSymbols>true</DebugSymbols>
+    <OutputPath>bin\Checked\</OutputPath>
+    <DefineConstants>DEBUG;TRACE</DefineConstants>
+    <DebugType>full</DebugType>
+    <PlatformTarget>AnyCPU</PlatformTarget>
+    <CodeAnalysisLogFile>bin\Debug\Basetypes.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>
+    <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
+    <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
+    <ErrorReport>prompt</ErrorReport>
+    <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
+    <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
+    <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
+    <CodeContractsEnableRuntimeChecking>True</CodeContractsEnableRuntimeChecking>
+    <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
+    <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
+    <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
+    <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
+    <CodeContractsRunCodeAnalysis>False</CodeContractsRunCodeAnalysis>
+    <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>
+    <CodeContractsBoundsObligations>False</CodeContractsBoundsObligations>
+    <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
+    <CodeContractsEnumObligations>False</CodeContractsEnumObligations>
+    <CodeContractsPointerObligations>False</CodeContractsPointerObligations>
+    <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
+    <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
+    <CodeContractsShowSquigglies>False</CodeContractsShowSquigglies>
+    <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
+    <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
+    <CodeContractsCustomRewriterAssembly />
+    <CodeContractsCustomRewriterClass />
+    <CodeContractsLibPaths />
+    <CodeContractsExtraRewriteOptions />
+    <CodeContractsExtraAnalysisOptions />
+    <CodeContractsBaseLineFile />
+    <CodeContractsCacheAnalysisResults>False</CodeContractsCacheAnalysisResults>
+    <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
+    <CodeContractsReferenceAssembly>Build</CodeContractsReferenceAssembly>
+    <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
+    <WarningLevel>4</WarningLevel>
+    <Optimize>false</Optimize>
+  </PropertyGroup>
+  <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'QED|AnyCPU'">
+    <DebugSymbols>true</DebugSymbols>
+    <OutputPath>bin\QED\</OutputPath>
+    <DefineConstants>DEBUG;TRACE</DefineConstants>
+    <DebugType>full</DebugType>
+    <PlatformTarget>AnyCPU</PlatformTarget>
+    <ErrorReport>prompt</ErrorReport>
+    <CodeAnalysisRuleSet>AllRules.ruleset</CodeAnalysisRuleSet>
+  </PropertyGroup>
+  <ItemGroup>
+    <Reference Include="System" />
+    <Reference Include="System.Data" />
+    <Reference Include="System.Numerics" />
+    <Reference Include="System.Xml" />
+  </ItemGroup>
+  <ItemGroup>
+    <Compile Include="..\version.cs">
+      <Link>version.cs</Link>
+    </Compile>
+    <Compile Include="BigDec.cs" />
+    <Compile Include="BigNum.cs" />
+    <Compile Include="BigFloat.cs" />
+    <Compile Include="Rational.cs" />
+    <Compile Include="Set.cs" />
+  </ItemGroup>
+  <ItemGroup>
+    <ProjectReference Include="..\CodeContractsExtender\CodeContractsExtender.csproj">
+      <Project>{ACCC0156-0921-43ED-8F67-AD8BDC8CDE31}</Project>
+      <Name>CodeContractsExtender</Name>
+    </ProjectReference>
+  </ItemGroup>
+  <ItemGroup>
+    <Folder Include="Properties\" />
+  </ItemGroup>
+  <ItemGroup>
+    <BootstrapperPackage Include="Microsoft.Net.Client.3.5">
+      <Visible>False</Visible>
+      <ProductName>.NET Framework 3.5 SP1 Client Profile</ProductName>
+      <Install>false</Install>
+    </BootstrapperPackage>
+    <BootstrapperPackage Include="Microsoft.Net.Framework.3.5.SP1">
+      <Visible>False</Visible>
+      <ProductName>.NET Framework 3.5 SP1</ProductName>
+      <Install>true</Install>
+    </BootstrapperPackage>
+    <BootstrapperPackage Include="Microsoft.Windows.Installer.3.1">
+      <Visible>False</Visible>
+      <ProductName>Windows Installer 3.1</ProductName>
+      <Install>true</Install>
+    </BootstrapperPackage>
+  </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/Basetypes/BigDec.cs b/Source/Basetypes/BigDec.cs
index 0aeea8b1..e4666793 100644
--- a/Source/Basetypes/BigDec.cs
+++ b/Source/Basetypes/BigDec.cs
@@ -1,380 +1,380 @@
-//-----------------------------------------------------------------------------

-//

-// Copyright (C) Microsoft Corporation.  All Rights Reserved.

-//

-//-----------------------------------------------------------------------------

-using System;

-using System.Text;

-using System.Diagnostics.Contracts;

-using System.Diagnostics;

-

-

-namespace Microsoft.Basetypes {

-  using BIM = System.Numerics.BigInteger;

-

-

-  /// <summary>

-  /// A representation of decimal values.

-  /// </summary>

-  public struct BigDec {

-

-    // the internal representation

-    [Rep]

-    internal readonly BIM mantissa;

-    [Rep]

-    internal readonly int exponent;

-

-    public BIM Mantissa {

-      get {

-        return mantissa;

-      }

-    }

-

-    public int Exponent {

-      get {

-        return exponent;

-      }

-    }

-

-    public static readonly BigDec ZERO = FromInt(0);

-    private static readonly BIM ten = new BIM(10);

-

-

-    ////////////////////////////////////////////////////////////////////////////

-    // Constructors

-

-    [Pure]

-    public static BigDec FromInt(int v) {

-      return new BigDec(v, 0);

-    }

-

-    [Pure]

-    public static BigDec FromBigInt(BIM v) {

-      return new BigDec(v, 0);

-    }

-

-    [Pure]

-    public static BigDec FromString(string v) {

-      if (v == null) throw new FormatException();

-

-      BIM integral = BIM.Zero;

-      BIM fraction = BIM.Zero;

-      int exponent = 0;

-

-      int len = v.Length;

-

-      int i = v.IndexOf('e');

-      if (i >= 0) {

-        if (i + 1 == v.Length) throw new FormatException();

-        exponent = Int32.Parse(v.Substring(i + 1, len - i - 1));

-        len = i;

-      }

-

-      int fractionLen = 0;

-      i = v.IndexOf('.');

-      if (i >= 0) {

-        if (i + 1 == v.Length) throw new FormatException();

-        fractionLen = len - i - 1;

-        fraction = BIM.Parse(v.Substring(i + 1, fractionLen));

-        len = i;

-      }

-

-      integral = BIM.Parse(v.Substring(0, len));

-

-      if (!fraction.IsZero) {

-        while (fractionLen > 0) {

-          integral = integral * ten;

-          exponent = exponent - 1;

-          fractionLen = fractionLen - 1;

-        }

-      }

-

-      if (integral.Sign == -1) {

-        return new BigDec(integral - fraction, exponent);

-      }

-      else {

-        return new BigDec(integral + fraction, exponent);

-      }

-    }

-

-    internal BigDec(BIM mantissa, int exponent) {

-      if (mantissa.IsZero) {

-        this.mantissa = mantissa;

-        this.exponent = 0;

-      }

-      else {

-        while (mantissa % ten == BIM.Zero) {

-          mantissa = mantissa / ten;

-          exponent = exponent + 1;

-        }

-        this.mantissa = mantissa;

-        this.exponent = exponent;

-      }

-    }

-

-

-    ////////////////////////////////////////////////////////////////////////////

-    // Basic object operations

-

-    [Pure]

-    [Reads(ReadsAttribute.Reads.Nothing)]

-    public override bool Equals(object obj) {

-      if (obj == null)

-        return false;

-      if (!(obj is BigDec))

-        return false;

-

-      return (this == (BigDec)obj);

-    }

-

-    [Pure]

-    public override int GetHashCode() {

-      return this.mantissa.GetHashCode() * 13 + this.exponent.GetHashCode();

-    }

-

-    [Pure]

-    public override string/*!*/ ToString() {

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

-      return String.Format("{0}e{1}", this.mantissa.ToString(), this.exponent.ToString());

-    }

-

-

-    ////////////////////////////////////////////////////////////////////////////

-    // Conversion operations

-

-    // ``floor`` rounds towards negative infinity (like SMT-LIBv2's to_int).

-    /// <summary>

-    /// Computes the floor and ceiling of this BigDec. Note the choice of rounding towards negative

-    /// infinity rather than zero for floor is because SMT-LIBv2's to_int function floors this way.

-    /// </summary>

-    /// <param name="floor">The Floor (rounded towards negative infinity)</param>

-    /// <param name="ceiling">Ceiling (rounded towards positive infinity)</param>

-    public void FloorCeiling(out BIM floor, out BIM ceiling) {

-      BIM n = this.mantissa;

-      int e = this.exponent;

-      if (n.IsZero) {

-        floor = ceiling = n;

-      } else if (0 <= e) {

-        // it's an integer

-        for (; 0 < e; e--) {

-          n = n * ten;

-        }

-        floor = ceiling = n;

-      } else {

-        // it's a non-zero integer, so the ceiling is one more than the floor

-        for (; e < 0 && !n.IsZero; e++) {

-          n = n / ten;  // Division rounds towards negative infinity

-        }

-

-        if (this.mantissa >= 0) {

-          floor = n;

-          ceiling = n + 1;

-        } else {

-          ceiling = n;

-          floor = n - 1;

-        }

-      }

-      Debug.Assert(floor <= ceiling, "Invariant was not maintained");

-    }

-

-    [Pure]

-    public String ToDecimalString(int maxDigits) {

-      string s = this.mantissa.ToString();

-      int digits = (this.mantissa >= 0) ? s.Length : s.Length - 1;

-      BIM max = BIM.Pow(10, maxDigits);

-      BIM min = -max;

-

-      if (this.exponent >= 0) {

-        if (maxDigits < digits || maxDigits - digits < this.exponent) {

-          return String.Format("{0}.0", (this.mantissa >= 0) ? max.ToString() : min.ToString());

-        }

-        else {

-          return String.Format("{0}{1}.0", s, new string('0', this.exponent));

-        }

-      }

-      else {

-        int exp = -this.exponent;

-

-        if (exp < digits) {

-          int intDigits = digits - exp;

-          if (maxDigits < intDigits) {

-            return String.Format("{0}.0", (this.mantissa >= 0) ? max.ToString() : min.ToString());

-          }

-          else {

-            int fracDigits = Math.Min(maxDigits, digits - intDigits);

-            return String.Format("{0}.{1}", s.Substring(0, intDigits), s.Substring(intDigits, fracDigits));

-          }

-        }

-        else {

-          int fracDigits = Math.Min(maxDigits, digits);

-          return String.Format("0.{0}{1}", new string('0', exp - fracDigits), s.Substring(0, fracDigits));

-        }

-      }

-    }

-

-    [Pure]

-    public string ToDecimalString() {

-      string m = this.mantissa.ToString();

-      var e = this.exponent;

-      if (0 <= this.exponent) {

-        return m + Zeros(e) + ".0";

-      } else {

-        e = -e;

-        // compute k to be the longest suffix of m consisting of all zeros (but no longer than e, and not the entire string)

-        var maxK = e < m.Length ? e : m.Length - 1;

-        var last = m.Length - 1;

-        var k = 0;

-        while (k < maxK && m[last - k] == '0') {

-          k++;

-        }

-        if (0 < k) {

-          // chop off the suffix of k zeros from m and adjust e accordingly

-          m = m.Substring(0, m.Length - k);

-          e -= k;

-        }

-        if (e == 0) {

-          return m;

-        } else if (e < m.Length) {

-          var n = m.Length - e;

-          return m.Substring(0, n) + "." + m.Substring(n);

-        } else {

-          return "0." + Zeros(e - m.Length) + m;

-        }

-      }

-    }

-

-    [Pure]

-    public static string Zeros(int n) {

-      Contract.Requires(0 <= n);

-      if (n <= 10) {

-        var tenZeros = "0000000000";

-        return tenZeros.Substring(0, n);

-      } else {

-        var d = n / 2;

-        var s = Zeros(d);

-        if (n % 2 == 0) {

-          return s + s;

-        } else {

-          return s + s + "0";

-        }

-      }

-    }

-

-

-    ////////////////////////////////////////////////////////////////////////////

-    // Basic arithmetic operations

-

-    [Pure]

-    public BigDec Abs {

-      get {

-        return new BigDec(BIM.Abs(this.mantissa), this.exponent);

-      }

-    }

-

-    [Pure]

-    public BigDec Negate {

-      get {

-        return new BigDec(BIM.Negate(this.mantissa), this.exponent);

-      }

-    }

-

-    [Pure]

-    public static BigDec operator -(BigDec x) {

-      return x.Negate;

-    }

-

-    [Pure]

-    public static BigDec operator +(BigDec x, BigDec y) {

-      BIM m1 = x.mantissa;

-      int e1 = x.exponent;

-      BIM m2 = y.mantissa;

-      int e2 = y.exponent;

-      if (e2 < e1) {

-        m1 = y.mantissa;

-        e1 = y.exponent;

-        m2 = x.mantissa;

-        e2 = x.exponent;

-      }

-

-      while (e2 > e1) {

-        m2 = m2 * ten;

-        e2 = e2 - 1;

-      }

-

-      return new BigDec(m1 + m2, e1);

-    }

-

-    [Pure]

-    public static BigDec operator -(BigDec x, BigDec y) {

-      return x + y.Negate;

-    }

-

-    [Pure]

-    public static BigDec operator *(BigDec x, BigDec y) {

-      return new BigDec(x.mantissa * y.mantissa, x.exponent + y.exponent);

-    }

-

-

-    ////////////////////////////////////////////////////////////////////////////

-    // Some basic comparison operations

-

-    public bool IsPositive {

-      get {

-        return (this.mantissa > BIM.Zero);

-      }

-    }

-

-    public bool IsNegative {

-      get {

-        return (this.mantissa < BIM.Zero);

-      }

-    }

-

-    public bool IsZero {

-      get {

-        return this.mantissa.IsZero;

-      }

-    }

-

-    [Pure]

-    public int CompareTo(BigDec that) {

-      if (this.mantissa == that.mantissa && this.exponent == that.exponent) {

-        return 0;

-      }

-      else {

-        BigDec d = this - that;

-        return d.IsNegative ? -1 : 1;

-      }

-    }

-

-    [Pure]

-    public static bool operator ==(BigDec x, BigDec y) {

-      return x.CompareTo(y) == 0;

-    }

-

-    [Pure]

-    public static bool operator !=(BigDec x, BigDec y) {

-      return x.CompareTo(y) != 0;

-    }

-

-    [Pure]

-    public static bool operator <(BigDec x, BigDec y) {

-      return x.CompareTo(y) < 0;

-    }

-

-    [Pure]

-    public static bool operator >(BigDec x, BigDec y) {

-      return x.CompareTo(y) > 0;

-    }

-

-    [Pure]

-    public static bool operator <=(BigDec x, BigDec y) {

-      return x.CompareTo(y) <= 0;

-    }

-

-    [Pure]

-    public static bool operator >=(BigDec x, BigDec y) {

-      return x.CompareTo(y) >= 0;

-    }

-  }

-}

+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Text;
+using System.Diagnostics.Contracts;
+using System.Diagnostics;
+
+
+namespace Microsoft.Basetypes {
+  using BIM = System.Numerics.BigInteger;
+
+
+  /// <summary>
+  /// A representation of decimal values.
+  /// </summary>
+  public struct BigDec {
+
+    // the internal representation
+    [Rep]
+    internal readonly BIM mantissa;
+    [Rep]
+    internal readonly int exponent;
+
+    public BIM Mantissa {
+      get {
+        return mantissa;
+      }
+    }
+
+    public int Exponent {
+      get {
+        return exponent;
+      }
+    }
+
+    public static readonly BigDec ZERO = FromInt(0);
+    private static readonly BIM ten = new BIM(10);
+
+
+    ////////////////////////////////////////////////////////////////////////////
+    // Constructors
+
+    [Pure]
+    public static BigDec FromInt(int v) {
+      return new BigDec(v, 0);
+    }
+
+    [Pure]
+    public static BigDec FromBigInt(BIM v) {
+      return new BigDec(v, 0);
+    }
+
+    [Pure]
+    public static BigDec FromString(string v) {
+      if (v == null) throw new FormatException();
+
+      BIM integral = BIM.Zero;
+      BIM fraction = BIM.Zero;
+      int exponent = 0;
+
+      int len = v.Length;
+
+      int i = v.IndexOf('e');
+      if (i >= 0) {
+        if (i + 1 == v.Length) throw new FormatException();
+        exponent = Int32.Parse(v.Substring(i + 1, len - i - 1));
+        len = i;
+      }
+
+      int fractionLen = 0;
+      i = v.IndexOf('.');
+      if (i >= 0) {
+        if (i + 1 == v.Length) throw new FormatException();
+        fractionLen = len - i - 1;
+        fraction = BIM.Parse(v.Substring(i + 1, fractionLen));
+        len = i;
+      }
+
+      integral = BIM.Parse(v.Substring(0, len));
+
+      if (!fraction.IsZero) {
+        while (fractionLen > 0) {
+          integral = integral * ten;
+          exponent = exponent - 1;
+          fractionLen = fractionLen - 1;
+        }
+      }
+
+      if (integral.Sign == -1) {
+        return new BigDec(integral - fraction, exponent);
+      }
+      else {
+        return new BigDec(integral + fraction, exponent);
+      }
+    }
+
+    internal BigDec(BIM mantissa, int exponent) {
+      if (mantissa.IsZero) {
+        this.mantissa = mantissa;
+        this.exponent = 0;
+      }
+      else {
+        while (mantissa % ten == BIM.Zero) {
+          mantissa = mantissa / ten;
+          exponent = exponent + 1;
+        }
+        this.mantissa = mantissa;
+        this.exponent = exponent;
+      }
+    }
+
+
+    ////////////////////////////////////////////////////////////////////////////
+    // Basic object operations
+
+    [Pure]
+    [Reads(ReadsAttribute.Reads.Nothing)]
+    public override bool Equals(object obj) {
+      if (obj == null)
+        return false;
+      if (!(obj is BigDec))
+        return false;
+
+      return (this == (BigDec)obj);
+    }
+
+    [Pure]
+    public override int GetHashCode() {
+      return this.mantissa.GetHashCode() * 13 + this.exponent.GetHashCode();
+    }
+
+    [Pure]
+    public override string/*!*/ ToString() {
+      Contract.Ensures(Contract.Result<string>() != null);
+      return String.Format("{0}e{1}", this.mantissa.ToString(), this.exponent.ToString());
+    }
+
+
+    ////////////////////////////////////////////////////////////////////////////
+    // Conversion operations
+
+    // ``floor`` rounds towards negative infinity (like SMT-LIBv2's to_int).
+    /// <summary>
+    /// Computes the floor and ceiling of this BigDec. Note the choice of rounding towards negative
+    /// infinity rather than zero for floor is because SMT-LIBv2's to_int function floors this way.
+    /// </summary>
+    /// <param name="floor">The Floor (rounded towards negative infinity)</param>
+    /// <param name="ceiling">Ceiling (rounded towards positive infinity)</param>
+    public void FloorCeiling(out BIM floor, out BIM ceiling) {
+      BIM n = this.mantissa;
+      int e = this.exponent;
+      if (n.IsZero) {
+        floor = ceiling = n;
+      } else if (0 <= e) {
+        // it's an integer
+        for (; 0 < e; e--) {
+          n = n * ten;
+        }
+        floor = ceiling = n;
+      } else {
+        // it's a non-zero integer, so the ceiling is one more than the floor
+        for (; e < 0 && !n.IsZero; e++) {
+          n = n / ten;  // Division rounds towards negative infinity
+        }
+
+        if (this.mantissa >= 0) {
+          floor = n;
+          ceiling = n + 1;
+        } else {
+          ceiling = n;
+          floor = n - 1;
+        }
+      }
+      Debug.Assert(floor <= ceiling, "Invariant was not maintained");
+    }
+
+    [Pure]
+    public String ToDecimalString(int maxDigits) {
+      string s = this.mantissa.ToString();
+      int digits = (this.mantissa >= 0) ? s.Length : s.Length - 1;
+      BIM max = BIM.Pow(10, maxDigits);
+      BIM min = -max;
+
+      if (this.exponent >= 0) {
+        if (maxDigits < digits || maxDigits - digits < this.exponent) {
+          return String.Format("{0}.0", (this.mantissa >= 0) ? max.ToString() : min.ToString());
+        }
+        else {
+          return String.Format("{0}{1}.0", s, new string('0', this.exponent));
+        }
+      }
+      else {
+        int exp = -this.exponent;
+
+        if (exp < digits) {
+          int intDigits = digits - exp;
+          if (maxDigits < intDigits) {
+            return String.Format("{0}.0", (this.mantissa >= 0) ? max.ToString() : min.ToString());
+          }
+          else {
+            int fracDigits = Math.Min(maxDigits, digits - intDigits);
+            return String.Format("{0}.{1}", s.Substring(0, intDigits), s.Substring(intDigits, fracDigits));
+          }
+        }
+        else {
+          int fracDigits = Math.Min(maxDigits, digits);
+          return String.Format("0.{0}{1}", new string('0', exp - fracDigits), s.Substring(0, fracDigits));
+        }
+      }
+    }
+
+    [Pure]
+    public string ToDecimalString() {
+      string m = this.mantissa.ToString();
+      var e = this.exponent;
+      if (0 <= this.exponent) {
+        return m + Zeros(e) + ".0";
+      } else {
+        e = -e;
+        // compute k to be the longest suffix of m consisting of all zeros (but no longer than e, and not the entire string)
+        var maxK = e < m.Length ? e : m.Length - 1;
+        var last = m.Length - 1;
+        var k = 0;
+        while (k < maxK && m[last - k] == '0') {
+          k++;
+        }
+        if (0 < k) {
+          // chop off the suffix of k zeros from m and adjust e accordingly
+          m = m.Substring(0, m.Length - k);
+          e -= k;
+        }
+        if (e == 0) {
+          return m;
+        } else if (e < m.Length) {
+          var n = m.Length - e;
+          return m.Substring(0, n) + "." + m.Substring(n);
+        } else {
+          return "0." + Zeros(e - m.Length) + m;
+        }
+      }
+    }
+
+    [Pure]
+    public static string Zeros(int n) {
+      Contract.Requires(0 <= n);
+      if (n <= 10) {
+        var tenZeros = "0000000000";
+        return tenZeros.Substring(0, n);
+      } else {
+        var d = n / 2;
+        var s = Zeros(d);
+        if (n % 2 == 0) {
+          return s + s;
+        } else {
+          return s + s + "0";
+        }
+      }
+    }
+
+
+    ////////////////////////////////////////////////////////////////////////////
+    // Basic arithmetic operations
+
+    [Pure]
+    public BigDec Abs {
+      get {
+        return new BigDec(BIM.Abs(this.mantissa), this.exponent);
+      }
+    }
+
+    [Pure]
+    public BigDec Negate {
+      get {
+        return new BigDec(BIM.Negate(this.mantissa), this.exponent);
+      }
+    }
+
+    [Pure]
+    public static BigDec operator -(BigDec x) {
+      return x.Negate;
+    }
+
+    [Pure]
+    public static BigDec operator +(BigDec x, BigDec y) {
+      BIM m1 = x.mantissa;
+      int e1 = x.exponent;
+      BIM m2 = y.mantissa;
+      int e2 = y.exponent;
+      if (e2 < e1) {
+        m1 = y.mantissa;
+        e1 = y.exponent;
+        m2 = x.mantissa;
+        e2 = x.exponent;
+      }
+
+      while (e2 > e1) {
+        m2 = m2 * ten;
+        e2 = e2 - 1;
+      }
+
+      return new BigDec(m1 + m2, e1);
+    }
+
+    [Pure]
+    public static BigDec operator -(BigDec x, BigDec y) {
+      return x + y.Negate;
+    }
+
+    [Pure]
+    public static BigDec operator *(BigDec x, BigDec y) {
+      return new BigDec(x.mantissa * y.mantissa, x.exponent + y.exponent);
+    }
+
+
+    ////////////////////////////////////////////////////////////////////////////
+    // Some basic comparison operations
+
+    public bool IsPositive {
+      get {
+        return (this.mantissa > BIM.Zero);
+      }
+    }
+
+    public bool IsNegative {
+      get {
+        return (this.mantissa < BIM.Zero);
+      }
+    }
+
+    public bool IsZero {
+      get {
+        return this.mantissa.IsZero;
+      }
+    }
+
+    [Pure]
+    public int CompareTo(BigDec that) {
+      if (this.mantissa == that.mantissa && this.exponent == that.exponent) {
+        return 0;
+      }
+      else {
+        BigDec d = this - that;
+        return d.IsNegative ? -1 : 1;
+      }
+    }
+
+    [Pure]
+    public static bool operator ==(BigDec x, BigDec y) {
+      return x.CompareTo(y) == 0;
+    }
+
+    [Pure]
+    public static bool operator !=(BigDec x, BigDec y) {
+      return x.CompareTo(y) != 0;
+    }
+
+    [Pure]
+    public static bool operator <(BigDec x, BigDec y) {
+      return x.CompareTo(y) < 0;
+    }
+
+    [Pure]
+    public static bool operator >(BigDec x, BigDec y) {
+      return x.CompareTo(y) > 0;
+    }
+
+    [Pure]
+    public static bool operator <=(BigDec x, BigDec y) {
+      return x.CompareTo(y) <= 0;
+    }
+
+    [Pure]
+    public static bool operator >=(BigDec x, BigDec y) {
+      return x.CompareTo(y) >= 0;
+    }
+  }
+}
diff --git a/Source/Basetypes/BigNum.cs b/Source/Basetypes/BigNum.cs
index ff676bc6..4469f149 100644
--- a/Source/Basetypes/BigNum.cs
+++ b/Source/Basetypes/BigNum.cs
@@ -1,361 +1,361 @@
-//-----------------------------------------------------------------------------

-//

-// Copyright (C) Microsoft Corporation.  All Rights Reserved.

-//

-//-----------------------------------------------------------------------------

-using System;

-using System.Text;

-using System.Diagnostics.Contracts;

-

-

-namespace Microsoft.Basetypes {

-  using BIM = System.Numerics.BigInteger;

-

-  /// <summary>

-  /// A thin wrapper around System.Numerics.BigInteger

-  /// (to be able to define equality, etc. properly)

-  /// </summary>

-  public struct BigNum {

-

-    // the internal representation

-    [Rep]

-    internal readonly System.Numerics.BigInteger val;

-    public static readonly BigNum ZERO = new BigNum(BIM.Zero);

-    public static readonly BigNum ONE = new BigNum(BIM.One);

-    public static readonly BigNum MINUS_ONE = new BigNum(-BIM.One);

-

-    [Pure]

-    public static BigNum FromInt(int v) {

-      return new BigNum(new BIM(v));

-    }

-

-    [Pure]

-    public static BigNum FromUInt(uint v) {

-      return new BigNum(new BIM((long)v));

-    }

-

-    [Pure]

-    public static BigNum FromLong(long v) {

-      return new BigNum(new BIM(v));

-    }

-

-    [Pure]

-    public static BigNum FromBigInt(System.Numerics.BigInteger v) {

-      return new BigNum(v);

-    }

-

-    [Pure]

-    public static BigNum FromULong(ulong v) {

-      return FromString("" + v);

-    }

-

-    [Pure]

-    public static BigNum FromString(string v) {

-      try {

-        return new BigNum(BIM.Parse(v));

-      } catch (System.ArgumentException) {

-        throw new FormatException();

-      }

-    }

-

-    public static bool TryParse(string v, out BigNum res) {

-      try {

-        res = BigNum.FromString(v);

-        return true;

-      } catch (FormatException) {

-        res = ZERO;

-        return false;

-      }

-    }

-

-    // Convert to int, without checking whether overflows occur

-    public int ToInt {

-      get {

-        return (int)val;

-      }

-    }

-

-    public BIM ToBigInteger {

-      get {

-        return val;

-      }

-    }

-

-    // Convert to int; assert that no overflows occur

-    public int ToIntSafe {

-      get {

-        Contract.Assert(this.InInt32);

-        return this.ToInt;

-      }

-    }

-

-    public Rational ToRational {

-      get {

-        return Rational.FromBignum(this);

-      }

-    }

-

-    public byte[] ToByteArray()

-    {

-      return this.val.ToByteArray();

-    }

-

-    internal BigNum(System.Numerics.BigInteger val) {

-      this.val = val;

-    }

-

-    public static bool operator ==(BigNum x, BigNum y) {

-      return (x.val == y.val);

-    }

-

-    public static bool operator !=(BigNum x, BigNum y) {

-      return !(x.val == y.val);

-    }

-

-    [Pure]

-    [Reads(ReadsAttribute.Reads.Nothing)]

-    public override bool Equals(object obj) {

-      if (obj == null)

-        return false;

-      if (!(obj is BigNum))

-        return false;

-

-      BigNum other = (BigNum)obj;

-      return (this.val == other.val);

-    }

-

-    [Pure]

-    public override int GetHashCode() {

-      return this.val.GetHashCode();

-    }

-

-    [Pure]

-    public override string/*!*/ ToString() {

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

-      return cce.NonNull(val.ToString());

-    }

-

-    //////////////////////////////////////////////////////////////////////////////

-    // Very limited support for format strings

-    // Note: Negative integers are linearised with a minus "-" in hexadecimal,

-    // not in 2-complement notation (in contrast to what the method

-    // int32.ToString(format) does) 

-

-    [Pure]

-    public string/*!*/ ToString(string/*!*/ format) {

-      Contract.Requires(format != null);

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

-      if (format.StartsWith("d") || format.StartsWith("D")) {

-        string res = this.Abs.ToString();

-        Contract.Assert(res != null);

-        return addMinus(this.Signum,

-                              prefixWithZeros(extractPrecision(format), res));

-      } else if (format.StartsWith("x") || format.StartsWith("X")) {

-        string res = this.toHex(format.Substring(0, 1));

-        Contract.Assert(res != null);

-        return addMinus(this.Signum,

-                              prefixWithZeros(extractPrecision(format), res));

-      } else {

-        throw new FormatException("Format " + format + " is not supported");

-      }

-    }

-

-    private static readonly System.Numerics.BigInteger BI_2_TO_24 = new BIM(0x1000000);

-

-    [Pure]

-    private string/*!*/ toHex(string/*!*/ format) {

-      Contract.Requires(format != null);

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

-      string res = "";

-      System.Numerics.BigInteger rem = this.Abs.val;

-

-      while (rem > BIM.Zero) {

-        res = ((int)(rem % BI_2_TO_24)).ToString(format) + res;

-        rem = rem / BI_2_TO_24;

-      }

-

-      return res;

-    }

-

-    [Pure]

-    private int extractPrecision(string/*!*/ format) {

-      Contract.Requires(format != null);

-      if (format.Length > 1)

-        // will throw a FormatException if the precision is invalid;

-        // that is ok

-        return Int32.Parse(format.Substring(1));

-      // always output at least one digit

-      return 1;

-    }

-

-    [Pure]

-    private string/*!*/ addMinus(int signum, string/*!*/ suffix) {

-      Contract.Requires(suffix != null);

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

-      if (signum < 0)

-        return "-" + suffix;

-      return suffix;

-    }

-

-    [Pure]

-    private string/*!*/ prefixWithZeros(int minLength, string/*!*/ suffix) {

-      Contract.Requires(suffix != null);

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

-      StringBuilder res = new StringBuilder();

-      while (res.Length + suffix.Length < minLength)

-        res.Append("0");

-      res.Append(suffix);

-      return res.ToString();

-    }

-

-    ////////////////////////////////////////////////////////////////////////////

-    // Basic arithmetic operations

-

-    public BigNum Abs {

-      get {

-        return new BigNum(BIM.Abs(this.val));

-      }

-    }

-

-    public BigNum Neg {

-      get {

-        return new BigNum(-this.val);

-      }

-    }

-

-    [Pure]

-    public static BigNum operator -(BigNum x) {

-      return x.Neg;

-    }

-

-    [Pure]

-    public static BigNum operator +(BigNum x, BigNum y) {

-      return new BigNum(x.val + y.val);

-    }

-

-    [Pure]

-    public static BigNum operator -(BigNum x, BigNum y) {

-      return new BigNum(x.val - y.val);

-    }

-

-    [Pure]

-    public static BigNum operator *(BigNum x, BigNum y) {

-      return new BigNum(x.val * y.val);

-    }

-

-    // TODO: check that this has a proper semantics (which? :-))

-    [Pure]

-    public static BigNum operator /(BigNum x, BigNum y) {

-      return new BigNum(x.val / y.val);

-    }

-

-    // TODO: check that this has a proper semantics (which? :-))

-    [Pure]

-    public static BigNum operator %(BigNum x, BigNum y) {

-      return new BigNum(x.val - ((x.val / y.val) * y.val));

-    }

-

-    [Pure]

-    public BigNum Min(BigNum that) {

-      return new BigNum(this.val <= that.val ? this.val : that.val);

-    }

-

-    [Pure]

-    public BigNum Max(BigNum that) {

-      return new BigNum(this.val >= that.val ? this.val : that.val);

-    }

-

-    /// <summary>

-    /// Returns the greatest common divisor of this and _y.

-    /// </summary>

-    /// <param name="_y"></param>

-    /// <returns></returns>

-    public BigNum Gcd(BigNum _y) {

-      Contract.Ensures(!Contract.Result<BigNum>().IsNegative);

-      BigNum x = this.Abs;

-      BigNum y = _y.Abs;

-

-      while (true) {

-        if (x < y) {

-          y = y % x;

-          if (y.IsZero) {

-            return x;

-          }

-        } else {

-          x = x % y;

-          if (x.IsZero) {

-            return y;

-          }

-        }

-      }

-    }

-

-    ////////////////////////////////////////////////////////////////////////////

-    // Some basic comparison operations

-

-    public int Signum {

-      get {

-        return this.val.Sign;

-      }

-    }

-

-    public bool IsPositive {

-      get {

-        return (this.val > BIM.Zero);

-      }

-    }

-

-    public bool IsNegative {

-      get {

-        return (this.val < BIM.Zero);

-      }

-    }

-

-    public bool IsZero {

-      get {

-        return this.val.IsZero;

-      }

-    }

-

-    [Pure]

-    public int CompareTo(BigNum that) {

-      if (this.val == that.val)

-        return 0;

-      if (this.val < that.val)

-        return -1;

-      return 1;

-    }

-

-    [Pure]

-    public static bool operator <(BigNum x, BigNum y) {

-      return (x.val < y.val);

-    }

-

-    [Pure]

-    public static bool operator >(BigNum x, BigNum y) {

-      return (x.val > y.val);

-    }

-

-    [Pure]

-    public static bool operator <=(BigNum x, BigNum y) {

-      return (x.val <= y.val);

-    }

-

-    [Pure]

-    public static bool operator >=(BigNum x, BigNum y) {

-      return (x.val >= y.val);

-    }

-

-

-    private static readonly System.Numerics.BigInteger MaxInt32 =

-      new BIM(Int32.MaxValue);

-    private static readonly System.Numerics.BigInteger MinInt32 =

-      new BIM(Int32.MinValue);

-

-    public bool InInt32 {

-      get {

-        return (val >= MinInt32) && (val <= MaxInt32);

-      }

-    }

-  }

-}

+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Text;
+using System.Diagnostics.Contracts;
+
+
+namespace Microsoft.Basetypes {
+  using BIM = System.Numerics.BigInteger;
+
+  /// <summary>
+  /// A thin wrapper around System.Numerics.BigInteger
+  /// (to be able to define equality, etc. properly)
+  /// </summary>
+  public struct BigNum {
+
+    // the internal representation
+    [Rep]
+    internal readonly System.Numerics.BigInteger val;
+    public static readonly BigNum ZERO = new BigNum(BIM.Zero);
+    public static readonly BigNum ONE = new BigNum(BIM.One);
+    public static readonly BigNum MINUS_ONE = new BigNum(-BIM.One);
+
+    [Pure]
+    public static BigNum FromInt(int v) {
+      return new BigNum(new BIM(v));
+    }
+
+    [Pure]
+    public static BigNum FromUInt(uint v) {
+      return new BigNum(new BIM((long)v));
+    }
+
+    [Pure]
+    public static BigNum FromLong(long v) {
+      return new BigNum(new BIM(v));
+    }
+
+    [Pure]
+    public static BigNum FromBigInt(System.Numerics.BigInteger v) {
+      return new BigNum(v);
+    }
+
+    [Pure]
+    public static BigNum FromULong(ulong v) {
+      return FromString("" + v);
+    }
+
+    [Pure]
+    public static BigNum FromString(string v) {
+      try {
+        return new BigNum(BIM.Parse(v));
+      } catch (System.ArgumentException) {
+        throw new FormatException();
+      }
+    }
+
+    public static bool TryParse(string v, out BigNum res) {
+      try {
+        res = BigNum.FromString(v);
+        return true;
+      } catch (FormatException) {
+        res = ZERO;
+        return false;
+      }
+    }
+
+    // Convert to int, without checking whether overflows occur
+    public int ToInt {
+      get {
+        return (int)val;
+      }
+    }
+
+    public BIM ToBigInteger {
+      get {
+        return val;
+      }
+    }
+
+    // Convert to int; assert that no overflows occur
+    public int ToIntSafe {
+      get {
+        Contract.Assert(this.InInt32);
+        return this.ToInt;
+      }
+    }
+
+    public Rational ToRational {
+      get {
+        return Rational.FromBignum(this);
+      }
+    }
+
+    public byte[] ToByteArray()
+    {
+      return this.val.ToByteArray();
+    }
+
+    internal BigNum(System.Numerics.BigInteger val) {
+      this.val = val;
+    }
+
+    public static bool operator ==(BigNum x, BigNum y) {
+      return (x.val == y.val);
+    }
+
+    public static bool operator !=(BigNum x, BigNum y) {
+      return !(x.val == y.val);
+    }
+
+    [Pure]
+    [Reads(ReadsAttribute.Reads.Nothing)]
+    public override bool Equals(object obj) {
+      if (obj == null)
+        return false;
+      if (!(obj is BigNum))
+        return false;
+
+      BigNum other = (BigNum)obj;
+      return (this.val == other.val);
+    }
+
+    [Pure]
+    public override int GetHashCode() {
+      return this.val.GetHashCode();
+    }
+
+    [Pure]
+    public override string/*!*/ ToString() {
+      Contract.Ensures(Contract.Result<string>() != null);
+      return cce.NonNull(val.ToString());
+    }
+
+    //////////////////////////////////////////////////////////////////////////////
+    // Very limited support for format strings
+    // Note: Negative integers are linearised with a minus "-" in hexadecimal,
+    // not in 2-complement notation (in contrast to what the method
+    // int32.ToString(format) does) 
+
+    [Pure]
+    public string/*!*/ ToString(string/*!*/ format) {
+      Contract.Requires(format != null);
+      Contract.Ensures(Contract.Result<string>() != null);
+      if (format.StartsWith("d") || format.StartsWith("D")) {
+        string res = this.Abs.ToString();
+        Contract.Assert(res != null);
+        return addMinus(this.Signum,
+                              prefixWithZeros(extractPrecision(format), res));
+      } else if (format.StartsWith("x") || format.StartsWith("X")) {
+        string res = this.toHex(format.Substring(0, 1));
+        Contract.Assert(res != null);
+        return addMinus(this.Signum,
+                              prefixWithZeros(extractPrecision(format), res));
+      } else {
+        throw new FormatException("Format " + format + " is not supported");
+      }
+    }
+
+    private static readonly System.Numerics.BigInteger BI_2_TO_24 = new BIM(0x1000000);
+
+    [Pure]
+    private string/*!*/ toHex(string/*!*/ format) {
+      Contract.Requires(format != null);
+      Contract.Ensures(Contract.Result<string>() != null);
+      string res = "";
+      System.Numerics.BigInteger rem = this.Abs.val;
+
+      while (rem > BIM.Zero) {
+        res = ((int)(rem % BI_2_TO_24)).ToString(format) + res;
+        rem = rem / BI_2_TO_24;
+      }
+
+      return res;
+    }
+
+    [Pure]
+    private int extractPrecision(string/*!*/ format) {
+      Contract.Requires(format != null);
+      if (format.Length > 1)
+        // will throw a FormatException if the precision is invalid;
+        // that is ok
+        return Int32.Parse(format.Substring(1));
+      // always output at least one digit
+      return 1;
+    }
+
+    [Pure]
+    private string/*!*/ addMinus(int signum, string/*!*/ suffix) {
+      Contract.Requires(suffix != null);
+      Contract.Ensures(Contract.Result<string>() != null);
+      if (signum < 0)
+        return "-" + suffix;
+      return suffix;
+    }
+
+    [Pure]
+    private string/*!*/ prefixWithZeros(int minLength, string/*!*/ suffix) {
+      Contract.Requires(suffix != null);
+      Contract.Ensures(Contract.Result<string>() != null);
+      StringBuilder res = new StringBuilder();
+      while (res.Length + suffix.Length < minLength)
+        res.Append("0");
+      res.Append(suffix);
+      return res.ToString();
+    }
+
+    ////////////////////////////////////////////////////////////////////////////
+    // Basic arithmetic operations
+
+    public BigNum Abs {
+      get {
+        return new BigNum(BIM.Abs(this.val));
+      }
+    }
+
+    public BigNum Neg {
+      get {
+        return new BigNum(-this.val);
+      }
+    }
+
+    [Pure]
+    public static BigNum operator -(BigNum x) {
+      return x.Neg;
+    }
+
+    [Pure]
+    public static BigNum operator +(BigNum x, BigNum y) {
+      return new BigNum(x.val + y.val);
+    }
+
+    [Pure]
+    public static BigNum operator -(BigNum x, BigNum y) {
+      return new BigNum(x.val - y.val);
+    }
+
+    [Pure]
+    public static BigNum operator *(BigNum x, BigNum y) {
+      return new BigNum(x.val * y.val);
+    }
+
+    // TODO: check that this has a proper semantics (which? :-))
+    [Pure]
+    public static BigNum operator /(BigNum x, BigNum y) {
+      return new BigNum(x.val / y.val);
+    }
+
+    // TODO: check that this has a proper semantics (which? :-))
+    [Pure]
+    public static BigNum operator %(BigNum x, BigNum y) {
+      return new BigNum(x.val - ((x.val / y.val) * y.val));
+    }
+
+    [Pure]
+    public BigNum Min(BigNum that) {
+      return new BigNum(this.val <= that.val ? this.val : that.val);
+    }
+
+    [Pure]
+    public BigNum Max(BigNum that) {
+      return new BigNum(this.val >= that.val ? this.val : that.val);
+    }
+
+    /// <summary>
+    /// Returns the greatest common divisor of this and _y.
+    /// </summary>
+    /// <param name="_y"></param>
+    /// <returns></returns>
+    public BigNum Gcd(BigNum _y) {
+      Contract.Ensures(!Contract.Result<BigNum>().IsNegative);
+      BigNum x = this.Abs;
+      BigNum y = _y.Abs;
+
+      while (true) {
+        if (x < y) {
+          y = y % x;
+          if (y.IsZero) {
+            return x;
+          }
+        } else {
+          x = x % y;
+          if (x.IsZero) {
+            return y;
+          }
+        }
+      }
+    }
+
+    ////////////////////////////////////////////////////////////////////////////
+    // Some basic comparison operations
+
+    public int Signum {
+      get {
+        return this.val.Sign;
+      }
+    }
+
+    public bool IsPositive {
+      get {
+        return (this.val > BIM.Zero);
+      }
+    }
+
+    public bool IsNegative {
+      get {
+        return (this.val < BIM.Zero);
+      }
+    }
+
+    public bool IsZero {
+      get {
+        return this.val.IsZero;
+      }
+    }
+
+    [Pure]
+    public int CompareTo(BigNum that) {
+      if (this.val == that.val)
+        return 0;
+      if (this.val < that.val)
+        return -1;
+      return 1;
+    }
+
+    [Pure]
+    public static bool operator <(BigNum x, BigNum y) {
+      return (x.val < y.val);
+    }
+
+    [Pure]
+    public static bool operator >(BigNum x, BigNum y) {
+      return (x.val > y.val);
+    }
+
+    [Pure]
+    public static bool operator <=(BigNum x, BigNum y) {
+      return (x.val <= y.val);
+    }
+
+    [Pure]
+    public static bool operator >=(BigNum x, BigNum y) {
+      return (x.val >= y.val);
+    }
+
+
+    private static readonly System.Numerics.BigInteger MaxInt32 =
+      new BIM(Int32.MaxValue);
+    private static readonly System.Numerics.BigInteger MinInt32 =
+      new BIM(Int32.MinValue);
+
+    public bool InInt32 {
+      get {
+        return (val >= MinInt32) && (val <= MaxInt32);
+      }
+    }
+  }
+}
diff --git a/Source/Basetypes/Rational.cs b/Source/Basetypes/Rational.cs
index cd0eddce..ef59cf4f 100644
--- a/Source/Basetypes/Rational.cs
+++ b/Source/Basetypes/Rational.cs
@@ -1,248 +1,248 @@
-//-----------------------------------------------------------------------------

-//

-// Copyright (C) Microsoft Corporation.  All Rights Reserved.

-//

-//-----------------------------------------------------------------------------

-using System;

-using System.Diagnostics.Contracts;

-

-namespace Microsoft.Basetypes {

-  /// <summary>

-  /// The representation of a rational number.

-  /// </summary>

-  public struct Rational {

-    public static readonly Rational ZERO = Rational.FromInts(0, 1);

-    public static readonly Rational ONE = Rational.FromInts(1, 1);

-    public static readonly Rational MINUS_ONE = Rational.FromInts(-1, 1);

-

-    private BigNum numerator, denominator;

-

-    //    int numerator;

-    //    int denominator;

-

-

-    // invariant: 0 < denominator || (numerator == 0 && denominator == 0);

-    // invariant: numerator != 0 ==> gcd(abs(numerator),denominator) == 1;

-    // invariant: numerator == 0 ==> denominator == 1 || denominator == 0;

-

-    public static Rational FromInt(int x) {

-      return FromBignum(BigNum.FromInt(x));

-    }

-

-    public static Rational FromBignum(BigNum n)       

-    {

-      return new Rational(n, BigNum.ONE);

-    }

-

-    private Rational(BigNum num, BigNum den)

-    {

-      Contract.Assert(den.Signum > 0);

-      Contract.Assert(num == BigNum.ZERO || num.Gcd(den) == BigNum.ONE);

-      numerator = num;

-      denominator = den;

-    }

-

-    public static Rational FromBignums(BigNum num, BigNum den) {

-      Contract.Assert(!den.IsZero);

-      if (num == BigNum.ZERO)

-        return ZERO;

-      if (den.Signum < 0) {

-        den = -den;

-        num = -num;

-      }

-      if (den == BigNum.ONE)

-        return new Rational(num, den);

-      var gcd = num.Gcd(den);

-      if (gcd == BigNum.ONE)

-        return new Rational(num, den);

-      return new Rational(num / gcd, den / gcd);

-    }

-

-    public static Rational FromInts(int num, int den) {

-      return FromBignums(BigNum.FromInt(num), BigNum.FromInt(den));

-    }

-

-    /// <summary>

-    /// Returns the absolute value of the rational.

-    /// </summary>

-    public Rational Abs() {

-      Contract.Ensures(Contract.Result<Rational>().IsNonNegative);

-      if (IsNonNegative) {

-        return this;

-      } else {

-        return -this;

-      }

-    }

-

-    /// <summary>

-    /// Returns a rational whose numerator and denominator, resepctively, are the Gcd

-    /// of the numerators and denominators of r and s.  If one of r and s is 0, the absolute

-    /// value of the other is returned.  If both are 0, 1 is returned.

-    /// </summary>

-    public static Rational Gcd(Rational r, Rational s) {

-      Contract.Ensures(Contract.Result<Rational>().IsPositive);

-      if (r.IsZero) {

-        if (s.IsZero) {

-          return ONE;

-        } else {

-          return s.Abs();

-        }

-      } else if (s.IsZero) {

-        return r.Abs();

-      } else {

-        return new Rational(r.Numerator.Gcd(s.Numerator),

-                             r.Denominator.Gcd(s.Denominator));

-      }

-    }

-

-    public BigNum Numerator { get { return numerator; } }

-    public BigNum Denominator { get { return denominator == BigNum.ZERO ? BigNum.ONE : denominator; } }

-

-    public override string/*!*/ ToString() {

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

-      return String.Format("{0}/{1}", Numerator, Denominator);

-    }

-

-

-    public static bool operator ==(Rational r, Rational s) {

-      return r.Numerator == s.Numerator && r.Denominator == s.Denominator;

-    }

-

-    public static bool operator !=(Rational r, Rational s) {

-      return !(r == s);

-    }

-

-    public override bool Equals(object obj) {

-      if (obj == null)

-        return false;

-      return obj is Rational && (Rational)obj == this;

-    }

-

-    public override int GetHashCode() {

-      return this.Numerator.GetHashCode() * 13 + this.Denominator.GetHashCode();

-    }

-

-    public int Signum {

-      get {

-        return this.Numerator.Signum;

-      }

-    }

-

-    public bool IsZero {

-      get {

-        return Signum == 0;

-      }

-    }

-

-    public bool IsNonZero {

-      get {

-        return Signum != 0;

-      }

-    }

-

-    public bool IsIntegral {

-      get {

-        return Denominator == BigNum.ONE;

-      }

-    }

-

-

-    [Pure]

-    [Reads(ReadsAttribute.Reads.Nothing)]

-    public bool HasValue(int n) {

-      return this == FromInt(n);

-    }

-

-    /// <summary>

-    /// Returns the rational as an integer.  Requires the rational to be integral.

-    /// </summary>

-    public int AsInteger {

-      get {

-        Contract.Assert(this.IsIntegral);

-        return Numerator.ToIntSafe;

-      }

-    }

-

-    public BigNum AsBigNum {

-      get {

-        Contract.Assert(this.IsIntegral);

-        return Numerator;

-      }

-    }

-

-    public double AsDouble {

-      [Pure]

-      get {

-        if (this.IsZero) {

-          return 0.0;

-        } else {

-          return (double)Numerator.ToIntSafe / (double)Denominator.ToIntSafe;

-        }

-      }

-    }

-

-    public bool IsNegative {

-      [Pure]

-      get {

-        return Signum < 0;

-      }

-    }

-

-    public bool IsPositive {

-      [Pure]

-      get {

-        return 0 < Signum;

-      }

-    }

-

-    public bool IsNonNegative {

-      [Pure]

-      get {

-        return 0 <= Signum;

-      }

-    }

-

-    public static Rational operator -(Rational r)

-    {

-      return new Rational(-r.Numerator, r.Denominator);

-    }

-

-    public static Rational operator /(Rational r, Rational s)

-    {

-      return FromBignums(r.Numerator * s.Denominator, r.Denominator * s.Numerator);

-    }

-

-    public static Rational operator -(Rational r, Rational s)

-    {

-      return r + (-s);

-    }

-

-    public static Rational operator +(Rational r, Rational s)

-    {

-      return FromBignums(r.Numerator * s.Denominator + s.Numerator * r.Denominator, r.Denominator * s.Denominator);

-    }

-

-    public static Rational operator *(Rational r, Rational s)

-    {

-      return FromBignums(r.Numerator * s.Numerator, r.Denominator * s.Denominator);

-    }

-

-    public static bool operator <(Rational r, Rational s)

-    {

-      return (r - s).Signum < 0;

-    }

-

-    public static bool operator <=(Rational r, Rational s)

-    {

-      return !(r > s);

-    }

-

-    public static bool operator >=(Rational r, Rational s) {

-      return !(r < s);

-    }

-

-    public static bool operator >(Rational r, Rational s) {

-      return s < r;

-    }

-  }

-}

+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+using System;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Basetypes {
+  /// <summary>
+  /// The representation of a rational number.
+  /// </summary>
+  public struct Rational {
+    public static readonly Rational ZERO = Rational.FromInts(0, 1);
+    public static readonly Rational ONE = Rational.FromInts(1, 1);
+    public static readonly Rational MINUS_ONE = Rational.FromInts(-1, 1);
+
+    private BigNum numerator, denominator;
+
+    //    int numerator;
+    //    int denominator;
+
+
+    // invariant: 0 < denominator || (numerator == 0 && denominator == 0);
+    // invariant: numerator != 0 ==> gcd(abs(numerator),denominator) == 1;
+    // invariant: numerator == 0 ==> denominator == 1 || denominator == 0;
+
+    public static Rational FromInt(int x) {
+      return FromBignum(BigNum.FromInt(x));
+    }
+
+    public static Rational FromBignum(BigNum n)       
+    {
+      return new Rational(n, BigNum.ONE);
+    }
+
+    private Rational(BigNum num, BigNum den)
+    {
+      Contract.Assert(den.Signum > 0);
+      Contract.Assert(num == BigNum.ZERO || num.Gcd(den) == BigNum.ONE);
+      numerator = num;
+      denominator = den;
+    }
+
+    public static Rational FromBignums(BigNum num, BigNum den) {
+      Contract.Assert(!den.IsZero);
+      if (num == BigNum.ZERO)
+        return ZERO;
+      if (den.Signum < 0) {
+        den = -den;
+        num = -num;
+      }
+      if (den == BigNum.ONE)
+        return new Rational(num, den);
+      var gcd = num.Gcd(den);
+      if (gcd == BigNum.ONE)
+        return new Rational(num, den);
+      return new Rational(num / gcd, den / gcd);
+    }
+
+    public static Rational FromInts(int num, int den) {
+      return FromBignums(BigNum.FromInt(num), BigNum.FromInt(den));
+    }
+
+    /// <summary>
+    /// Returns the absolute value of the rational.
+    /// </summary>
+    public Rational Abs() {
+      Contract.Ensures(Contract.Result<Rational>().IsNonNegative);
+      if (IsNonNegative) {
+        return this;
+      } else {
+        return -this;
+      }
+    }
+
+    /// <summary>
+    /// Returns a rational whose numerator and denominator, resepctively, are the Gcd
+    /// of the numerators and denominators of r and s.  If one of r and s is 0, the absolute
+    /// value of the other is returned.  If both are 0, 1 is returned.
+    /// </summary>
+    public static Rational Gcd(Rational r, Rational s) {
+      Contract.Ensures(Contract.Result<Rational>().IsPositive);
+      if (r.IsZero) {
+        if (s.IsZero) {
+          return ONE;
+        } else {
+          return s.Abs();
+        }
+      } else if (s.IsZero) {
+        return r.Abs();
+      } else {
+        return new Rational(r.Numerator.Gcd(s.Numerator),
+                             r.Denominator.Gcd(s.Denominator));
+      }
+    }
+
+    public BigNum Numerator { get { return numerator; } }
+    public BigNum Denominator { get { return denominator == BigNum.ZERO ? BigNum.ONE : denominator; } }
+
+    public override string/*!*/ ToString() {
+      Contract.Ensures(Contract.Result<string>() != null);
+      return String.Format("{0}/{1}", Numerator, Denominator);
+    }
+
+
+    public static bool operator ==(Rational r, Rational s) {
+      return r.Numerator == s.Numerator && r.Denominator == s.Denominator;
+    }
+
+    public static bool operator !=(Rational r, Rational s) {
+      return !(r == s);
+    }
+
+    public override bool Equals(object obj) {
+      if (obj == null)
+        return false;
+      return obj is Rational && (Rational)obj == this;
+    }
+
+    public override int GetHashCode() {
+      return this.Numerator.GetHashCode() * 13 + this.Denominator.GetHashCode();
+    }
+
+    public int Signum {
+      get {
+        return this.Numerator.Signum;
+      }
+    }
+
+    public bool IsZero {
+      get {
+        return Signum == 0;
+      }
+    }
+
+    public bool IsNonZero {
+      get {
+        return Signum != 0;
+      }
+    }
+
+    public bool IsIntegral {
+      get {
+        return Denominator == BigNum.ONE;
+      }
+    }
+
+
+    [Pure]
+    [Reads(ReadsAttribute.Reads.Nothing)]
+    public bool HasValue(int n) {
+      return this == FromInt(n);
+    }
+
+    /// <summary>
+    /// Returns the rational as an integer.  Requires the rational to be integral.
+    /// </summary>
+    public int AsInteger {
+      get {
+        Contract.Assert(this.IsIntegral);
+        return Numerator.ToIntSafe;
+      }
+    }
+
+    public BigNum AsBigNum {
+      get {
+        Contract.Assert(this.IsIntegral);
+        return Numerator;
+      }
+    }
+
+    public double AsDouble {
+      [Pure]
+      get {
+        if (this.IsZero) {
+          return 0.0;
+        } else {
+          return (double)Numerator.ToIntSafe / (double)Denominator.ToIntSafe;
+        }
+      }
+    }
+
+    public bool IsNegative {
+      [Pure]
+      get {
+        return Signum < 0;
+      }
+    }
+
+    public bool IsPositive {
+      [Pure]
+      get {
+        return 0 < Signum;
+      }
+    }
+
+    public bool IsNonNegative {
+      [Pure]
+      get {
+        return 0 <= Signum;
+      }
+    }
+
+    public static Rational operator -(Rational r)
+    {
+      return new Rational(-r.Numerator, r.Denominator);
+    }
+
+    public static Rational operator /(Rational r, Rational s)
+    {
+      return FromBignums(r.Numerator * s.Denominator, r.Denominator * s.Numerator);
+    }
+
+    public static Rational operator -(Rational r, Rational s)
+    {
+      return r + (-s);
+    }
+
+    public static Rational operator +(Rational r, Rational s)
+    {
+      return FromBignums(r.Numerator * s.Denominator + s.Numerator * r.Denominator, r.Denominator * s.Denominator);
+    }
+
+    public static Rational operator *(Rational r, Rational s)
+    {
+      return FromBignums(r.Numerator * s.Numerator, r.Denominator * s.Denominator);
+    }
+
+    public static bool operator <(Rational r, Rational s)
+    {
+      return (r - s).Signum < 0;
+    }
+
+    public static bool operator <=(Rational r, Rational s)
+    {
+      return !(r > s);
+    }
+
+    public static bool operator >=(Rational r, Rational s) {
+      return !(r < s);
+    }
+
+    public static bool operator >(Rational r, Rational s) {
+      return s < r;
+    }
+  }
+}
diff --git a/Source/Basetypes/Set.cs b/Source/Basetypes/Set.cs
index dfd65b4b..0cc1d103 100644
--- a/Source/Basetypes/Set.cs
+++ b/Source/Basetypes/Set.cs
@@ -1,286 +1,286 @@
-//-----------------------------------------------------------------------------

-//

-// Copyright (C) Microsoft Corporation.  All Rights Reserved.

-//

-//-----------------------------------------------------------------------------

-namespace Microsoft.Boogie {

-  using System;

-  using System.IO;

-  using System.Collections;

-  using System.Collections.Generic;

-  using System.Diagnostics.Contracts;

-

-  /// <summary>

-  /// A class representing a mathematical set.

-  /// </summary>

-  public class GSet<T> : ICloneable, IEnumerable, IEnumerable<T> {

-    /*[Own]*/

-    Dictionary<T, int> ht;

-    List<T> arr; // keep elements in a well-defined order; otherwise iteration is non-deterministic

-

-    [ContractInvariantMethod]

-    void ObjectInvariant() {

-      Contract.Invariant(ht != null);

-      Contract.Invariant(arr != null);

-      Contract.Invariant(ht.Count == arr.Count);

-    }

-

-

-    public GSet() {

-      ht = new Dictionary<T, int>();

-      arr = new List<T>();

-      //:base();

-    }

-

-    private GSet(Dictionary<T,int>/*!*/ ht, List<T> arr) {

-      Contract.Requires(ht != null);

-      Contract.Requires(arr != null);

-      this.ht = ht;

-      this.arr = arr;

-      //:base();

-    }

-

-    public GSet(int capacity) {

-      ht = new Dictionary<T, int>(capacity);

-      arr = new List<T>(capacity);

-      //:base();

-    }

-

-

-    public readonly static GSet<T>/*!*/ Empty = new GSet<T>();

-

-    public void Clear() {

-      ht.Clear();

-      arr.Clear();

-    }

-

-    /// <summary>

-    /// This method idempotently adds "o" to the set.

-    /// In notation:

-    ///   this.SetElements =  this.SetElements_old \union {o};

-    /// </summary>

-    public void Add(T o) {

-      if (!ht.ContainsKey(o)) {

-        ht[o] = arr.Count;

-        arr.Add(o);

-      }

-    }

-

-    /// <summary>

-    /// this.SetElements =  this.SetElements_old \union s.GSet<T>Elements;

-    /// </summary>

-    public void AddRange(IEnumerable<T> s) {

-      foreach (T o in s) {

-        Add(o);

-      }

-    }

-

-    /// <summary>

-    /// this.SetElements =  this.SetElements_old \setminus {o};

-    /// </summary>

-    public void Remove(T o) {

-      int idx;

-      if (ht.TryGetValue(o, out idx)) {

-        var last = arr[arr.Count - 1];

-        arr.RemoveAt(arr.Count - 1);

-        if (idx != arr.Count) {

-          arr[idx] = last;

-          ht[last] = idx;

-        }

-        ht.Remove(o);

-      }

-    }

-

-    /// <summary>

-    /// this.SetElements =  this.SetElements_old \setminus s.SetElements;

-    /// </summary>

-    public void RemoveRange(IEnumerable<T> s) {

-      Contract.Requires(s != null);

-      if (s == this) {

-        ht.Clear();

-        arr.Clear();

-      } else {

-        foreach (T o in s) {

-          Remove(o);

-        }

-      }

-    }

-

-    /// <summary>

-    /// Returns an arbitrary element from the set.

-    /// </summary>

-    public T Choose() {

-      Contract.Requires((Count > 0));

-      foreach(var e in this) 

-        return e;

-      return default(T);

-    }

-

-    /// <summary>

-    /// Picks an arbitrary element from the set, removes it, and returns it.

-    /// </summary>

-    public T Take() {

-      Contract.Requires((Count > 0));

-      Contract.Ensures(Count == Contract.OldValue(Count) - 1);

-      T r = Choose();

-      Remove(r);

-      return r;

-    }

-

-    public void Intersect(GSet<T>/*!*/ s) {

-      Contract.Requires(s != null);

-      if (s == this) return;

-      ht.Clear();

-      var newArr = new List<T>();

-      foreach (T key in arr) {

-        if (s.ht.ContainsKey(key)) {

-          ht[key] = newArr.Count;

-          newArr.Add(key);

-        }

-      }

-      arr = newArr;

-    }

-

-    /// <summary>

-    /// The getter returns true iff "o" is in the set.

-    /// The setter adds the value "o" (for "true") or removes "o" (for "false")

-    /// </summary>

-    public bool this[T o] {

-      get {

-        return ht.ContainsKey(o);

-      }

-      set {

-        if (value) {

-          Add(o);

-        } else {

-          Remove(o);

-        }

-      }

-    }

-

-    /// <summary>

-    /// Returns true iff "o" is an element of "this".

-    /// </summary>

-    /// <param name="o"></param>

-    /// <returns></returns>

-    [Pure]

-    public bool Contains(T o) {

-      return this.ht.ContainsKey(o);

-    }

-

-    /// <summary>

-    /// Returns true iff every element of "s" is an element of "this", that is, if

-    /// "s" is a subset of "this".

-    /// </summary>

-    /// <param name="s"></param>

-    /// <returns></returns>

-    public bool ContainsRange(IEnumerable<T> s) {

-      Contract.Requires(s != null);

-      if (s != this) {

-        foreach (T key in s) {

-          if (!this.ht.ContainsKey(key)) {

-            return false;

-          }

-        }

-      }

-      return true;

-    }

-

-    public object/*!*/ Clone() {

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

-      return new GSet<T>(new Dictionary<T,int>(ht), new List<T>(arr));

-    }

-

-    public virtual int Count {

-      get {

-        return ht.Count;

-      }

-    }

-

-    [Pure]

-    public override string/*!*/ ToString() {

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

-      string s = null;

-      foreach (object/*!*/ key in ht.Keys) {

-        Contract.Assert(key != null);

-        if (s == null) {

-          s = "{";

-        } else {

-          s += ", ";

-        }

-        s += key.ToString();

-      }

-      if (s == null) {

-        return "{}";

-      } else {

-        return s + "}";

-      }

-    }

-

-    //----------------------------- Static Methods ---------------------------------

-

-    // Functional Intersect

-    public static GSet<T>/*!*/ Intersect(GSet<T>/*!*/ a, GSet<T>/*!*/ b) {

-      Contract.Requires(b != null);

-      Contract.Requires(a != null);

-      Contract.Ensures(Contract.Result<GSet<T>>() != null);

-      //Contract.Ensures(Contract.ForAll(result, x => a[x] && b[x] ));

-      GSet<T>/*!*/ res = (GSet<T>/*!*/)cce.NonNull(a.Clone());

-      res.Intersect(b);

-      return res;

-    }

-    // Functional Union

-    public static GSet<T>/*!*/ Union(GSet<T>/*!*/ a, GSet<T>/*!*/ b) {

-      Contract.Requires(a != null);

-      Contract.Requires(b != null);

-      Contract.Ensures(Contract.Result<GSet<T>>() != null);

-      //  Contract.Ensures(Contract.ForAll(result, x => a[x] || b[x] ));

-      GSet<T>/*!*/ res = (GSet<T>/*!*/)cce.NonNull(a.Clone());

-      res.AddRange(b);

-      return res;

-    }

-

-    public delegate bool SetFilter(object/*!*/ obj);

-

-    public static GSet<T>/*!*/ Filter(GSet<T>/*!*/ a, Func<T,bool> filter) {

-      Contract.Requires(filter != null);

-      Contract.Requires(a != null);

-      Contract.Ensures(Contract.Result<GSet<T>>() != null);

-      GSet<T> inter = new GSet<T>();

-

-      foreach (T elem in a) {

-        Contract.Assert(elem != null);

-        if (filter(elem)) {

-          inter.Add(elem);

-        }

-      }

-      return inter;

-    }

-

-    public IEnumerator<T> GetEnumerator()

-    {

-      return arr.GetEnumerator();

-    }

-

-    IEnumerator IEnumerable.GetEnumerator()

-    {

-      return ((IEnumerable)arr).GetEnumerator();

-    }

-

-    public bool AddAll(IEnumerable s)

-    {

-      foreach (T e in s) Add(e);

-      return true;

-    }

-  }

-

-

-  public interface IWorkList : ICollection {

-    bool Add(object o);

-    bool AddAll(IEnumerable objs);

-    bool IsEmpty();

-    object Pull();

-  }

-

-

+//-----------------------------------------------------------------------------
+//
+// Copyright (C) Microsoft Corporation.  All Rights Reserved.
+//
+//-----------------------------------------------------------------------------
+namespace Microsoft.Boogie {
+  using System;
+  using System.IO;
+  using System.Collections;
+  using System.Collections.Generic;
+  using System.Diagnostics.Contracts;
+
+  /// <summary>
+  /// A class representing a mathematical set.
+  /// </summary>
+  public class GSet<T> : ICloneable, IEnumerable, IEnumerable<T> {
+    /*[Own]*/
+    Dictionary<T, int> ht;
+    List<T> arr; // keep elements in a well-defined order; otherwise iteration is non-deterministic
+
+    [ContractInvariantMethod]
+    void ObjectInvariant() {
+      Contract.Invariant(ht != null);
+      Contract.Invariant(arr != null);
+      Contract.Invariant(ht.Count == arr.Count);
+    }
+
+
+    public GSet() {
+      ht = new Dictionary<T, int>();
+      arr = new List<T>();
+      //:base();
+    }
+
+    private GSet(Dictionary<T,int>/*!*/ ht, List<T> arr) {
+      Contract.Requires(ht != null);
+      Contract.Requires(arr != null);
+      this.ht = ht;
+      this.arr = arr;
+      //:base();
+    }
+
+    public GSet(int capacity) {
+      ht = new Dictionary<T, int>(capacity);
+      arr = new List<T>(capacity);
+      //:base();
+    }
+
+
+    public readonly static GSet<T>/*!*/ Empty = new GSet<T>();
+
+    public void Clear() {
+      ht.Clear();
+      arr.Clear();
+    }
+
+    /// <summary>
+    /// This method idempotently adds "o" to the set.
+    /// In notation:
+    ///   this.SetElements =  this.SetElements_old \union {o};
+    /// </summary>
+    public void Add(T o) {
+      if (!ht.ContainsKey(o)) {
+        ht[o] = arr.Count;
+        arr.Add(o);
+      }
+    }
+
+    /// <summary>
+    /// this.SetElements =  this.SetElements_old \union s.GSet<T>Elements;
+    /// </summary>
+    public void AddRange(IEnumerable<T> s) {
+      foreach (T o in s) {
+        Add(o);
+      }
+    }
+
+    /// <summary>
+    /// this.SetElements =  this.SetElements_old \setminus {o};
+    /// </summary>
+    public void Remove(T o) {
+      int idx;
+      if (ht.TryGetValue(o, out idx)) {
+        var last = arr[arr.Count - 1];
+        arr.RemoveAt(arr.Count - 1);
+        if (idx != arr.Count) {
+          arr[idx] = last;
+          ht[last] = idx;
+        }
+        ht.Remove(o);
+      }
+    }
+
+    /// <summary>
+    /// this.SetElements =  this.SetElements_old \setminus s.SetElements;
+    /// </summary>
+    public void RemoveRange(IEnumerable<T> s) {
+      Contract.Requires(s != null);
+      if (s == this) {
+        ht.Clear();
+        arr.Clear();
+      } else {
+        foreach (T o in s) {
+          Remove(o);
+        }
+      }
+    }
+
+    /// <summary>
+    /// Returns an arbitrary element from the set.
+    /// </summary>
+    public T Choose() {
+      Contract.Requires((Count > 0));
+      foreach(var e in this) 
+        return e;
+      return default(T);
+    }
+
+    /// <summary>
+    /// Picks an arbitrary element from the set, removes it, and returns it.
+    /// </summary>
+    public T Take() {
+      Contract.Requires((Count > 0));
+      Contract.Ensures(Count == Contract.OldValue(Count) - 1);
+      T r = Choose();
+      Remove(r);
+      return r;
+    }
+
+    public void Intersect(GSet<T>/*!*/ s) {
+      Contract.Requires(s != null);
+      if (s == this) return;
+      ht.Clear();
+      var newArr = new List<T>();
+      foreach (T key in arr) {
+        if (s.ht.ContainsKey(key)) {
+          ht[key] = newArr.Count;
+          newArr.Add(key);
+        }
+      }
+      arr = newArr;
+    }
+
+    /// <summary>
+    /// The getter returns true iff "o" is in the set.
+    /// The setter adds the value "o" (for "true") or removes "o" (for "false")
+    /// </summary>
+    public bool this[T o] {
+      get {
+        return ht.ContainsKey(o);
+      }
+      set {
+        if (value) {
+          Add(o);
+        } else {
+          Remove(o);
+        }
+      }
+    }
+
+    /// <summary>
+    /// Returns true iff "o" is an element of "this".
+    /// </summary>
+    /// <param name="o"></param>
+    /// <returns></returns>
+    [Pure]
+    public bool Contains(T o) {
+      return this.ht.ContainsKey(o);
+    }
+
+    /// <summary>
+    /// Returns true iff every element of "s" is an element of "this", that is, if
+    /// "s" is a subset of "this".
+    /// </summary>
+    /// <param name="s"></param>
+    /// <returns></returns>
+    public bool ContainsRange(IEnumerable<T> s) {
+      Contract.Requires(s != null);
+      if (s != this) {
+        foreach (T key in s) {
+          if (!this.ht.ContainsKey(key)) {
+            return false;
+          }
+        }
+      }
+      return true;
+    }
+
+    public object/*!*/ Clone() {
+      Contract.Ensures(Contract.Result<object>() != null);
+      return new GSet<T>(new Dictionary<T,int>(ht), new List<T>(arr));
+    }
+
+    public virtual int Count {
+      get {
+        return ht.Count;
+      }
+    }
+
+    [Pure]
+    public override string/*!*/ ToString() {
+      Contract.Ensures(Contract.Result<string>() != null);
+      string s = null;
+      foreach (object/*!*/ key in ht.Keys) {
+        Contract.Assert(key != null);
+        if (s == null) {
+          s = "{";
+        } else {
+          s += ", ";
+        }
+        s += key.ToString();
+      }
+      if (s == null) {
+        return "{}";
+      } else {
+        return s + "}";
+      }
+    }
+
+    //----------------------------- Static Methods ---------------------------------
+
+    // Functional Intersect
+    public static GSet<T>/*!*/ Intersect(GSet<T>/*!*/ a, GSet<T>/*!*/ b) {
+      Contract.Requires(b != null);
+      Contract.Requires(a != null);
+      Contract.Ensures(Contract.Result<GSet<T>>() != null);
+      //Contract.Ensures(Contract.ForAll(result, x => a[x] && b[x] ));
+      GSet<T>/*!*/ res = (GSet<T>/*!*/)cce.NonNull(a.Clone());
+      res.Intersect(b);
+      return res;
+    }
+    // Functional Union
+    public static GSet<T>/*!*/ Union(GSet<T>/*!*/ a, GSet<T>/*!*/ b) {
+      Contract.Requires(a != null);
+      Contract.Requires(b != null);
+      Contract.Ensures(Contract.Result<GSet<T>>() != null);
+      //  Contract.Ensures(Contract.ForAll(result, x => a[x] || b[x] ));
+      GSet<T>/*!*/ res = (GSet<T>/*!*/)cce.NonNull(a.Clone());
+      res.AddRange(b);
+      return res;
+    }
+
+    public delegate bool SetFilter(object/*!*/ obj);
+
+    public static GSet<T>/*!*/ Filter(GSet<T>/*!*/ a, Func<T,bool> filter) {
+      Contract.Requires(filter != null);
+      Contract.Requires(a != null);
+      Contract.Ensures(Contract.Result<GSet<T>>() != null);
+      GSet<T> inter = new GSet<T>();
+
+      foreach (T elem in a) {
+        Contract.Assert(elem != null);
+        if (filter(elem)) {
+          inter.Add(elem);
+        }
+      }
+      return inter;
+    }
+
+    public IEnumerator<T> GetEnumerator()
+    {
+      return arr.GetEnumerator();
+    }
+
+    IEnumerator IEnumerable.GetEnumerator()
+    {
+      return ((IEnumerable)arr).GetEnumerator();
+    }
+
+    public bool AddAll(IEnumerable s)
+    {
+      foreach (T e in s) Add(e);
+      return true;
+    }
+  }
+
+
+  public interface IWorkList : ICollection {
+    bool Add(object o);
+    bool AddAll(IEnumerable objs);
+    bool IsEmpty();
+    object Pull();
+  }
+
+
 }
\ No newline at end of file
diff --git a/Source/Basetypes/cce.cs b/Source/Basetypes/cce.cs
index ef594484..1e0b12a5 100644
--- a/Source/Basetypes/cce.cs
+++ b/Source/Basetypes/cce.cs
@@ -1,193 +1,193 @@
-using System;

-using SA=System.Attribute;

-using System.Collections.Generic;

-using System.Diagnostics.Contracts;

-using System.Text;

-//using Microsoft.Boogie;

-

-/// <summary>

-/// A class containing static methods to extend the functionality of Code Contracts

-/// </summary>

-

-public static class cce {

-  //[Pure]

-  //public static bool NonNullElements<T>(Microsoft.Dafny.Graph<T> collection) {

-  //  return collection != null && cce.NonNullElements(collection.TopologicallySortedComponents());

-  //}

-  [Pure]

-  public static T NonNull<T>(T t) {

-    Contract.Assert(t != null);

-    return t;

-  }

-  [Pure]

-  public static bool NonNullElements<T>(IEnumerable<T> collection) {

-    return collection != null && Contract.ForAll(collection, c => c != null);

-  }

-  [Pure]

-  public static bool NonNullElements<TKey, TValue>(IDictionary<TKey, TValue> collection) {

-    return collection != null && Contract.ForAll(collection, pair => NonNullElements(pair));

-  }

-  //[Pure]

-  //public static bool NonNullElements(VariableSeq collection) {

-  //  return collection != null && Contract.ForAll(0, collection.Length, i => collection[i] != null);

-  //}

-  /// <summary>

-  /// For possibly-null lists of non-null elements

-  /// </summary>

-  /// <typeparam name="T"></typeparam>

-  /// <param name="collection"></param>

-  /// <param name="nullability">If true, the collection is treated as an IEnumerable&lt;T!&gt;?, rather than an IEnumerable&lt;T!&gt;!</param>

-  /// <returns></returns>

-  [Pure]

-  public static bool NonNullElements<T>(IEnumerable<T> collection, bool nullability) {

-    return (nullability && collection == null) || cce.NonNullElements(collection);

-    //Should be the same as:

-    /*if(nullability&&collection==null)

-     * return true;

-     * return cce.NonNullElements(collection)

-     */

-

-  }

-  [Pure]

-  public static bool NonNullElements<TKey, TValue>(KeyValuePair<TKey, TValue> kvp) {

-    return kvp.Key != null && kvp.Value != null;

-  }

-  [Pure]

-  public static bool NonNullElements<T>(IEnumerator<T> iEnumerator) {

-    return iEnumerator != null;

-  }

-  //[Pure]

-  //public static bool NonNullElements<T>(Graphing.Graph<T> graph) {

-  //  return cce.NonNullElements(graph.TopologicalSort());

-  //}

-  [Pure]

-  public static void BeginExpose(object o) {

-  }

-  [Pure]

-  public static void EndExpose() {

-  }

-  [Pure]

-  public static bool IsPeerConsistent(object o) {

-    return true;

-  }

-  [Pure]

-  public static bool IsConsistent(object o) {

-    return true;

-  }

-  [Pure]

-  public static bool IsExposable(object o) {

-    return true;

-  }

-  [Pure]

-  public static bool IsExposed(object o) {

-    return true;

-  }

-  [Pure]

-  public static bool IsNew(object o) {

-    return true;

-  }

-  public static class Owner {

-    [Pure]

-    public static bool Same(object o, object p) {

-      return true;

-    }

-    [Pure]

-    public static void AssignSame(object o, object p) {

-    }

-    [Pure]

-    public static object ElementProxy(object o) {

-      return o;

-    }

-    [Pure]

-    public static bool None(object o) {

-      return true;

-    }

-    [Pure]

-    public static bool Different(object o, object p) {

-      return true;

-    }

-    [Pure]

-    public static bool New(object o) {

-      return true;

-    }

-  }

-  [Pure]

-  public static void LoopInvariant(bool p) {

-    Contract.Assert(p);

-  }

-  public class UnreachableException : Exception {

-    public UnreachableException() {

-    }

-  }

-  //[Pure]

-  //public static bool IsValid(Microsoft.Dafny.Expression expression) {

-  //  return true;

-  //}

-  //public static List<T> toList<T>(PureCollections.Sequence s) {

-  //  List<T> toRet = new List<T>();

-  //  foreach (T t in s.elems)

-  //    if(t!=null)

-  //    toRet.Add(t);

-  //  return toRet;

-  //}

-

-  //internal static bool NonNullElements(Set set) {

-  //  return set != null && Contract.ForAll(0,set.Count, i => set[i] != null);

-  //}

-}

-

-public class PeerAttribute : SA {

-}

-public class RepAttribute : SA {

-}

-public class CapturedAttribute : SA {

-}

-public class NotDelayedAttribute : SA {

-}

-public class NoDefaultContractAttribute : SA {

-}

-public class VerifyAttribute : SA {

-  public VerifyAttribute(bool b) {

-

-  }

-}

-public class StrictReadonlyAttribute : SA {

-}

-public class AdditiveAttribute : SA {

-}

-public class ReadsAttribute : SA {

-  public enum Reads {

-    Nothing,

-    Everything,

-  };

-  public ReadsAttribute(object o) {

-  }

-}

-public class GlobalAccessAttribute : SA {

-  public GlobalAccessAttribute(bool b) {

-  }

-}

-public class EscapesAttribute : SA {

-  public EscapesAttribute(bool b, bool b_2) {

-  }

-}

-public class NeedsContractsAttribute : SA {

-  public NeedsContractsAttribute() {

-  }

-  public NeedsContractsAttribute(bool ret, bool parameters) {

-  }

-  public NeedsContractsAttribute(bool ret, int[] parameters) {

-  }

-}

-public class ImmutableAttribute : SA {

-}

-public class InsideAttribute : SA {

-}

-public class SpecPublicAttribute : SA {

-}

-public class ElementsPeerAttribute : SA {

-}

-public class ResultNotNewlyAllocatedAttribute : SA {

-}

-public class OnceAttribute : SA {

+using System;
+using SA=System.Attribute;
+using System.Collections.Generic;
+using System.Diagnostics.Contracts;
+using System.Text;
+//using Microsoft.Boogie;
+
+/// <summary>
+/// A class containing static methods to extend the functionality of Code Contracts
+/// </summary>
+
+public static class cce {
+  //[Pure]
+  //public static bool NonNullElements<T>(Microsoft.Dafny.Graph<T> collection) {
+  //  return collection != null && cce.NonNullElements(collection.TopologicallySortedComponents());
+  //}
+  [Pure]
+  public static T NonNull<T>(T t) {
+    Contract.Assert(t != null);
+    return t;
+  }
+  [Pure]
+  public static bool NonNullElements<T>(IEnumerable<T> collection) {
+    return collection != null && Contract.ForAll(collection, c => c != null);
+  }
+  [Pure]
+  public static bool NonNullElements<TKey, TValue>(IDictionary<TKey, TValue> collection) {
+    return collection != null && Contract.ForAll(collection, pair => NonNullElements(pair));
+  }
+  //[Pure]
+  //public static bool NonNullElements(VariableSeq collection) {
+  //  return collection != null && Contract.ForAll(0, collection.Length, i => collection[i] != null);
+  //}
+  /// <summary>
+  /// For possibly-null lists of non-null elements
+  /// </summary>
+  /// <typeparam name="T"></typeparam>
+  /// <param name="collection"></param>
+  /// <param name="nullability">If true, the collection is treated as an IEnumerable&lt;T!&gt;?, rather than an IEnumerable&lt;T!&gt;!</param>
+  /// <returns></returns>
+  [Pure]
+  public static bool NonNullElements<T>(IEnumerable<T> collection, bool nullability) {
+    return (nullability && collection == null) || cce.NonNullElements(collection);
+    //Should be the same as:
+    /*if(nullability&&collection==null)
+     * return true;
+     * return cce.NonNullElements(collection)
+     */
+
+  }
+  [Pure]
+  public static bool NonNullElements<TKey, TValue>(KeyValuePair<TKey, TValue> kvp) {
+    return kvp.Key != null && kvp.Value != null;
+  }
+  [Pure]
+  public static bool NonNullElements<T>(IEnumerator<T> iEnumerator) {
+    return iEnumerator != null;
+  }
+  //[Pure]
+  //public static bool NonNullElements<T>(Graphing.Graph<T> graph) {
+  //  return cce.NonNullElements(graph.TopologicalSort());
+  //}
+  [Pure]
+  public static void BeginExpose(object o) {
+  }
+  [Pure]
+  public static void EndExpose() {
+  }
+  [Pure]
+  public static bool IsPeerConsistent(object o) {
+    return true;
+  }
+  [Pure]
+  public static bool IsConsistent(object o) {
+    return true;
+  }
+  [Pure]
+  public static bool IsExposable(object o) {
+    return true;
+  }
+  [Pure]
+  public static bool IsExposed(object o) {
+    return true;
+  }
+  [Pure]
+  public static bool IsNew(object o) {
+    return true;
+  }
+  public static class Owner {
+    [Pure]
+    public static bool Same(object o, object p) {
+      return true;
+    }
+    [Pure]
+    public static void AssignSame(object o, object p) {
+    }
+    [Pure]
+    public static object ElementProxy(object o) {
+      return o;
+    }
+    [Pure]
+    public static bool None(object o) {
+      return true;
+    }
+    [Pure]
+    public static bool Different(object o, object p) {
+      return true;
+    }
+    [Pure]
+    public static bool New(object o) {
+      return true;
+    }
+  }
+  [Pure]
+  public static void LoopInvariant(bool p) {
+    Contract.Assert(p);
+  }
+  public class UnreachableException : Exception {
+    public UnreachableException() {
+    }
+  }
+  //[Pure]
+  //public static bool IsValid(Microsoft.Dafny.Expression expression) {
+  //  return true;
+  //}
+  //public static List<T> toList<T>(PureCollections.Sequence s) {
+  //  List<T> toRet = new List<T>();
+  //  foreach (T t in s.elems)
+  //    if(t!=null)
+  //    toRet.Add(t);
+  //  return toRet;
+  //}
+
+  //internal static bool NonNullElements(Set set) {
+  //  return set != null && Contract.ForAll(0,set.Count, i => set[i] != null);
+  //}
+}
+
+public class PeerAttribute : SA {
+}
+public class RepAttribute : SA {
+}
+public class CapturedAttribute : SA {
+}
+public class NotDelayedAttribute : SA {
+}
+public class NoDefaultContractAttribute : SA {
+}
+public class VerifyAttribute : SA {
+  public VerifyAttribute(bool b) {
+
+  }
+}
+public class StrictReadonlyAttribute : SA {
+}
+public class AdditiveAttribute : SA {
+}
+public class ReadsAttribute : SA {
+  public enum Reads {
+    Nothing,
+    Everything,
+  };
+  public ReadsAttribute(object o) {
+  }
+}
+public class GlobalAccessAttribute : SA {
+  public GlobalAccessAttribute(bool b) {
+  }
+}
+public class EscapesAttribute : SA {
+  public EscapesAttribute(bool b, bool b_2) {
+  }
+}
+public class NeedsContractsAttribute : SA {
+  public NeedsContractsAttribute() {
+  }
+  public NeedsContractsAttribute(bool ret, bool parameters) {
+  }
+  public NeedsContractsAttribute(bool ret, int[] parameters) {
+  }
+}
+public class ImmutableAttribute : SA {
+}
+public class InsideAttribute : SA {
+}
+public class SpecPublicAttribute : SA {
+}
+public class ElementsPeerAttribute : SA {
+}
+public class ResultNotNewlyAllocatedAttribute : SA {
+}
+public class OnceAttribute : SA {
 }
\ No newline at end of file