Merge branch 'unstable' into contrib

scripts/dead/mk_util_old.py

@@ -1,308 +0,0 @@
-############################################
-# Copyright (c) 2012 Microsoft Corporation
-# 
-# Auxiliary scripts for generating Makefiles 
-# and Visual Studio project files.
-#
-# Author: Leonardo de Moura (leonardo)
-############################################
-import os
-import glob
-
-BUILD_DIR='build'
-SRC_DIR='src'
-MODES=[]
-PLATFORMS=[]
-
-class MKException(Exception):
-    def __init__(self, value):
-        self.value = value
-    def __str__(self):
-        return repr(self.value)
-
-def set_build_dir(d):
-    global BUILD_DIR
-    BUILD_DIR = d
-    mk_dir(BUILD_DIR)
-
-def set_src_dir(d):
-    global SRC_DIR
-    SRC_DIR = d
-
-def set_modes(l):
-    global MODES
-    MODES=l
-
-def set_platforms(l):
-    global PLATFORMS
-    PLATFORMS=l
-
-VS_COMMON_OPTIONS='WIN32'
-VS_DBG_OPTIONS='_DEBUG'
-VS_RELEASE_OPTIONS='NDEBUG'
-
-GUI = 0
-Name2GUI = {}
-
-def mk_gui_str(id):
-    return '4D2F40D8-E5F9-473B-B548-%012d' % id
-
-MODULES = []
-HEADERS = []
-LIBS = []
-EXES = []
-DEPS = {}
-
-def set_vs_options(common, dbg, release):
-    global VS_COMMON_OPTIONS, VS_DBG_OPTIONS, VS_RELEASE_OPTIONS
-    VS_COMMON_OPTIONS = common
-    VS_DBG_OPTIONS = dbg
-    VS_RELEASE_OPTIONS = release
-
-def is_debug(mode):
-    return mode == 'Debug'
-
-def is_x64(platform):
-    return platform == 'x64'
-
-def mk_dir(d):
-    if not os.path.exists(d):
-        os.makedirs(d)
-
-def module_src_dir(name):
-    return '%s%s%s' % (SRC_DIR, os.sep, name)
-
-def module_build_dir(name):
-    return '%s%s%s' % (BUILD_DIR, os.sep, name)
-
-LIB_KIND = 0
-EXE_KIND = 1
-
-def get_extension(kind):
-    if kind == LIB_KIND:
-        return 'lib'
-    elif kind == EXE_KIND:
-        return 'exe'
-    else:
-        raise MKException('unknown kind %s' % kind)
-
-def vs_header(f):
-    f.write(
-'<?xml version="1.0" encoding="utf-8"?>\n'
-'<Project DefaultTargets="Build" ToolsVersion="4.0" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">\n')
-
-def vs_project_configurations(f, name):
-    global GUI, Name2GUI
-    f.write('  <ItemGroup Label="ProjectConfigurations">\n')
-    for mode in MODES:
-        for platform in PLATFORMS:
-            f.write('    <ProjectConfiguration Include="%s|%s">\n' % (mode, platform))
-            f.write('      <Configuration>%s</Configuration>\n' % mode)
-            f.write('      <Platform>%s</Platform>\n' % platform)
-            f.write('    </ProjectConfiguration>\n')
-    f.write('  </ItemGroup>\n')
-
-    f.write('   <PropertyGroup Label="Globals">\n')
-    f.write('    <ProjectGuid>{%s}</ProjectGuid>\n' % mk_gui_str(GUI))
-    f.write('    <ProjectName>%s</ProjectName>\n' % name)
-    f.write('    <Keyword>Win32Proj</Keyword>\n')
-    f.write('  </PropertyGroup>\n')
-    f.write('  <Import Project="$(VCTargetsPath)\Microsoft.Cpp.Default.props" />\n')
-    Name2GUI[name] = GUI
-    GUI = GUI + 1
-
-def vs_configurations(f, name, kind):
-    for mode in MODES:
-        for platform in PLATFORMS:
-            f.write('  <PropertyGroup Condition="\'$(Configuration)|$(Platform)\'==\'%s|%s\'" Label="Configuration">\n' % (mode, platform))
-            if kind == LIB_KIND:
-                f.write('    <ConfigurationType>StaticLibrary</ConfigurationType>\n')
-            elif kind == EXE_KIND:
-                f.write('    <ConfigurationType>Application</ConfigurationType>\n')
-            else:
-                raise MKException("unknown kind %s" % kind)
-            f.write('    <CharacterSet>Unicode</CharacterSet>\n')
-            f.write('    <UseOfMfc>false</UseOfMfc>\n')
-            f.write('  </PropertyGroup>\n')
-
-    f.write('  <Import Project="$(VCTargetsPath)\Microsoft.Cpp.props" />\n')
-    f.write('  <ImportGroup Label="ExtensionSettings">\n')
-    f.write('   </ImportGroup>\n')
-    f.write('   <ImportGroup Label="PropertySheets">\n')
-    f.write('    <Import Project="$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props" Condition="exists(\'$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props\')" Label="LocalAppDataPlatform" />  </ImportGroup>\n')
-    f.write('  <PropertyGroup Label="UserMacros" />\n')
-
-    f.write('  <PropertyGroup>\n')
-    for mode in MODES:
-        for platform in PLATFORMS:
-            if is_x64(platform):
-                f.write('    <OutDir Condition="\'$(Configuration)|$(Platform)\'==\'%s|%s\'">$(SolutionDir)$(Platform)\$(Configuration)\</OutDir>\n' % 
-                        (mode, platform))
-            else:
-                f.write('    <OutDir Condition="\'$(Configuration)|$(Platform)\'==\'%s|%s\'">$(SolutionDir)$(Configuration)\</OutDir>\n' % (mode, platform))
-    for mode in MODES:
-        for platform in PLATFORMS:
-            f.write('    <TargetName Condition="\'$(Configuration)|$(Platform)\'==\'%s|%s\'">%s</TargetName>\n' % (mode, platform, name))
-            f.write('    <TargetExt Condition="\'$(Configuration)|$(Platform)\'==\'%s|%s\'">.%s</TargetExt>\n' % (mode, platform, get_extension(kind)))
-    f.write('  </PropertyGroup>\n')
-
-def vs_compilation_options(f, name, deps, kind):
-    for mode in MODES:
-        for platform in PLATFORMS:
-            f.write('  <ItemDefinitionGroup Condition="\'$(Configuration)|$(Platform)\'==\'%s|%s\'">\n' % (mode, platform))
-            if is_x64(platform):
-                f.write('    <Midl>\n')
-                f.write('      <TargetEnvironment>X64</TargetEnvironment>\n')
-                f.write('    </Midl>\n')
-            f.write('    <ClCompile>\n')
-            if is_debug(mode):
-                f.write('      <Optimization>Disabled</Optimization>\n')
-            else:
-                f.write('      <Optimization>Full</Optimization>\n')
-            options = VS_COMMON_OPTIONS
-            if is_debug(mode):
-                options = "%s;%s" % (options, VS_DBG_OPTIONS)
-            else:
-                options = "%s;%s" % (options, VS_RELEASE_OPTIONS)
-            if is_x64(platform):
-                options = "%s;_AMD64_" % options
-            f.write('      <PreprocessorDefinitions>%s;%%(PreprocessorDefinitions)</PreprocessorDefinitions>\n' % options)
-            if is_debug(mode):
-                f.write('      <MinimalRebuild>true</MinimalRebuild>\n')
-                f.write('      <BasicRuntimeChecks>EnableFastChecks</BasicRuntimeChecks>\n')
-                f.write('      <WarningLevel>Level3</WarningLevel>\n')
-            f.write('      <RuntimeLibrary>MultiThreadedDebugDLL</RuntimeLibrary>\n')
-            f.write('      <OpenMPSupport>true</OpenMPSupport>\n')
-            f.write('      <DebugInformationFormat>ProgramDatabase</DebugInformationFormat>\n')
-            f.write('      <AdditionalIncludeDirectories>')
-            f.write('..\..\src\%s' % name)
-            for dep in deps:
-                f.write(';..\..\src\%s' % dep)
-            f.write('</AdditionalIncludeDirectories>\n')
-            f.write('    </ClCompile>\n')
-            f.write('    <Link>\n')
-            f.write('      <OutputFile>$(OutDir)%s.%s</OutputFile>\n' % (name, get_extension(kind)))
-            f.write('      <AdditionalLibraryDirectories>%(AdditionalLibraryDirectories)</AdditionalLibraryDirectories>\n')
-            if is_x64(platform):
-                f.write('      <TargetMachine>MachineX64</TargetMachine>\n')
-            else:
-                f.write('      <TargetMachine>MachineX86</TargetMachine>\n')
-            if kind == EXE_KIND:
-                f.write('<AdditionalDependencies>kernel32.lib;user32.lib;gdi32.lib;winspool.lib;comdlg32.lib;advapi32.lib;shell32.lib;ole32.lib;oleaut32.lib;uuid.lib;odbc32.lib;odbccp32.lib')
-                for dep in deps:
-                    f.write(';$(OutDir)%s.lib' % dep)
-                    # if is_x64(platform):
-                    #    f.write(';..\%s\%s\%s\%s.lib' % (dep, platform, mode, dep))
-                    # else:
-                    #    f.write(';..\%s\%s\%s.lib' % (dep, mode, dep))
-                f.write(';%(AdditionalDependencies)</AdditionalDependencies>\n')
-            f.write('    </Link>\n')
-            f.write('  </ItemDefinitionGroup>\n')
-
-def add_vs_cpps(f, name):
-    f.write('  <ItemGroup>\n')
-    srcs = module_src_dir(name)
-    for cppfile in glob.glob(os.path.join(srcs, '*.cpp')):
-       f.write('    <ClCompile Include="..%s..%s%s" />\n' % (os.sep, os.sep, cppfile))
-    f.write('  </ItemGroup>\n')
-
-def vs_footer(f):
-    f.write(
-'  <Import Project="$(VCTargetsPath)\Microsoft.Cpp.targets" />\n'
-'  <ImportGroup Label="ExtensionTargets">\n'
-'  </ImportGroup>\n'
-'</Project>\n')
-
-def check_new_component(name):
-    if (name in HEADERS) or (name in LIBS) or (name in EXES):
-        raise MKException("Component '%s' was already defined" % name)
-
-# Add a directory containing only .h files
-def add_header(name):
-    check_new_component(name)
-    HEADERS.append(name)
-
-def find_all_deps(name, deps):
-    new_deps = []
-    for dep in deps:
-        if dep in LIBS:
-            if not (dep in new_deps):
-                new_deps.append(dep)
-            for dep_dep in DEPS[dep]:
-                if not (dep_dep in new_deps):
-                    new_deps.append(dep_dep)
-        elif dep in HEADERS:
-            if not (dep in new_deps):
-                new_deps.append(dep)
-        else:
-            raise MKException("Unknown component '%s' at '%s'." % (dep, name))
-    return new_deps
-
-def add_component(name, deps, kind):
-    check_new_component(name)
-    if kind == LIB_KIND:
-        LIBS.append(name)
-    elif kind == EXE_KIND:
-        EXES.append(name)
-    else:
-        raise MKException("unknown kind %s" % kind)
-    MODULES.append(name)
-    deps = find_all_deps(name, deps)
-    DEPS[name] = deps
-    print "Dependencies for '%s': %s" % (name, deps)
-
-    module_dir = module_build_dir(name)
-    mk_dir(module_dir)
-
-    vs_proj = open('%s%s%s.vcxproj' % (module_dir, os.sep, name), 'w')
-    vs_header(vs_proj)
-    vs_project_configurations(vs_proj, name)
-    vs_configurations(vs_proj, name, kind)
-    vs_compilation_options(vs_proj, name, deps, kind)
-    add_vs_cpps(vs_proj, name)
-    vs_footer(vs_proj)
-
-def add_lib(name, deps):
-    add_component(name, deps, LIB_KIND)
-
-def add_exe(name, deps):
-    add_component(name, deps, EXE_KIND)
-
-def is_lib(name):
-    # Add DLL dependency
-    return name in LIBS
-
-def mk_vs_solution():
-    sln = open('%s%sz3.sln' % (BUILD_DIR, os.sep), 'w')
-    sln.write('\n')
-    sln.write("Microsoft Visual Studio Solution File, Format Version 11.00\n")
-    sln.write("# Visual Studio 2010\n")
-    for module in MODULES:
-        gui = Name2GUI[module]
-        deps = DEPS[module]
-        sln.write('Project("{8BC9CEB8-8B4A-11D0-8D11-00A0C91BC942}") = "%s", "%s%s%s.vcxproj", "{%s}"\n' %
-                  (module, module, os.sep, module, mk_gui_str(gui)))
-        if len(deps) > 0:
-            sln.write('    ProjectSection(ProjectDependencies) = postProject\n')
-            for dep in deps:
-                if is_lib(dep):
-                    i = Name2GUI[dep]
-                    sln.write('        {%s} = {%s}\n' % (mk_gui_str(i), mk_gui_str(i)))
-            sln.write('    EndProjectSection\n')
-        sln.write('EndProject\n')
-    sln.write('Global\n')
-    sln.write('GlobalSection(SolutionConfigurationPlatforms) = preSolution\n')
-    for mode in MODES:
-        for platform in PLATFORMS:
-            sln.write('   %s|%s = %s|%s\n' % (mode, platform, mode, platform))
-    sln.write('EndGlobalSection\n')
-    sln.write('GlobalSection(ProjectConfigurationPlatforms) = postSolution\n')
-    for module in MODULES:
-        gui = Name2GUI[module]
-        for mode in MODES:
-            for platform in PLATFORMS:
-                sln.write('    {%s}.%s|%s.ActiveCfg = %s|%s\n' % (mk_gui_str(gui), mode, platform, mode, platform))
-                sln.write('    {%s}.%s|%s.Build.0   = %s|%s\n' % (mk_gui_str(gui), mode, platform, mode, platform))
-    sln.write('EndGlobalSection\n')
-                
-    print "Visual Solution was generated."

src/api/dotnet/AST.cs

@@ -203,7 +203,7 @@ namespace Microsoft.Z3
         internal AST(Context ctx) : base(ctx) { Contract.Requires(ctx != null); }
         internal AST(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
 
-        internal class DecRefQueue : Z3.DecRefQueue
+        internal class DecRefQueue : IDecRefQueue
         {
             public override void IncRef(Context ctx, IntPtr obj)
             {

src/api/dotnet/ASTMap.cs

@@ -126,7 +126,7 @@ namespace Microsoft.Z3
             Contract.Requires(ctx != null);
         }
 
-        internal class DecRefQueue : Z3.DecRefQueue
+        internal class DecRefQueue : IDecRefQueue
         {
             public override void IncRef(Context ctx, IntPtr obj)
             {

src/api/dotnet/ASTVector.cs

@@ -103,7 +103,7 @@ namespace Microsoft.Z3
         internal ASTVector(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
         internal ASTVector(Context ctx) : base(ctx, Native.Z3_mk_ast_vector(ctx.nCtx)) { Contract.Requires(ctx != null); }
 
-        internal class DecRefQueue : Z3.DecRefQueue
+        internal class DecRefQueue : IDecRefQueue
         {
             public override void IncRef(Context ctx, IntPtr obj)
             {

src/api/dotnet/AlgebraicNum.cs

@@ -0,0 +1,81 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    IntNum.cs
+
+Abstract:
+
+    Z3 Managed API: Int Numerals
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2012-03-20
+
+Notes:
+    
+--*/
+using System;
+using System.Diagnostics.Contracts;
+
+#if !FRAMEWORK_LT_4
+using System.Numerics;
+#endif
+
+namespace Microsoft.Z3
+{
+    /// <summary>
+    /// Algebraic numbers
+    /// </summary>
+    [ContractVerification(true)]
+    public class AlgebraicNum : ArithExpr
+    {
+        /// <summary>
+        /// Return a upper bound for a given real algebraic number. 
+        /// The interval isolating the number is smaller than 1/10^<paramref name="precision"/>.    
+        /// <seealso cref="Expr.IsAlgebraicNumber"/>   
+        /// </summary>
+        /// <param name="precision">the precision of the result</param>
+        /// <returns>A numeral Expr of sort Real</returns>
+        public RatNum ToUpper(uint precision)
+        {
+            Contract.Ensures(Contract.Result<RatNum>() != null);
+
+            return new RatNum(Context, Native.Z3_get_algebraic_number_upper(Context.nCtx, NativeObject, precision));
+        }
+
+        /// <summary>
+        /// Return a lower bound for the given real algebraic number. 
+        /// The interval isolating the number is smaller than 1/10^<paramref name="precision"/>.    
+        /// <seealso cref="Expr.IsAlgebraicNumber"/>
+        /// </summary>
+        /// <param name="precision"></param>
+        /// <returns>A numeral Expr of sort Real</returns>
+        public RatNum ToLower(uint precision)
+        {
+            Contract.Ensures(Contract.Result<RatNum>() != null);
+
+            return new RatNum(Context, Native.Z3_get_algebraic_number_lower(Context.nCtx, NativeObject, precision));
+        }
+
+        /// <summary>
+        /// Returns a string representation in decimal notation.
+        /// </summary>
+        /// <remarks>The result has at most <paramref name="precision"/> decimal places.</remarks>    
+        public string ToDecimal(uint precision)
+        {
+            Contract.Ensures(Contract.Result<string>() != null);
+
+            return Native.Z3_get_numeral_decimal_string(Context.nCtx, NativeObject, precision);
+        }
+
+        #region Internal
+        internal AlgebraicNum(Context ctx, IntPtr obj)
+            : base(ctx, obj)
+        {
+            Contract.Requires(ctx != null);
+        }
+        #endregion
+    }
+}

src/api/dotnet/ApplyResult.cs

@@ -44,8 +44,8 @@ namespace Microsoft.Z3
         {
             get
             {
-              Contract.Ensures(Contract.Result<Goal[]>() != null);
+                Contract.Ensures(Contract.Result<Goal[]>() != null);
-              Contract.Ensures(Contract.Result<Goal[]>().Length == this.NumSubgoals);
+                Contract.Ensures(Contract.Result<Goal[]>().Length == this.NumSubgoals);
 
                 uint n = NumSubgoals;
                 Goal[] res = new Goal[n];
@@ -77,12 +77,13 @@ namespace Microsoft.Z3
         }
 
         #region Internal
-        internal ApplyResult(Context ctx, IntPtr obj) : base(ctx, obj) 
+        internal ApplyResult(Context ctx, IntPtr obj)
+            : base(ctx, obj)
         {
             Contract.Requires(ctx != null);
         }
 
-        internal class DecRefQueue : Z3.DecRefQueue
+        internal class DecRefQueue : IDecRefQueue
         {
             public override void IncRef(Context ctx, IntPtr obj)
             {

src/api/dotnet/ArithExpr.cs

@@ -0,0 +1,47 @@
+/*++
+Copyright (<c>) 2012 Microsoft Corporation
+
+Module Name:
+
+    ArithExpr.cs
+
+Abstract:
+
+    Z3 Managed API: Arith Expressions
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2012-11-23
+
+Notes:
+    
+--*/
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Z3
+{
+    /// <summary>
+    /// Arithmetic expressions (int/real)
+    /// </summary>
+    public class ArithExpr : Expr
+    {
+        #region Internal
+        /// <summary> Constructor for ArithExpr </summary>
+        internal protected ArithExpr(Context ctx)
+            : base(ctx)
+        {
+            Contract.Requires(ctx != null);
+        }
+        internal ArithExpr(Context ctx, IntPtr obj)
+            : base(ctx, obj)
+        {
+            Contract.Requires(ctx != null);
+        }
+        #endregion
+    }
+}

src/api/dotnet/ArithSort.cs

@@ -0,0 +1,34 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    ArithSort.cs
+
+Abstract:
+
+    Z3 Managed API: Arith Sorts
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2012-11-23
+
+Notes:
+    
+--*/
+
+using System;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Z3
+{
+    /// <summary>
+    /// An arithmetic sort, i.e., Int or Real.
+    /// </summary>
+    public class ArithSort : Sort
+    {
+        #region Internal
+        internal ArithSort(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
+        #endregion
+    };
+}

src/api/dotnet/ArrayExpr.cs

@@ -0,0 +1,47 @@
+/*++
+Copyright (<c>) 2012 Microsoft Corporation
+
+Module Name:
+
+    ArrayExpr.cs
+
+Abstract:
+
+    Z3 Managed API: Array Expressions
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2012-11-23
+
+Notes:
+    
+--*/
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Z3
+{
+    /// <summary>
+    /// Array expressions
+    /// </summary>
+    public class ArrayExpr : Expr
+    {
+        #region Internal
+        /// <summary> Constructor for ArrayExpr </summary>
+        internal protected ArrayExpr(Context ctx)
+            : base(ctx)
+        {
+            Contract.Requires(ctx != null);
+        }
+        internal ArrayExpr(Context ctx, IntPtr obj)
+            : base(ctx, obj)
+        {
+            Contract.Requires(ctx != null);
+        }
+        #endregion
+    }
+}

src/api/dotnet/ArraySort.cs

@@ -0,0 +1,69 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    ArraySort.cs
+
+Abstract:
+
+    Z3 Managed API: Array Sorts
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2012-11-23
+
+Notes:
+    
+--*/
+
+using System;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Z3
+{
+    /// <summary>
+    /// Array sorts.
+    /// </summary>
+    [ContractVerification(true)]
+    public class ArraySort : Sort
+    {
+        /// <summary>
+        /// The domain of the array sort.
+        /// </summary>
+        public Sort Domain
+        {
+            get
+            {
+                Contract.Ensures(Contract.Result<Sort>() != null);
+
+                return Sort.Create(Context, Native.Z3_get_array_sort_domain(Context.nCtx, NativeObject));
+            }
+        }
+
+        /// <summary>
+        /// The range of the array sort.
+        /// </summary>
+        public Sort Range
+        {
+            get
+            {
+                Contract.Ensures(Contract.Result<Sort>() != null);
+
+                return Sort.Create(Context, Native.Z3_get_array_sort_range(Context.nCtx, NativeObject));
+            }
+        }
+
+        #region Internal
+        internal ArraySort(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
+        internal ArraySort(Context ctx, Sort domain, Sort range)
+            : base(ctx, Native.Z3_mk_array_sort(ctx.nCtx, domain.NativeObject, range.NativeObject))
+        {
+            Contract.Requires(ctx != null);
+            Contract.Requires(domain != null);
+            Contract.Requires(range != null);
+        }
+        #endregion
+    };
+
+}

src/api/dotnet/BitVecExpr.cs

@@ -0,0 +1,48 @@
+/*++
+Copyright (<c>) 2012 Microsoft Corporation
+
+Module Name:
+
+    BitVecExpr.cs
+
+Abstract:
+
+    Z3 Managed API: BitVec Expressions
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2012-11-23
+
+Notes:
+    
+--*/
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Z3
+{
+    /// <summary>
+    /// Bit-vector expressions
+    /// </summary>
+    public class BitVecExpr : Expr
+    {
+
+        /// <summary>
+        /// The size of the sort of a bit-vector term.
+        /// </summary>
+        public uint SortSize
+        {
+            get { return ((BitVecSort)Sort).Size; }
+        }
+
+        #region Internal
+        /// <summary> Constructor for BitVecExpr </summary>
+        internal protected BitVecExpr(Context ctx) : base(ctx) { Contract.Requires(ctx != null); }
+        internal BitVecExpr(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
+        #endregion
+    }
+}

src/api/dotnet/BitVecNum.cs

@@ -0,0 +1,115 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    IntNum.cs
+
+Abstract:
+
+    Z3 Managed API: Int Numerals
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2012-03-20
+
+Notes:
+    
+--*/
+using System;
+using System.Diagnostics.Contracts;
+
+#if !FRAMEWORK_LT_4
+using System.Numerics;
+#endif
+
+namespace Microsoft.Z3
+{
+    /// <summary>
+    /// Bit-vector numerals
+    /// </summary>
+    [ContractVerification(true)]
+    public class BitVecNum : BitVecExpr
+    {
+        /// <summary>
+        /// Retrieve the 64-bit unsigned integer value.
+        /// </summary>
+        public UInt64 UInt64
+        {
+            get
+            {
+                UInt64 res = 0;
+                if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == 0)
+                    throw new Z3Exception("Numeral is not a 64 bit unsigned");
+                return res;
+            }
+        }
+
+        /// <summary>
+        /// Retrieve the int value.
+        /// </summary>
+        public int Int
+        {
+            get
+            {
+                int res = 0;
+                if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == 0)
+                    throw new Z3Exception("Numeral is not an int");
+                return res;
+            }
+        }
+
+        /// <summary>
+        /// Retrieve the 64-bit int value.
+        /// </summary>
+        public Int64 Int64
+        {
+            get
+            {
+                Int64 res = 0;
+                if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == 0)
+                    throw new Z3Exception("Numeral is not an int64");
+                return res;
+            }
+        }
+
+        /// <summary>
+        /// Retrieve the int value.
+        /// </summary>
+        public uint UInt
+        {
+            get
+            {
+                uint res = 0;
+                if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == 0)
+                    throw new Z3Exception("Numeral is not a uint");
+                return res;
+            }
+        }
+
+#if !FRAMEWORK_LT_4
+        /// <summary>
+        /// Retrieve the BigInteger value.
+        /// </summary>
+        public BigInteger BigInteger
+        {
+            get
+            {
+                return BigInteger.Parse(this.ToString());
+            }
+        }
+#endif
+
+        /// <summary>
+        /// Returns a string representation of the numeral.
+        /// </summary>        
+        public override string ToString()
+        {
+            return Native.Z3_get_numeral_string(Context.nCtx, NativeObject);
+        }
+
+        #region Internal
+        internal BitVecNum(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
+        #endregion
+    }
+}

src/api/dotnet/BitVecSort.cs

@@ -0,0 +1,43 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    BitVecSort.cs
+
+Abstract:
+
+    Z3 Managed API: BitVec Sorts
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2012-11-23
+
+Notes:
+    
+--*/
+
+using System;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Z3
+{
+    /// <summary>
+    /// Bit-vector sorts.
+    /// </summary>
+    public class BitVecSort : Sort
+    {
+        /// <summary>
+        /// The size of the bit-vector sort.
+        /// </summary>
+        public uint Size
+        {
+            get { return Native.Z3_get_bv_sort_size(Context.nCtx, NativeObject); }
+        }
+
+        #region Internal
+        internal BitVecSort(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
+        internal BitVecSort(Context ctx, uint size) : base(ctx, Native.Z3_mk_bv_sort(ctx.nCtx, size)) { Contract.Requires(ctx != null); }
+        #endregion
+    };
+}

src/api/dotnet/BoolExpr.cs

@@ -0,0 +1,40 @@
+/*++
+Copyright (<c>) 2012 Microsoft Corporation
+
+Module Name:
+
+    BoolExpr.cs
+
+Abstract:
+
+    Z3 Managed API: Boolean Expressions
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2012-11-23
+
+Notes:
+    
+--*/
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Z3
+{
+    /// <summary>
+    /// Boolean expressions
+    /// </summary>
+    public class BoolExpr : Expr
+    {
+        #region Internal
+        /// <summary> Constructor for BoolExpr </summary>
+        internal protected BoolExpr(Context ctx) : base(ctx) { Contract.Requires(ctx != null); }
+        /// <summary> Constructor for BoolExpr </summary>
+        internal BoolExpr(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
+        #endregion
+    }
+}

src/api/dotnet/BoolSort.cs

@@ -0,0 +1,35 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    BoolSort.cs
+
+Abstract:
+
+    Z3 Managed API: Bool Sorts
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2012-11-23
+
+Notes:
+    
+--*/
+
+using System;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Z3
+{
+    /// <summary>
+    /// A Boolean sort.
+    /// </summary>
+    public class BoolSort : Sort
+    {
+        #region Internal
+        internal BoolSort(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
+        internal BoolSort(Context ctx) : base(ctx, Native.Z3_mk_bool_sort(ctx.nCtx)) { Contract.Requires(ctx != null); }
+        #endregion
+    };
+}

src/api/dotnet/Constructor.cs

@@ -149,35 +149,4 @@ namespace Microsoft.Z3
 
         #endregion
     }
-
-    /// <summary>
-    /// Lists of constructors
-    /// </summary>
-    public class ConstructorList : Z3Object
-    {
-        /// <summary>
-        /// Destructor.
-        /// </summary>
-        ~ConstructorList()
-        {
-            Native.Z3_del_constructor_list(Context.nCtx, NativeObject);
-        }
-
-        #region Internal
-        internal ConstructorList(Context ctx, IntPtr obj)
-            : base(ctx, obj)
-        {
-            Contract.Requires(ctx != null);
-        }
-
-        internal ConstructorList(Context ctx, Constructor[] constructors)
-            : base(ctx)
-        {
-            Contract.Requires(ctx != null);
-            Contract.Requires(constructors != null);
-
-            NativeObject = Native.Z3_mk_constructor_list(Context.nCtx, (uint)constructors.Length, Constructor.ArrayToNative(constructors));
-        }
-        #endregion
-    }
 }

src/api/dotnet/ConstructorList.cs

@@ -0,0 +1,59 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    ConstructorList.cs
+
+Abstract:
+
+    Z3 Managed API: Constructor Lists
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2012-11-23
+
+Notes:
+    
+--*/
+
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Z3
+{
+    /// <summary>
+    /// Lists of constructors
+    /// </summary>
+    public class ConstructorList : Z3Object
+    {
+        /// <summary>
+        /// Destructor.
+        /// </summary>
+        ~ConstructorList()
+        {
+            Native.Z3_del_constructor_list(Context.nCtx, NativeObject);
+        }
+
+        #region Internal
+        internal ConstructorList(Context ctx, IntPtr obj)
+            : base(ctx, obj)
+        {
+            Contract.Requires(ctx != null);
+        }
+
+        internal ConstructorList(Context ctx, Constructor[] constructors)
+            : base(ctx)
+        {
+            Contract.Requires(ctx != null);
+            Contract.Requires(constructors != null);
+
+            NativeObject = Native.Z3_mk_constructor_list(Context.nCtx, (uint)constructors.Length, Constructor.ArrayToNative(constructors));
+        }
+        #endregion
+    }
+}

src/api/dotnet/DatatypeExpr.cs

@@ -0,0 +1,47 @@
+/*++
+Copyright (<c>) 2012 Microsoft Corporation
+
+Module Name:
+
+    DatatypeExpr.cs
+
+Abstract:
+
+    Z3 Managed API: Datatype Expressions
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2012-11-23
+
+Notes:
+    
+--*/
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Z3
+{
+    /// <summary>
+    /// Datatype expressions
+    /// </summary>
+    public class DatatypeExpr : Expr
+    {
+        #region Internal
+        /// <summary> Constructor for DatatypeExpr </summary>
+        internal protected DatatypeExpr(Context ctx)
+            : base(ctx)
+        {
+            Contract.Requires(ctx != null);
+        }
+        internal DatatypeExpr(Context ctx, IntPtr obj)
+            : base(ctx, obj)
+        {
+            Contract.Requires(ctx != null);
+        }
+        #endregion
+    }
+}

src/api/dotnet/DatatypeSort.cs

@@ -0,0 +1,109 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    DatatypeSort.cs
+
+Abstract:
+
+    Z3 Managed API: Datatype Sorts
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2012-11-23
+
+Notes:
+    
+--*/
+
+using System;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Z3
+{
+    /// <summary>
+    /// Datatype sorts.
+    /// </summary>
+    [ContractVerification(true)]
+    public class DatatypeSort : Sort
+    {
+        /// <summary>
+        /// The number of constructors of the datatype sort.
+        /// </summary>
+        public uint NumConstructors
+        {
+            get { return Native.Z3_get_datatype_sort_num_constructors(Context.nCtx, NativeObject); }
+        }
+
+        /// <summary>
+        /// The constructors.
+        /// </summary>
+        public FuncDecl[] Constructors
+        {
+            get
+            {
+                Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
+
+                uint n = NumConstructors;
+                FuncDecl[] res = new FuncDecl[n];
+                for (uint i = 0; i < n; i++)
+                    res[i] = new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor(Context.nCtx, NativeObject, i));
+                return res;
+            }
+        }
+
+        /// <summary>
+        /// The recognizers.
+        /// </summary>
+        public FuncDecl[] Recognizers
+        {
+            get
+            {
+                Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
+
+                uint n = NumConstructors;
+                FuncDecl[] res = new FuncDecl[n];
+                for (uint i = 0; i < n; i++)
+                    res[i] = new FuncDecl(Context, Native.Z3_get_datatype_sort_recognizer(Context.nCtx, NativeObject, i));
+                return res;
+            }
+        }
+
+        /// <summary>
+        /// The constructor accessors.
+        /// </summary>
+        public FuncDecl[][] Accessors
+        {
+            get
+            {
+                Contract.Ensures(Contract.Result<FuncDecl[][]>() != null);
+
+                uint n = NumConstructors;
+                FuncDecl[][] res = new FuncDecl[n][];
+                for (uint i = 0; i < n; i++)
+                {
+                    FuncDecl fd = new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor(Context.nCtx, NativeObject, i));
+                    uint ds = fd.DomainSize;
+                    FuncDecl[] tmp = new FuncDecl[ds];
+                    for (uint j = 0; j < ds; j++)
+                        tmp[j] = new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor_accessor(Context.nCtx, NativeObject, i, j));
+                    res[i] = tmp;
+                }
+                return res;
+            }
+        }
+
+        #region Internal
+        internal DatatypeSort(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
+
+        internal DatatypeSort(Context ctx, Symbol name, Constructor[] constructors)
+            : base(ctx, Native.Z3_mk_datatype(ctx.nCtx, name.NativeObject, (uint)constructors.Length, ArrayToNative(constructors)))
+        {
+            Contract.Requires(ctx != null);
+            Contract.Requires(name != null);
+            Contract.Requires(constructors != null);
+        }
+        #endregion
+    };
+}

src/api/dotnet/EnumSort.cs

@@ -0,0 +1,111 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    EnumSort.cs
+
+Abstract:
+
+    Z3 Managed API: Enum Sorts
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2012-11-23
+
+Notes:
+    
+--*/
+
+using System;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Z3
+{
+    /// <summary>
+    /// Enumeration sorts.
+    /// </summary>
+    [ContractVerification(true)]
+    public class EnumSort : Sort
+    {
+        /// <summary>
+        /// The function declarations of the constants in the enumeration.
+        /// </summary>
+        public FuncDecl[] ConstDecls
+        {
+            get
+            {
+                Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
+
+                return _constdecls;
+            }
+        }
+
+        /// <summary>
+        /// The constants in the enumeration.
+        /// </summary>
+        public Expr[] Consts
+        {
+            get
+            {
+                Contract.Ensures(Contract.Result<Expr[]>() != null);
+
+                return _consts;
+            }
+        }
+
+        /// <summary>
+        /// The test predicates for the constants in the enumeration.
+        /// </summary>
+        public FuncDecl[] TesterDecls
+        {
+            get
+            {
+                Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
+
+                return _testerdecls;
+            }
+        }
+
+        #region Object Invariant
+
+        [ContractInvariantMethod]
+        private void ObjectInvariant()
+        {
+            Contract.Invariant(this._constdecls != null);
+            Contract.Invariant(this._testerdecls != null);
+            Contract.Invariant(this._consts != null);
+        }
+
+
+        #endregion
+
+        #region Internal
+        readonly private FuncDecl[] _constdecls = null, _testerdecls = null;
+        readonly private Expr[] _consts = null;
+
+        internal EnumSort(Context ctx, Symbol name, Symbol[] enumNames)
+            : base(ctx)
+        {
+            Contract.Requires(ctx != null);
+            Contract.Requires(name != null);
+            Contract.Requires(enumNames != null);
+
+            int n = enumNames.Length;
+            IntPtr[] n_constdecls = new IntPtr[n];
+            IntPtr[] n_testers = new IntPtr[n];
+            NativeObject = Native.Z3_mk_enumeration_sort(ctx.nCtx, name.NativeObject, (uint)n,
+                                                         Symbol.ArrayToNative(enumNames), n_constdecls, n_testers);
+            _constdecls = new FuncDecl[n];
+            for (uint i = 0; i < n; i++)
+                _constdecls[i] = new FuncDecl(ctx, n_constdecls[i]);
+            _testerdecls = new FuncDecl[n];
+            for (uint i = 0; i < n; i++)
+                _testerdecls[i] = new FuncDecl(ctx, n_testers[i]);
+            _consts = new Expr[n];
+            for (uint i = 0; i < n; i++)
+                _consts[i] = ctx.MkApp(_constdecls[i]);
+        }
+        #endregion
+    };
+}

src/api/dotnet/Expr.cs

@@ -1548,138 +1548,4 @@ namespace Microsoft.Z3
         }
         #endregion
     }
-
-    /// <summary>
-    /// Boolean expressions
-    /// </summary>
-    public class BoolExpr : Expr
-    {
-        #region Internal
-        /// <summary> Constructor for BoolExpr </summary>
-        internal protected BoolExpr(Context ctx) : base(ctx) { Contract.Requires(ctx != null); }
-        /// <summary> Constructor for BoolExpr </summary>
-        internal BoolExpr(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
-        #endregion
-    }
-
-    /// <summary>
-    /// Arithmetic expressions (int/real)
-    /// </summary>
-    public class ArithExpr : Expr
-    {
-        #region Internal
-        /// <summary> Constructor for ArithExpr </summary>
-        internal protected ArithExpr(Context ctx)
-            : base(ctx)
-        {
-            Contract.Requires(ctx != null);
-        }
-        internal ArithExpr(Context ctx, IntPtr obj)
-            : base(ctx, obj)
-        {
-            Contract.Requires(ctx != null);
-        }
-        #endregion
-    }
-
-    /// <summary>
-    /// Int expressions
-    /// </summary>
-    public class IntExpr : ArithExpr
-    {
-        #region Internal
-        /// <summary> Constructor for IntExpr </summary>
-        internal protected IntExpr(Context ctx)
-            : base(ctx)
-        {
-            Contract.Requires(ctx != null);
-        }
-        internal IntExpr(Context ctx, IntPtr obj)
-            : base(ctx, obj)
-        {
-            Contract.Requires(ctx != null);
-        }
-        #endregion
-    }
-
-    /// <summary>
-    /// Real expressions
-    /// </summary>
-    public class RealExpr : ArithExpr
-    {
-        #region Internal
-        /// <summary> Constructor for RealExpr </summary>
-        internal protected RealExpr(Context ctx)
-            : base(ctx)
-        {
-            Contract.Requires(ctx != null);
-        }
-        internal RealExpr(Context ctx, IntPtr obj)
-            : base(ctx, obj)
-        {
-            Contract.Requires(ctx != null);
-        }
-        #endregion
-    }
-
-    /// <summary>
-    /// Bit-vector expressions
-    /// </summary>
-    public class BitVecExpr : Expr
-    {
-
-        /// <summary>
-        /// The size of the sort of a bit-vector term.
-        /// </summary>
-        public uint SortSize
-        {
-            get { return ((BitVecSort)Sort).Size; }
-        }
-
-        #region Internal
-        /// <summary> Constructor for BitVecExpr </summary>
-        internal protected BitVecExpr(Context ctx) : base(ctx) { Contract.Requires(ctx != null); }
-        internal BitVecExpr(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
-        #endregion
-    }
-
-    /// <summary>
-    /// Array expressions
-    /// </summary>
-    public class ArrayExpr : Expr
-    {
-        #region Internal
-        /// <summary> Constructor for ArrayExpr </summary>
-        internal protected ArrayExpr(Context ctx)
-            : base(ctx)
-        {
-            Contract.Requires(ctx != null);
-        }
-        internal ArrayExpr(Context ctx, IntPtr obj)
-            : base(ctx, obj)
-        {
-            Contract.Requires(ctx != null);
-        }
-        #endregion
-    }
-
-    /// <summary>
-    /// Datatype expressions
-    /// </summary>
-    public class DatatypeExpr : Expr
-    {
-        #region Internal
-        /// <summary> Constructor for DatatypeExpr </summary>
-        internal protected DatatypeExpr(Context ctx)
-            : base(ctx)
-        {
-            Contract.Requires(ctx != null);
-        }
-        internal DatatypeExpr(Context ctx, IntPtr obj)
-            : base(ctx, obj)
-        {
-            Contract.Requires(ctx != null);
-        }
-        #endregion
-    }
 }

src/api/dotnet/FiniteDomainSort.cs

@@ -0,0 +1,59 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    FiniteDomainSort.cs
+
+Abstract:
+
+    Z3 Managed API: Finite Domain Sorts
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2012-11-23
+
+Notes:
+    
+--*/
+
+using System;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Z3
+{
+    /// <summary>
+    /// Finite domain sorts.
+    /// </summary>
+    [ContractVerification(true)]
+    public class FiniteDomainSort : Sort
+    {
+        /// <summary>
+        /// The size of the finite domain sort.
+        /// </summary>
+        public ulong Size
+        {
+            get
+            {
+                ulong res = 0;
+                Native.Z3_get_finite_domain_sort_size(Context.nCtx, NativeObject, ref res);
+                return res;
+            }
+        }
+
+        #region Internal
+        internal FiniteDomainSort(Context ctx, IntPtr obj)
+            : base(ctx, obj)
+        {
+            Contract.Requires(ctx != null);
+        }
+        internal FiniteDomainSort(Context ctx, Symbol name, ulong size)
+            : base(ctx, Native.Z3_mk_finite_domain_sort(ctx.nCtx, name.NativeObject, size))
+        {
+            Contract.Requires(ctx != null);
+            Contract.Requires(name != null);
+
+        }
+        #endregion
+    }
+}

src/api/dotnet/Fixedpoint.cs

@@ -310,7 +310,7 @@ namespace Microsoft.Z3
             Contract.Requires(ctx != null);
         }
 
-        internal class DecRefQueue : Z3.DecRefQueue
+        internal class DecRefQueue : IDecRefQueue
         {
             public override void IncRef(Context ctx, IntPtr obj)
             {

src/api/dotnet/FuncDecl.cs

@@ -291,9 +291,7 @@ namespace Microsoft.Z3
         }
 
         internal FuncDecl(Context ctx, Symbol name, Sort[] domain, Sort range)
-            : base(ctx, Native.Z3_mk_func_decl(ctx.nCtx, name.NativeObject,
+            : base(ctx, Native.Z3_mk_func_decl(ctx.nCtx, name.NativeObject, AST.ArrayLength(domain), AST.ArrayToNative(domain), range.NativeObject))
-                                             AST.ArrayLength(domain), AST.ArrayToNative(domain),
-                                             range.NativeObject))
         {
             Contract.Requires(ctx != null);
             Contract.Requires(name != null);
@@ -301,9 +299,7 @@ namespace Microsoft.Z3
         }
 
         internal FuncDecl(Context ctx, string prefix, Sort[] domain, Sort range)
-            : base(ctx, Native.Z3_mk_fresh_func_decl(ctx.nCtx, prefix,
+            : base(ctx, Native.Z3_mk_fresh_func_decl(ctx.nCtx, prefix, AST.ArrayLength(domain), AST.ArrayToNative(domain), range.NativeObject))
-                                             AST.ArrayLength(domain), AST.ArrayToNative(domain),
-                                             range.NativeObject))
         {
             Contract.Requires(ctx != null);
             Contract.Requires(range != null);

src/api/dotnet/FuncInterp.cs

@@ -40,9 +40,11 @@ namespace Microsoft.Z3
             /// </summary>
             public Expr Value
             {
-                get {
+                get
+                {
                     Contract.Ensures(Contract.Result<Expr>() != null);
-                    return Expr.Create(Context, Native.Z3_func_entry_get_value(Context.nCtx, NativeObject)); }
+                    return Expr.Create(Context, Native.Z3_func_entry_get_value(Context.nCtx, NativeObject));
+                }
             }
 
             /// <summary>
@@ -87,7 +89,7 @@ namespace Microsoft.Z3
             #region Internal
             internal Entry(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
 
-            internal class DecRefQueue : Z3.DecRefQueue
+            internal class DecRefQueue : IDecRefQueue
             {
                 public override void IncRef(Context ctx, IntPtr obj)
                 {
@@ -130,8 +132,7 @@ namespace Microsoft.Z3
             get
             {
                 Contract.Ensures(Contract.Result<Entry[]>() != null);
-                Contract.Ensures(Contract.ForAll(0, Contract.Result<Entry[]>().Length, 
+                Contract.Ensures(Contract.ForAll(0, Contract.Result<Entry[]>().Length, j => Contract.Result<Entry[]>()[j] != null));
-                    j => Contract.Result<Entry[]>()[j] != null));
 
                 uint n = NumEntries;
                 Entry[] res = new Entry[n];
@@ -146,10 +147,12 @@ namespace Microsoft.Z3
         /// </summary>
         public Expr Else
         {
-            get {
+            get
+            {
                 Contract.Ensures(Contract.Result<Expr>() != null);
 
-                return Expr.Create(Context, Native.Z3_func_interp_get_else(Context.nCtx, NativeObject)); }
+                return Expr.Create(Context, Native.Z3_func_interp_get_else(Context.nCtx, NativeObject));
+            }
         }
 
         /// <summary>
@@ -192,7 +195,7 @@ namespace Microsoft.Z3
             Contract.Requires(ctx != null);
         }
 
-        internal class DecRefQueue : Z3.DecRefQueue
+        internal class DecRefQueue : IDecRefQueue
         {
             public override void IncRef(Context ctx, IntPtr obj)
             {

src/api/dotnet/Goal.cs

@@ -209,7 +209,7 @@ namespace Microsoft.Z3
             Contract.Requires(ctx != null);
         }
 
-        internal class DecRefQueue : Z3.DecRefQueue
+        internal class DecRefQueue : IDecRefQueue
         {
             public override void IncRef(Context ctx, IntPtr obj)
             {

src/api/dotnet/IDecRefQueue.cs

@@ -26,7 +26,7 @@ using System.Diagnostics.Contracts;
 namespace Microsoft.Z3
 {    
     [ContractClass(typeof(DecRefQueueContracts))]
-    internal abstract class DecRefQueue
+    internal abstract class IDecRefQueue
     {
         #region Object invariant
 
@@ -76,8 +76,8 @@ namespace Microsoft.Z3
         }
     }
 
-    [ContractClassFor(typeof(DecRefQueue))]
+    [ContractClassFor(typeof(IDecRefQueue))]
-    abstract class DecRefQueueContracts : DecRefQueue
+    abstract class DecRefQueueContracts : IDecRefQueue
     {
         public override void IncRef(Context ctx, IntPtr obj)
         {

src/api/dotnet/IntExpr.cs

@@ -0,0 +1,47 @@
+/*++
+Copyright (<c>) 2012 Microsoft Corporation
+
+Module Name:
+
+    IntExpr.cs
+
+Abstract:
+
+    Z3 Managed API: Int Expressions
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2012-11-23
+
+Notes:
+    
+--*/
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Z3
+{
+    /// <summary>
+    /// Int expressions
+    /// </summary>
+    public class IntExpr : ArithExpr
+    {
+        #region Internal
+        /// <summary> Constructor for IntExpr </summary>
+        internal protected IntExpr(Context ctx)
+            : base(ctx)
+        {
+            Contract.Requires(ctx != null);
+        }
+        internal IntExpr(Context ctx, IntPtr obj)
+            : base(ctx, obj)
+        {
+            Contract.Requires(ctx != null);
+        }
+        #endregion
+    }
+}

src/api/dotnet/IntNum.cs

@@ -0,0 +1,121 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    IntNum.cs
+
+Abstract:
+
+    Z3 Managed API: Int Numerals
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2012-03-20
+
+Notes:
+    
+--*/
+using System;
+using System.Diagnostics.Contracts;
+
+#if !FRAMEWORK_LT_4
+using System.Numerics;
+#endif
+
+namespace Microsoft.Z3
+{
+    /// <summary>
+    /// Integer Numerals
+    /// </summary>
+    [ContractVerification(true)]
+    public class IntNum : IntExpr
+    {
+
+        #region Internal
+        internal IntNum(Context ctx, IntPtr obj)
+            : base(ctx, obj)
+        {
+            Contract.Requires(ctx != null);
+        }
+        #endregion
+
+
+        /// <summary>
+        /// Retrieve the 64-bit unsigned integer value.
+        /// </summary>
+        public UInt64 UInt64
+        {
+            get
+            {
+                UInt64 res = 0;
+                if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == 0)
+                    throw new Z3Exception("Numeral is not a 64 bit unsigned");
+                return res;
+            }
+        }
+
+        /// <summary>
+        /// Retrieve the int value.
+        /// </summary>
+        public int Int
+        {
+            get
+            {
+                int res = 0;
+                if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == 0)
+                    throw new Z3Exception("Numeral is not an int");
+                return res;
+            }
+        }
+
+        /// <summary>
+        /// Retrieve the 64-bit int value.
+        /// </summary>
+        public Int64 Int64
+        {
+            get
+            {
+                Int64 res = 0;
+                if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == 0)
+                    throw new Z3Exception("Numeral is not an int64");
+                return res;
+            }
+        }
+
+        /// <summary>
+        /// Retrieve the int value.
+        /// </summary>
+        public uint UInt
+        {
+            get
+            {
+                uint res = 0;
+                if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == 0)
+                    throw new Z3Exception("Numeral is not a uint");
+                return res;
+            }
+        }
+
+#if !FRAMEWORK_LT_4
+        /// <summary>
+        /// Retrieve the BigInteger value.
+        /// </summary>
+        public BigInteger BigInteger
+        {
+            get
+            {
+                return BigInteger.Parse(this.ToString());
+            }
+        }
+#endif
+
+        /// <summary>
+        /// Returns a string representation of the numeral.
+        /// </summary>        
+        public override string ToString()
+        {
+            return Native.Z3_get_numeral_string(Context.nCtx, NativeObject);
+        }
+    }
+}

src/api/dotnet/IntSort.cs

@@ -0,0 +1,43 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    IntSort.cs
+
+Abstract:
+
+    Z3 Managed API: Int Sorts
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2012-11-23
+
+Notes:
+    
+--*/
+
+using System;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Z3
+{
+    /// <summary>
+    ///  An Integer sort
+    /// </summary>
+    public class IntSort : ArithSort
+    {
+        #region Internal
+        internal IntSort(Context ctx, IntPtr obj)
+            : base(ctx, obj)
+        {
+            Contract.Requires(ctx != null);
+        }
+        internal IntSort(Context ctx)
+            : base(ctx, Native.Z3_mk_int_sort(ctx.nCtx))
+        {
+            Contract.Requires(ctx != null);
+        }
+        #endregion
+    }
+}

src/api/dotnet/IntSymbol.cs

@@ -0,0 +1,68 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    IntSymbol.cs
+
+Abstract:
+
+    Z3 Managed API: Int Symbols
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2012-11-23
+
+Notes:
+    
+--*/
+
+using System;
+using System.Runtime.InteropServices;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Z3
+{
+    /// <summary>
+    /// Numbered symbols
+    /// </summary>
+    [ContractVerification(true)]
+    public class IntSymbol : Symbol
+    {
+        /// <summary>
+        /// The int value of the symbol.
+        /// </summary>
+        /// <remarks>Throws an exception if the symbol is not of int kind. </remarks>
+        public int Int
+        {
+            get
+            {
+                if (!IsIntSymbol())
+                    throw new Z3Exception("Int requested from non-Int symbol");
+                return Native.Z3_get_symbol_int(Context.nCtx, NativeObject);
+            }
+        }
+
+        #region Internal
+        internal IntSymbol(Context ctx, IntPtr obj)
+            : base(ctx, obj)
+        {
+            Contract.Requires(ctx != null);
+        }
+        internal IntSymbol(Context ctx, int i)
+            : base(ctx, Native.Z3_mk_int_symbol(ctx.nCtx, i))
+        {
+            Contract.Requires(ctx != null);
+        }
+
+#if DEBUG
+        internal override void CheckNativeObject(IntPtr obj)
+        {
+            if ((Z3_symbol_kind)Native.Z3_get_symbol_kind(Context.nCtx, obj) != Z3_symbol_kind.Z3_INT_SYMBOL)
+                throw new Z3Exception("Symbol is not of integer kind");
+            base.CheckNativeObject(obj);
+        }
+#endif
+        #endregion
+    }
+}

src/api/dotnet/ListSort.cs

@@ -0,0 +1,163 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    ListSort.cs
+
+Abstract:
+
+    Z3 Managed API: List Sorts
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2012-11-23
+
+Notes:
+    
+--*/
+
+using System;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Z3
+{
+    /// <summary>
+    /// List sorts.
+    /// </summary>
+    [ContractVerification(true)]
+    public class ListSort : Sort
+    {
+        /// <summary>
+        /// The declaration of the nil function of this list sort.
+        /// </summary>
+        public FuncDecl NilDecl
+        {
+            get
+            {
+                Contract.Ensures(Contract.Result<FuncDecl>() != null);
+                return nilDecl;
+            }
+        }
+
+        /// <summary>
+        /// The empty list.
+        /// </summary>
+        public Expr Nil
+        {
+            get
+            {
+                Contract.Ensures(Contract.Result<Expr>() != null);
+                return nilConst;
+            }
+        }
+
+        /// <summary>
+        /// The declaration of the isNil function of this list sort.
+        /// </summary>
+        public FuncDecl IsNilDecl
+        {
+            get
+            {
+                Contract.Ensures(Contract.Result<FuncDecl>() != null);
+                return isNilDecl;
+            }
+        }
+
+        /// <summary>
+        /// The declaration of the cons function of this list sort.
+        /// </summary>
+        public FuncDecl ConsDecl
+        {
+            get
+            {
+                Contract.Ensures(Contract.Result<FuncDecl>() != null);
+                return consDecl;
+            }
+        }
+
+        /// <summary>
+        /// The declaration of the isCons function of this list sort.
+        /// </summary>
+        /// 
+        public FuncDecl IsConsDecl
+        {
+            get
+            {
+                Contract.Ensures(Contract.Result<FuncDecl>() != null);
+                return isConsDecl;
+            }
+        }
+
+        /// <summary>
+        /// The declaration of the head function of this list sort.
+        /// </summary>
+        public FuncDecl HeadDecl
+        {
+            get
+            {
+                Contract.Ensures(Contract.Result<FuncDecl>() != null);
+                return headDecl;
+            }
+        }
+
+        /// <summary>
+        /// The declaration of the tail function of this list sort.
+        /// </summary>
+        public FuncDecl TailDecl
+        {
+            get
+            {
+                Contract.Ensures(Contract.Result<FuncDecl>() != null);
+                return tailDecl;
+            }
+        }
+
+        #region Object Invariant
+
+        [ContractInvariantMethod]
+        private void ObjectInvariant()
+        {
+            Contract.Invariant(nilConst != null);
+            Contract.Invariant(nilDecl != null);
+            Contract.Invariant(isNilDecl != null);
+            Contract.Invariant(consDecl != null);
+            Contract.Invariant(isConsDecl != null);
+            Contract.Invariant(headDecl != null);
+            Contract.Invariant(tailDecl != null);
+        }
+
+
+        #endregion
+
+        #region Internal
+        readonly private FuncDecl nilDecl, isNilDecl, consDecl, isConsDecl, headDecl, tailDecl;
+        readonly private Expr nilConst;
+
+        internal ListSort(Context ctx, Symbol name, Sort elemSort)
+            : base(ctx)
+        {
+            Contract.Requires(ctx != null);
+            Contract.Requires(name != null);
+            Contract.Requires(elemSort != null);
+
+            IntPtr inil = IntPtr.Zero,
+                   iisnil = IntPtr.Zero,
+                   icons = IntPtr.Zero,
+                   iiscons = IntPtr.Zero,
+                   ihead = IntPtr.Zero,
+                   itail = IntPtr.Zero;
+
+            NativeObject = Native.Z3_mk_list_sort(ctx.nCtx, name.NativeObject, elemSort.NativeObject,
+                                                  ref inil, ref iisnil, ref icons, ref iiscons, ref ihead, ref itail);
+            nilDecl = new FuncDecl(ctx, inil);
+            isNilDecl = new FuncDecl(ctx, iisnil);
+            consDecl = new FuncDecl(ctx, icons);
+            isConsDecl = new FuncDecl(ctx, iiscons);
+            headDecl = new FuncDecl(ctx, ihead);
+            tailDecl = new FuncDecl(ctx, itail);
+            nilConst = ctx.MkConst(nilDecl);
+        }
+        #endregion
+    };
+}

src/api/dotnet/Microsoft.Z3.csproj

@@ -258,29 +258,56 @@
     <Reference Include="System.Numerics" />
   </ItemGroup>
   <ItemGroup>
+    <Compile Include="AlgebraicNum.cs" />
     <Compile Include="ApplyResult.cs" />
+    <Compile Include="ArithExpr.cs" />
+    <Compile Include="ArithSort.cs" />
+    <Compile Include="ArrayExpr.cs" />
+    <Compile Include="ArraySort.cs" />
     <Compile Include="AST.cs" />
     <Compile Include="ASTMap.cs" />
     <Compile Include="ASTVector.cs" />
+    <Compile Include="BitVecExpr.cs" />
+    <Compile Include="BitVecNum.cs" />
+    <Compile Include="BitVecSort.cs" />
+    <Compile Include="BoolExpr.cs" />
+    <Compile Include="BoolSort.cs" />
     <Compile Include="Constructor.cs" />
-    <Compile Include="DecRefQueue.cs" />
+    <Compile Include="ConstructorList.cs" />
+    <Compile Include="DatatypeExpr.cs" />
+    <Compile Include="DatatypeSort.cs" />
+    <Compile Include="IDecRefQueue.cs" />
     <Compile Include="Enumerations.cs" />
+    <Compile Include="EnumSort.cs" />
     <Compile Include="Expr.cs" />
+    <Compile Include="FiniteDomainSort.cs" />
     <Compile Include="Fixedpoint.cs" />
     <Compile Include="FuncDecl.cs" />
     <Compile Include="FuncInterp.cs" />
     <Compile Include="Goal.cs" />
+    <Compile Include="IntExpr.cs" />
+    <Compile Include="IntNum.cs" />
+    <Compile Include="IntSort.cs" />
+    <Compile Include="IntSymbol.cs" />
+    <Compile Include="ListSort.cs" />
     <Compile Include="Model.cs" />
-    <Compile Include="Numeral.cs" />
     <Compile Include="Params.cs" />
     <Compile Include="ParamDescrs.cs" />
     <Compile Include="Pattern.cs" />
+    <Compile Include="RatNum.cs" />
+    <Compile Include="RealExpr.cs" />
+    <Compile Include="RealSort.cs" />
+    <Compile Include="RelationSort.cs" />
+    <Compile Include="SetSort.cs" />
     <Compile Include="Statistics.cs" />
     <Compile Include="Status.cs" />
     <Compile Include="Context.cs" />
     <Compile Include="Probe.cs" />
     <Compile Include="Solver.cs" />
+    <Compile Include="StringSymbol.cs" />
     <Compile Include="Tactic.cs" />
+    <Compile Include="TupleSort.cs" />
+    <Compile Include="UninterpretedSort.cs" />
     <Compile Include="Z3Exception.cs" />
     <Compile Include="Log.cs" />
     <Compile Include="Native.cs" />

src/api/dotnet/Microsoft.Z3_35.csproj

@@ -1,403 +0,0 @@
-<?xml version="1.0" encoding="utf-8"?>
-<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
-  <PropertyGroup>
-    <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
-    <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
-    <ProductVersion>8.0.30703</ProductVersion>
-    <SchemaVersion>2.0</SchemaVersion>
-    <ProjectGuid>{EC3DB697-B734-42F7-9468-5B62821EEB5A}</ProjectGuid>
-    <OutputType>Library</OutputType>
-    <AppDesignerFolder>Properties</AppDesignerFolder>
-    <RootNamespace>Microsoft.Z3</RootNamespace>
-    <AssemblyName>Microsoft.Z3</AssemblyName>
-    <TargetFrameworkVersion>v3.5</TargetFrameworkVersion>
-    <FileAlignment>512</FileAlignment>
-    <TargetFrameworkProfile>Client</TargetFrameworkProfile>
-    <CodeContractsAssemblyMode>0</CodeContractsAssemblyMode>
-  </PropertyGroup>
-  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
-    <DebugSymbols>true</DebugSymbols>
-    <DebugType>full</DebugType>
-    <Optimize>false</Optimize>
-    <OutputPath>bin35\Debug\</OutputPath>
-    <DefineConstants>DEBUG;TRACE</DefineConstants>
-    <ErrorReport>prompt</ErrorReport>
-    <WarningLevel>4</WarningLevel>
-    <AllowUnsafeBlocks>true</AllowUnsafeBlocks>
-    <DocumentationFile>
-    </DocumentationFile>
-    <CodeContractsEnableRuntimeChecking>False</CodeContractsEnableRuntimeChecking>
-    <CodeContractsRuntimeOnlyPublicSurface>False</CodeContractsRuntimeOnlyPublicSurface>
-    <CodeContractsRuntimeThrowOnFailure>True</CodeContractsRuntimeThrowOnFailure>
-    <CodeContractsRuntimeCallSiteRequires>False</CodeContractsRuntimeCallSiteRequires>
-    <CodeContractsRuntimeSkipQuantifiers>False</CodeContractsRuntimeSkipQuantifiers>
-    <CodeContractsRunCodeAnalysis>True</CodeContractsRunCodeAnalysis>
-    <CodeContractsNonNullObligations>False</CodeContractsNonNullObligations>
-    <CodeContractsBoundsObligations>True</CodeContractsBoundsObligations>
-    <CodeContractsArithmeticObligations>True</CodeContractsArithmeticObligations>
-    <CodeContractsEnumObligations>False</CodeContractsEnumObligations>
-    <CodeContractsPointerObligations>False</CodeContractsPointerObligations>
-    <CodeContractsRedundantAssumptions>False</CodeContractsRedundantAssumptions>
-    <CodeContractsInferRequires>True</CodeContractsInferRequires>
-    <CodeContractsInferEnsures>False</CodeContractsInferEnsures>
-    <CodeContractsInferObjectInvariants>False</CodeContractsInferObjectInvariants>
-    <CodeContractsSuggestAssumptions>False</CodeContractsSuggestAssumptions>
-    <CodeContractsSuggestRequires>True</CodeContractsSuggestRequires>
-    <CodeContractsSuggestEnsures>False</CodeContractsSuggestEnsures>
-    <CodeContractsSuggestObjectInvariants>False</CodeContractsSuggestObjectInvariants>
-    <CodeContractsDisjunctiveRequires>True</CodeContractsDisjunctiveRequires>
-    <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
-    <CodeContractsShowSquigglies>True</CodeContractsShowSquigglies>
-    <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
-    <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
-    <CodeContractsCustomRewriterAssembly />
-    <CodeContractsCustomRewriterClass />
-    <CodeContractsLibPaths />
-    <CodeContractsExtraRewriteOptions />
-    <CodeContractsExtraAnalysisOptions />
-    <CodeContractsBaseLineFile />
-    <CodeContractsCacheAnalysisResults>True</CodeContractsCacheAnalysisResults>
-    <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
-    <CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>
-    <CodeContractsAnalysisWarningLevel>2</CodeContractsAnalysisWarningLevel>
-  </PropertyGroup>
-  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
-    <DebugType>pdbonly</DebugType>
-    <Optimize>true</Optimize>
-    <OutputPath>bin35\external\bin\</OutputPath>
-    <DefineConstants>FRAMEWORK_LT_4</DefineConstants>
-    <ErrorReport>prompt</ErrorReport>
-    <WarningLevel>4</WarningLevel>
-    <AllowUnsafeBlocks>true</AllowUnsafeBlocks>
-    <DocumentationFile>..\external\Microsoft.Z3.xml</DocumentationFile>
-  </PropertyGroup>
-  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'external|AnyCPU' ">
-    <OutputPath>bin35\external\bin\</OutputPath>
-    <AllowUnsafeBlocks>true</AllowUnsafeBlocks>
-    <DocumentationFile>..\external\Microsoft.Z3.xml</DocumentationFile>
-    <Optimize>true</Optimize>
-    <DebugType>pdbonly</DebugType>
-    <PlatformTarget>AnyCPU</PlatformTarget>
-    <CodeAnalysisLogFile>bin\Release\Microsoft.Z3.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>
-    <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
-    <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
-    <ErrorReport>prompt</ErrorReport>
-    <CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
-    <CodeAnalysisRuleSetDirectories>;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
-    <CodeAnalysisIgnoreBuiltInRuleSets>true</CodeAnalysisIgnoreBuiltInRuleSets>
-    <CodeAnalysisRuleDirectories>;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
-    <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
-    <CodeAnalysisFailOnMissingRules>false</CodeAnalysisFailOnMissingRules>
-    <DefineConstants>FRAMEWORK_LT_4</DefineConstants>
-  </PropertyGroup>
-  <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'external|Win32' ">
-    <OutputPath>bin35\external\bin\</OutputPath>
-    <AllowUnsafeBlocks>true</AllowUnsafeBlocks>
-    <DocumentationFile>..\external\Microsoft.Z3.xml</DocumentationFile>
-    <Optimize>true</Optimize>
-    <DebugType>pdbonly</DebugType>
-    <PlatformTarget>AnyCPU</PlatformTarget>
-    <CodeAnalysisLogFile>bin\Release\Microsoft.Z3.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>
-    <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
-    <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
-    <ErrorReport>prompt</ErrorReport>
-    <CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
-    <CodeAnalysisRuleSetDirectories>;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
-    <CodeAnalysisIgnoreBuiltInRuleSets>true</CodeAnalysisIgnoreBuiltInRuleSets>
-    <CodeAnalysisRuleDirectories>;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
-    <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
-    <CodeAnalysisFailOnMissingRules>false</CodeAnalysisFailOnMissingRules>
-    <DefineConstants>FRAMEWORK_LT_4</DefineConstants>
-  </PropertyGroup>
-  <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Debug|x64'">
-    <DebugSymbols>true</DebugSymbols>
-    <OutputPath>bin35\x64\Debug\</OutputPath>
-    <DefineConstants>DEBUG;TRACE</DefineConstants>
-    <AllowUnsafeBlocks>true</AllowUnsafeBlocks>
-    <DebugType>full</DebugType>
-    <PlatformTarget>x64</PlatformTarget>
-    <CodeAnalysisLogFile>..\Debug\Microsoft.Z3.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>
-    <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
-    <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
-    <ErrorReport>prompt</ErrorReport>
-    <CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
-    <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
-    <CodeAnalysisIgnoreBuiltInRuleSets>true</CodeAnalysisIgnoreBuiltInRuleSets>
-    <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
-    <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
-    <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>
-    <CodeContractsInferRequires>False</CodeContractsInferRequires>
-    <CodeContractsInferEnsures>False</CodeContractsInferEnsures>
-    <CodeContractsInferObjectInvariants>False</CodeContractsInferObjectInvariants>
-    <CodeContractsSuggestAssumptions>False</CodeContractsSuggestAssumptions>
-    <CodeContractsSuggestRequires>True</CodeContractsSuggestRequires>
-    <CodeContractsSuggestEnsures>False</CodeContractsSuggestEnsures>
-    <CodeContractsSuggestObjectInvariants>False</CodeContractsSuggestObjectInvariants>
-    <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>%28none%29</CodeContractsReferenceAssembly>
-    <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
-  </PropertyGroup>
-  <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Release|x64'">
-    <OutputPath>bin35\external\x64\</OutputPath>
-    <AllowUnsafeBlocks>true</AllowUnsafeBlocks>
-    <DocumentationFile>..\x64\external_64\Microsoft.Z3.xml</DocumentationFile>
-    <Optimize>true</Optimize>
-    <DebugType>pdbonly</DebugType>
-    <PlatformTarget>x64</PlatformTarget>
-    <CodeAnalysisLogFile>..\release\Microsoft.Z3.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>
-    <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
-    <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
-    <ErrorReport>prompt</ErrorReport>
-    <CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
-    <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
-    <CodeAnalysisIgnoreBuiltInRuleSets>true</CodeAnalysisIgnoreBuiltInRuleSets>
-    <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>True</CodeContractsRunCodeAnalysis>
-    <CodeContractsNonNullObligations>True</CodeContractsNonNullObligations>
-    <CodeContractsBoundsObligations>True</CodeContractsBoundsObligations>
-    <CodeContractsArithmeticObligations>False</CodeContractsArithmeticObligations>
-    <CodeContractsEnumObligations>False</CodeContractsEnumObligations>
-    <CodeContractsPointerObligations>False</CodeContractsPointerObligations>
-    <CodeContractsRedundantAssumptions>True</CodeContractsRedundantAssumptions>
-    <CodeContractsInferRequires>True</CodeContractsInferRequires>
-    <CodeContractsInferEnsures>False</CodeContractsInferEnsures>
-    <CodeContractsInferObjectInvariants>False</CodeContractsInferObjectInvariants>
-    <CodeContractsSuggestAssumptions>False</CodeContractsSuggestAssumptions>
-    <CodeContractsSuggestRequires>True</CodeContractsSuggestRequires>
-    <CodeContractsSuggestEnsures>False</CodeContractsSuggestEnsures>
-    <CodeContractsSuggestObjectInvariants>False</CodeContractsSuggestObjectInvariants>
-    <CodeContractsRunInBackground>True</CodeContractsRunInBackground>
-    <CodeContractsShowSquigglies>True</CodeContractsShowSquigglies>
-    <CodeContractsUseBaseLine>False</CodeContractsUseBaseLine>
-    <CodeContractsEmitXMLDocs>False</CodeContractsEmitXMLDocs>
-    <CodeContractsCustomRewriterAssembly />
-    <CodeContractsCustomRewriterClass />
-    <CodeContractsLibPaths />
-    <CodeContractsExtraRewriteOptions />
-    <CodeContractsExtraAnalysisOptions>-repro</CodeContractsExtraAnalysisOptions>
-    <CodeContractsBaseLineFile />
-    <CodeContractsCacheAnalysisResults>True</CodeContractsCacheAnalysisResults>
-    <CodeContractsRuntimeCheckingLevel>Full</CodeContractsRuntimeCheckingLevel>
-    <CodeContractsReferenceAssembly>%28none%29</CodeContractsReferenceAssembly>
-    <CodeContractsAnalysisWarningLevel>2</CodeContractsAnalysisWarningLevel>
-  </PropertyGroup>
-  <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'external|x64'">
-    <OutputPath>bin35\external\x64</OutputPath>
-    <AllowUnsafeBlocks>true</AllowUnsafeBlocks>
-    <DocumentationFile>..\external\Microsoft.Z3.xml</DocumentationFile>
-    <Optimize>true</Optimize>
-    <DebugType>pdbonly</DebugType>
-    <PlatformTarget>x64</PlatformTarget>
-    <CodeAnalysisLogFile>bin\Release\Microsoft.Z3.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>
-    <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
-    <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
-    <ErrorReport>prompt</ErrorReport>
-    <CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
-    <CodeAnalysisRuleSetDirectories>;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
-    <CodeAnalysisIgnoreBuiltInRuleSets>true</CodeAnalysisIgnoreBuiltInRuleSets>
-    <CodeAnalysisRuleDirectories>;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
-    <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
-  </PropertyGroup>
-  <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'external_64|AnyCPU'">
-    <OutputPath>bin35\external_64\x64</OutputPath>
-    <AllowUnsafeBlocks>true</AllowUnsafeBlocks>
-    <DocumentationFile>..\x64\external_64\Microsoft.Z3.xml</DocumentationFile>
-    <DefineConstants>FRAMEWORK_LT_4</DefineConstants>
-    <Optimize>true</Optimize>
-    <DebugType>pdbonly</DebugType>
-    <PlatformTarget>AnyCPU</PlatformTarget>
-    <CodeAnalysisLogFile>bin\Release\Microsoft.Z3.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>
-    <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
-    <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
-    <ErrorReport>prompt</ErrorReport>
-    <CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
-    <CodeAnalysisRuleSetDirectories>;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
-    <CodeAnalysisIgnoreBuiltInRuleSets>true</CodeAnalysisIgnoreBuiltInRuleSets>
-    <CodeAnalysisRuleDirectories>;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
-    <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
-    <CodeAnalysisFailOnMissingRules>false</CodeAnalysisFailOnMissingRules>
-  </PropertyGroup>
-  <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'external_64|x64'">
-    <OutputPath>bin35\external_64\x64</OutputPath>
-    <AllowUnsafeBlocks>true</AllowUnsafeBlocks>
-    <DocumentationFile>..\x64\external_64\Microsoft.Z3.xml</DocumentationFile>
-    <Optimize>true</Optimize>
-    <DebugType>pdbonly</DebugType>
-    <PlatformTarget>x64</PlatformTarget>
-    <CodeAnalysisLogFile>bin\Release\Microsoft.Z3.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>
-    <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
-    <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
-    <ErrorReport>prompt</ErrorReport>
-    <CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
-    <CodeAnalysisRuleSetDirectories>;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
-    <CodeAnalysisIgnoreBuiltInRuleSets>true</CodeAnalysisIgnoreBuiltInRuleSets>
-    <CodeAnalysisRuleDirectories>;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
-    <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
-    <CodeAnalysisFailOnMissingRules>false</CodeAnalysisFailOnMissingRules>
-    <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>
-    <CodeContractsInferRequires>False</CodeContractsInferRequires>
-    <CodeContractsInferEnsures>False</CodeContractsInferEnsures>
-    <CodeContractsInferObjectInvariants>False</CodeContractsInferObjectInvariants>
-    <CodeContractsSuggestAssumptions>False</CodeContractsSuggestAssumptions>
-    <CodeContractsSuggestRequires>True</CodeContractsSuggestRequires>
-    <CodeContractsSuggestEnsures>False</CodeContractsSuggestEnsures>
-    <CodeContractsSuggestObjectInvariants>False</CodeContractsSuggestObjectInvariants>
-    <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>%28none%29</CodeContractsReferenceAssembly>
-    <CodeContractsAnalysisWarningLevel>0</CodeContractsAnalysisWarningLevel>
-    <DefineConstants>FRAMEWORK_LT_4</DefineConstants>
-  </PropertyGroup>
-  <PropertyGroup>
-    <SignAssembly>true</SignAssembly>
-  </PropertyGroup>
-  <PropertyGroup>
-    <AssemblyOriginatorKeyFile>z3.snk</AssemblyOriginatorKeyFile>
-  </PropertyGroup>
-  <PropertyGroup>
-    <DelaySign>false</DelaySign>
-  </PropertyGroup>
-  <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Release_delaysign|AnyCPU'">
-    <OutputPath>bin35\Release_delaysign\</OutputPath>
-    <AllowUnsafeBlocks>true</AllowUnsafeBlocks>
-    <DocumentationFile>..\Release_delaysign\Microsoft.Z3.xml</DocumentationFile>
-    <Optimize>true</Optimize>
-    <DebugType>pdbonly</DebugType>
-    <PlatformTarget>AnyCPU</PlatformTarget>
-    <CodeAnalysisLogFile>..\release\Microsoft.Z3.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>
-    <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
-    <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
-    <ErrorReport>prompt</ErrorReport>
-    <CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
-    <CodeAnalysisRuleSetDirectories>;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
-    <CodeAnalysisIgnoreBuiltInRuleSets>true</CodeAnalysisIgnoreBuiltInRuleSets>
-    <CodeAnalysisRuleDirectories>;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
-    <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
-    <DefineConstants>DELAYSIGN</DefineConstants>
-  </PropertyGroup>
-  <PropertyGroup Condition="'$(Configuration)|$(Platform)' == 'Release_delaysign|x64'">
-    <OutputPath>bin\x64\Release_delaysign\</OutputPath>
-    <AllowUnsafeBlocks>true</AllowUnsafeBlocks>
-    <DocumentationFile>..\x64\external_64\Microsoft.Z3.xml</DocumentationFile>
-    <Optimize>true</Optimize>
-    <DebugType>pdbonly</DebugType>
-    <PlatformTarget>x64</PlatformTarget>
-    <CodeAnalysisLogFile>..\release\Microsoft.Z3.dll.CodeAnalysisLog.xml</CodeAnalysisLogFile>
-    <CodeAnalysisUseTypeNameInSuppression>true</CodeAnalysisUseTypeNameInSuppression>
-    <CodeAnalysisModuleSuppressionsFile>GlobalSuppressions.cs</CodeAnalysisModuleSuppressionsFile>
-    <ErrorReport>prompt</ErrorReport>
-    <CodeAnalysisRuleSet>MinimumRecommendedRules.ruleset</CodeAnalysisRuleSet>
-    <CodeAnalysisRuleSetDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\\Rule Sets</CodeAnalysisRuleSetDirectories>
-    <CodeAnalysisIgnoreBuiltInRuleSets>true</CodeAnalysisIgnoreBuiltInRuleSets>
-    <CodeAnalysisRuleDirectories>;C:\Program Files (x86)\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules;C:\Program Files\Microsoft Visual Studio 10.0\Team Tools\Static Analysis Tools\FxCop\\Rules</CodeAnalysisRuleDirectories>
-    <CodeAnalysisIgnoreBuiltInRules>true</CodeAnalysisIgnoreBuiltInRules>
-  </PropertyGroup>
-  <ItemGroup>
-    <Reference Include="Microsoft.Contracts, Version=1.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
-      <SpecificVersion>False</SpecificVersion>
-      <HintPath>..\..\..\..\Program Files\Microsoft\Contracts\Contracts\v3.5\Microsoft.Contracts.dll</HintPath>
-    </Reference>
-    <Reference Include="System" />
-    <Reference Include="System.Core" />
-  </ItemGroup>
-  <ItemGroup>
-    <Compile Include="ApplyResult.cs" />
-    <Compile Include="AST.cs" />
-    <Compile Include="ASTMap.cs" />
-    <Compile Include="ASTVector.cs" />
-    <Compile Include="Constructor.cs" />
-    <Compile Include="DecRefQueue.cs" />
-    <Compile Include="Enumerations.cs" />
-    <Compile Include="Expr.cs" />
-    <Compile Include="Fixedpoint.cs" />
-    <Compile Include="FuncDecl.cs" />
-    <Compile Include="FuncInterp.cs" />
-    <Compile Include="Goal.cs" />
-    <Compile Include="Model.cs" />
-    <Compile Include="Numeral.cs" />
-    <Compile Include="Params.cs" />
-    <Compile Include="Pattern.cs" />
-    <Compile Include="Statistics.cs" />
-    <Compile Include="Status.cs" />
-    <Compile Include="Context.cs" />
-    <Compile Include="Probe.cs" />
-    <Compile Include="Solver.cs" />
-    <Compile Include="Tactic.cs" />
-    <Compile Include="Z3Exception.cs" />
-    <Compile Include="Log.cs" />
-    <Compile Include="Native.cs" />
-    <Compile Include="Properties\AssemblyInfo.cs" />
-    <Compile Include="Quantifier.cs" />
-    <Compile Include="Sort.cs" />
-    <Compile Include="Symbol.cs" />
-    <Compile Include="Util.cs" />
-    <Compile Include="Version.cs" />
-    <Compile Include="Z3Object.cs" />
-  </ItemGroup>
-  <ItemGroup>
-    <WCFMetadata Include="Service References\" />
-  </ItemGroup>
-  <ItemGroup>
-    <None Include="z3.snk" />
-  </ItemGroup>
-  <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />
-  <PropertyGroup>
-    <PostBuildEvent>
-    </PostBuildEvent>
-  </PropertyGroup>
-  <!-- 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>

src/api/dotnet/Model.cs

@@ -289,7 +289,7 @@ namespace Microsoft.Z3
             Contract.Requires(ctx != null);
         }
 
-        internal class DecRefQueue : Z3.DecRefQueue
+        internal class DecRefQueue : IDecRefQueue
         {
             public override void IncRef(Context ctx, IntPtr obj)
             {

src/api/dotnet/Numeral.cs

@@ -1,344 +0,0 @@
-/*++
-Copyright (c) 2012 Microsoft Corporation
-
-Module Name:
-
-    Numeral.cs
-
-Abstract:
-
-    Z3 Managed API: Numerals
-
-Author:
-
-    Christoph Wintersteiger (cwinter) 2012-03-20
-
-Notes:
-    
---*/
-using System;
-using System.Diagnostics.Contracts;
-
-#if !FRAMEWORK_LT_4
-using System.Numerics;
-#endif
-
-namespace Microsoft.Z3
-{
-    /// <summary>
-    /// Integer Numerals
-    /// </summary>
-    [ContractVerification(true)]
-    public class IntNum : IntExpr
-    {
-
-        #region Internal
-        internal IntNum(Context ctx, IntPtr obj)
-            : base(ctx, obj)
-        {
-            Contract.Requires(ctx != null);
-        }
-        #endregion
-
-
-        /// <summary>
-        /// Retrieve the 64-bit unsigned integer value.
-        /// </summary>
-        public UInt64 UInt64
-        {
-            get
-            {
-                UInt64 res = 0;
-                if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == 0)
-                    throw new Z3Exception("Numeral is not a 64 bit unsigned");
-                return res;
-            }
-        }
-
-        /// <summary>
-        /// Retrieve the int value.
-        /// </summary>
-        public int Int
-        {
-            get
-            {
-                int res = 0;
-                if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == 0)
-                    throw new Z3Exception("Numeral is not an int");
-                return res;
-            }
-        }
-
-        /// <summary>
-        /// Retrieve the 64-bit int value.
-        /// </summary>
-        public Int64 Int64
-        {
-            get
-            {
-                Int64 res = 0;
-                if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == 0)
-                    throw new Z3Exception("Numeral is not an int64");
-                return res;
-            }
-        }
-
-        /// <summary>
-        /// Retrieve the int value.
-        /// </summary>
-        public uint UInt
-        {
-            get
-            {
-                uint res = 0;
-                if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == 0)
-                    throw new Z3Exception("Numeral is not a uint");
-                return res;
-            }
-        }
-
-#if !FRAMEWORK_LT_4
-        /// <summary>
-        /// Retrieve the BigInteger value.
-        /// </summary>
-        public BigInteger BigInteger
-        {
-            get
-            {  
-                return BigInteger.Parse(this.ToString());
-            }
-        }
-#endif
-
-        /// <summary>
-        /// Returns a string representation of the numeral.
-        /// </summary>        
-        public override string ToString()
-        {
-            return Native.Z3_get_numeral_string(Context.nCtx, NativeObject);
-        }
-    }
-
-    /// <summary>
-    /// Rational Numerals
-    /// </summary>
-    [ContractVerification(true)]
-    public class RatNum : RealExpr
-    {
-        /// <summary>
-        /// The numerator of a rational numeral.
-        /// </summary>
-        public IntNum Numerator
-        {
-            get {
-                Contract.Ensures(Contract.Result<IntNum>() != null);
-
-                return new IntNum(Context, Native.Z3_get_numerator(Context.nCtx, NativeObject)); }
-        }
-
-        /// <summary>
-        /// The denominator of a rational numeral.
-        /// </summary>
-        public IntNum Denominator
-        {
-            get {
-                Contract.Ensures(Contract.Result<IntNum>() != null);
-
-                return new IntNum(Context, Native.Z3_get_denominator(Context.nCtx, NativeObject)); }
-        }
-
-#if !FRAMEWORK_LT_4
-        /// <summary>
-        /// Converts the numerator of the rational to a BigInteger
-        /// </summary>
-        public BigInteger BigIntNumerator
-        {
-            get
-            {                
-                IntNum n = Numerator;
-                return BigInteger.Parse(n.ToString());
-            }
-        }
-
-        /// <summary>
-        /// Converts the denominator of the rational to a BigInteger
-        /// </summary>
-        public BigInteger BigIntDenominator
-        {
-            get
-            {
-                IntNum n = Denominator;
-                return BigInteger.Parse(n.ToString());
-            }
-        }
-#endif
-
-        /// <summary>
-        /// Returns a string representation in decimal notation.
-        /// </summary>
-        /// <remarks>The result has at most <paramref name="precision"/> decimal places.</remarks>    
-        public string ToDecimalString(uint precision)
-        {
-            return Native.Z3_get_numeral_decimal_string(Context.nCtx, NativeObject, precision);
-        }
-
-        /// <summary>
-        /// Returns a string representation of the numeral.
-        /// </summary>        
-        public override string ToString()
-        {
-            return Native.Z3_get_numeral_string(Context.nCtx, NativeObject);
-        }
-
-        #region Internal
-        internal RatNum(Context ctx, IntPtr obj)
-            : base(ctx, obj)
-        {
-            Contract.Requires(ctx != null);
-        }
-        #endregion
-    }
-
-
-    /// <summary>
-    /// Bit-vector numerals
-    /// </summary>
-    [ContractVerification(true)]
-    public class BitVecNum : BitVecExpr
-    {
-        /// <summary>
-        /// Retrieve the 64-bit unsigned integer value.
-        /// </summary>
-        public UInt64 UInt64
-        {
-            get
-            {
-                UInt64 res = 0;
-                if (Native.Z3_get_numeral_uint64(Context.nCtx, NativeObject, ref res) == 0)
-                    throw new Z3Exception("Numeral is not a 64 bit unsigned");
-                return res;
-            }
-        }
-
-        /// <summary>
-        /// Retrieve the int value.
-        /// </summary>
-        public int Int
-        {
-            get
-            {
-                int res = 0;
-                if (Native.Z3_get_numeral_int(Context.nCtx, NativeObject, ref res) == 0)
-                    throw new Z3Exception("Numeral is not an int");
-                return res;
-            }
-        }
-
-        /// <summary>
-        /// Retrieve the 64-bit int value.
-        /// </summary>
-        public Int64 Int64
-        {
-            get
-            {
-                Int64 res = 0;
-                if (Native.Z3_get_numeral_int64(Context.nCtx, NativeObject, ref res) == 0)
-                    throw new Z3Exception("Numeral is not an int64");
-                return res;
-            }
-        }
-
-        /// <summary>
-        /// Retrieve the int value.
-        /// </summary>
-        public uint UInt
-        {
-            get
-            {
-                uint res = 0;
-                if (Native.Z3_get_numeral_uint(Context.nCtx, NativeObject, ref res) == 0)
-                    throw new Z3Exception("Numeral is not a uint");
-                return res;
-            }
-        }
-
-#if !FRAMEWORK_LT_4
-        /// <summary>
-        /// Retrieve the BigInteger value.
-        /// </summary>
-        public BigInteger BigInteger
-        {
-            get
-            {
-                return BigInteger.Parse(this.ToString());
-            }
-        }
-#endif
-
-        /// <summary>
-        /// Returns a string representation of the numeral.
-        /// </summary>        
-        public override string ToString()
-        {
-            return Native.Z3_get_numeral_string(Context.nCtx, NativeObject);
-        }
-
-        #region Internal
-        internal BitVecNum(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
-        #endregion
-    }
-
-    /// <summary>
-    /// Algebraic numbers
-    /// </summary>
-    [ContractVerification(true)]
-    public class AlgebraicNum : ArithExpr
-    {
-        /// <summary>
-        /// Return a upper bound for a given real algebraic number. 
-        /// The interval isolating the number is smaller than 1/10^<paramref name="precision"/>.    
-        /// <seealso cref="Expr.IsAlgebraicNumber"/>   
-        /// </summary>
-        /// <param name="precision">the precision of the result</param>
-        /// <returns>A numeral Expr of sort Real</returns>
-        public RatNum ToUpper(uint precision)
-        {
-            Contract.Ensures(Contract.Result<RatNum>() != null);
-
-            return new RatNum(Context, Native.Z3_get_algebraic_number_upper(Context.nCtx, NativeObject, precision));
-        }
-
-        /// <summary>
-        /// Return a lower bound for the given real algebraic number. 
-        /// The interval isolating the number is smaller than 1/10^<paramref name="precision"/>.    
-        /// <seealso cref="Expr.IsAlgebraicNumber"/>
-        /// </summary>
-        /// <param name="precision"></param>
-        /// <returns>A numeral Expr of sort Real</returns>
-        public RatNum ToLower(uint precision)
-        {
-            Contract.Ensures(Contract.Result<RatNum>() != null);
-
-            return new RatNum(Context, Native.Z3_get_algebraic_number_lower(Context.nCtx, NativeObject, precision));
-        }
-
-        /// <summary>
-        /// Returns a string representation in decimal notation.
-        /// </summary>
-        /// <remarks>The result has at most <paramref name="precision"/> decimal places.</remarks>    
-        public string ToDecimal(uint precision)
-        {
-            Contract.Ensures(Contract.Result<string>() != null);
-
-            return Native.Z3_get_numeral_decimal_string(Context.nCtx, NativeObject, precision);
-        }
-
-        #region Internal
-        internal AlgebraicNum(Context ctx, IntPtr obj)
-            : base(ctx, obj)
-        {
-            Contract.Requires(ctx != null);
-        }
-        #endregion
-    }
-}

src/api/dotnet/ParamDescrs.cs

@@ -85,7 +85,7 @@ namespace Microsoft.Z3
             Contract.Requires(ctx != null);
         }
 
-        internal class DecRefQueue : Z3.DecRefQueue
+        internal class DecRefQueue : IDecRefQueue
         {
             public override void IncRef(Context ctx, IntPtr obj)
             {

src/api/dotnet/Params.cs

@@ -118,7 +118,7 @@ namespace Microsoft.Z3
             Contract.Requires(ctx != null);
         }
 
-        internal class DecRefQueue : Z3.DecRefQueue
+        internal class DecRefQueue : IDecRefQueue
         {
             public override void IncRef(Context ctx, IntPtr obj)
             {

src/api/dotnet/Probe.cs

@@ -49,10 +49,15 @@ namespace Microsoft.Z3
         /// <summary>
         /// Apply the probe to a goal.
         /// </summary>
-        public double this[Goal g] { get {
+        public double this[Goal g]
-            Contract.Requires(g != null);
+        {
+            get
+            {
+                Contract.Requires(g != null);
 
-            return Apply(g); } }
+                return Apply(g);
+            }
+        }
 
         #region Internal
         internal Probe(Context ctx, IntPtr obj)
@@ -66,7 +71,7 @@ namespace Microsoft.Z3
             Contract.Requires(ctx != null);
         }
 
-        internal class DecRefQueue : Z3.DecRefQueue
+        internal class DecRefQueue : IDecRefQueue
         {
             public override void IncRef(Context ctx, IntPtr obj)
             {

src/api/dotnet/Quantifier.cs

@@ -149,18 +149,17 @@ namespace Microsoft.Z3
         /// </summary>
         public BoolExpr Body
         {
-            get {
+            get
+            {
                 Contract.Ensures(Contract.Result<BoolExpr>() != null);
 
-                return new BoolExpr(Context, Native.Z3_get_quantifier_body(Context.nCtx, NativeObject)); }
+                return new BoolExpr(Context, Native.Z3_get_quantifier_body(Context.nCtx, NativeObject));
+            }
         }
 
         #region Internal
         [ContractVerification(false)] // F: Clousot ForAll decompilation gets confused below. Setting verification off until I fixed the bug
-        internal Quantifier(Context ctx, bool isForall, Sort[] sorts, Symbol[] names, Expr body,
+        internal Quantifier(Context ctx, bool isForall, Sort[] sorts, Symbol[] names, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
-                            uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null,
-                            Symbol quantifierID = null, Symbol skolemID = null
-                            )
             : base(ctx)
         {
             Contract.Requires(ctx != null);
@@ -187,7 +186,7 @@ namespace Microsoft.Z3
             if (noPatterns == null && quantifierID == null && skolemID == null)
             {
                 NativeObject = Native.Z3_mk_quantifier(ctx.nCtx, (isForall) ? 1 : 0, weight,
-                                           AST.ArrayLength(patterns),  AST.ArrayToNative(patterns),
+                                           AST.ArrayLength(patterns), AST.ArrayToNative(patterns),
                                            AST.ArrayLength(sorts), AST.ArrayToNative(sorts),
                                            Symbol.ArrayToNative(names),
                                            body.NativeObject);
@@ -205,10 +204,7 @@ namespace Microsoft.Z3
         }
 
         [ContractVerification(false)] // F: Clousot ForAll decompilation gets confused below. Setting verification off until I fixed the bug
-        internal Quantifier(Context ctx, bool isForall, Expr[] bound, Expr body,
+        internal Quantifier(Context ctx, bool isForall, Expr[] bound, Expr body, uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null, Symbol quantifierID = null, Symbol skolemID = null)
-                            uint weight = 1, Pattern[] patterns = null, Expr[] noPatterns = null,
-                            Symbol quantifierID = null, Symbol skolemID = null
-            )
             : base(ctx)
         {
             Contract.Requires(ctx != null);
@@ -244,14 +240,14 @@ namespace Microsoft.Z3
 
         internal Quantifier(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
 
-        #if DEBUG
+#if DEBUG
         internal override void CheckNativeObject(IntPtr obj)
         {
             if ((Z3_ast_kind)Native.Z3_get_ast_kind(Context.nCtx, obj) != Z3_ast_kind.Z3_QUANTIFIER_AST)
                 throw new Z3Exception("Underlying object is not a quantifier");
             base.CheckNativeObject(obj);
         }
-        #endif
+#endif
         #endregion
     }
 }

src/api/dotnet/RatNum.cs

@@ -0,0 +1,111 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    IntNum.cs
+
+Abstract:
+
+    Z3 Managed API: Int Numerals
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2012-03-20
+
+Notes:
+    
+--*/
+using System;
+using System.Diagnostics.Contracts;
+
+#if !FRAMEWORK_LT_4
+using System.Numerics;
+#endif
+
+namespace Microsoft.Z3
+{
+    /// <summary>
+    /// Rational Numerals
+    /// </summary>
+    [ContractVerification(true)]
+    public class RatNum : RealExpr
+    {
+        /// <summary>
+        /// The numerator of a rational numeral.
+        /// </summary>
+        public IntNum Numerator
+        {
+            get
+            {
+                Contract.Ensures(Contract.Result<IntNum>() != null);
+
+                return new IntNum(Context, Native.Z3_get_numerator(Context.nCtx, NativeObject));
+            }
+        }
+
+        /// <summary>
+        /// The denominator of a rational numeral.
+        /// </summary>
+        public IntNum Denominator
+        {
+            get
+            {
+                Contract.Ensures(Contract.Result<IntNum>() != null);
+
+                return new IntNum(Context, Native.Z3_get_denominator(Context.nCtx, NativeObject));
+            }
+        }
+
+#if !FRAMEWORK_LT_4
+        /// <summary>
+        /// Converts the numerator of the rational to a BigInteger
+        /// </summary>
+        public BigInteger BigIntNumerator
+        {
+            get
+            {
+                IntNum n = Numerator;
+                return BigInteger.Parse(n.ToString());
+            }
+        }
+
+        /// <summary>
+        /// Converts the denominator of the rational to a BigInteger
+        /// </summary>
+        public BigInteger BigIntDenominator
+        {
+            get
+            {
+                IntNum n = Denominator;
+                return BigInteger.Parse(n.ToString());
+            }
+        }
+#endif
+
+        /// <summary>
+        /// Returns a string representation in decimal notation.
+        /// </summary>
+        /// <remarks>The result has at most <paramref name="precision"/> decimal places.</remarks>    
+        public string ToDecimalString(uint precision)
+        {
+            return Native.Z3_get_numeral_decimal_string(Context.nCtx, NativeObject, precision);
+        }
+
+        /// <summary>
+        /// Returns a string representation of the numeral.
+        /// </summary>        
+        public override string ToString()
+        {
+            return Native.Z3_get_numeral_string(Context.nCtx, NativeObject);
+        }
+
+        #region Internal
+        internal RatNum(Context ctx, IntPtr obj)
+            : base(ctx, obj)
+        {
+            Contract.Requires(ctx != null);
+        }
+        #endregion
+    }
+}

src/api/dotnet/RealExpr.cs

@@ -0,0 +1,47 @@
+/*++
+Copyright (<c>) 2012 Microsoft Corporation
+
+Module Name:
+
+    RealExpr.cs
+
+Abstract:
+
+    Z3 Managed API: Real Expressions
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2012-11-23
+
+Notes:
+    
+--*/
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Z3
+{
+    /// <summary>
+    /// Real expressions
+    /// </summary>
+    public class RealExpr : ArithExpr
+    {
+        #region Internal
+        /// <summary> Constructor for RealExpr </summary>
+        internal protected RealExpr(Context ctx)
+            : base(ctx)
+        {
+            Contract.Requires(ctx != null);
+        }
+        internal RealExpr(Context ctx, IntPtr obj)
+            : base(ctx, obj)
+        {
+            Contract.Requires(ctx != null);
+        }
+        #endregion
+    }
+}

src/api/dotnet/RealSort.cs

@@ -0,0 +1,43 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    RealSort.cs
+
+Abstract:
+
+    Z3 Managed API: Real Sorts
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2012-11-23
+
+Notes:
+    
+--*/
+
+using System;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Z3
+{
+    /// <summary>
+    /// A real sort
+    /// </summary>
+    public class RealSort : ArithSort
+    {
+        #region Internal
+        internal RealSort(Context ctx, IntPtr obj)
+            : base(ctx, obj)
+        {
+            Contract.Requires(ctx != null);
+        }
+        internal RealSort(Context ctx)
+            : base(ctx, Native.Z3_mk_real_sort(ctx.nCtx))
+        {
+            Contract.Requires(ctx != null);
+        }
+        #endregion
+    }
+}

src/api/dotnet/RelationSort.cs

@@ -0,0 +1,69 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    RelationSort.cs
+
+Abstract:
+
+    Z3 Managed API: Relation Sorts
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2012-11-23
+
+Notes:
+    
+--*/
+
+using System;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Z3
+{
+    /// <summary>
+    /// Relation sorts.
+    /// </summary>
+    [ContractVerification(true)]
+    public class RelationSort : Sort
+    {
+        /// <summary>
+        /// The arity of the relation sort.
+        /// </summary>
+        public uint Arity
+        {
+            get { return Native.Z3_get_relation_arity(Context.nCtx, NativeObject); }
+        }
+
+        /// <summary>
+        /// The sorts of the columns of the relation sort.
+        /// </summary>
+        public Sort[] ColumnSorts
+        {
+            get
+            {
+                Contract.Ensures(Contract.Result<Sort[]>() != null);
+
+                if (m_columnSorts != null)
+                    return m_columnSorts;
+
+                uint n = Arity;
+                Sort[] res = new Sort[n];
+                for (uint i = 0; i < n; i++)
+                    res[i] = Sort.Create(Context, Native.Z3_get_relation_column(Context.nCtx, NativeObject, i));
+                return res;
+            }
+        }
+
+        #region Internal
+        private Sort[] m_columnSorts = null;
+
+        internal RelationSort(Context ctx, IntPtr obj)
+            : base(ctx, obj)
+        {
+            Contract.Requires(ctx != null);
+        }
+        #endregion
+    }
+}

src/api/dotnet/SetSort.cs

@@ -0,0 +1,45 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    SetSort.cs
+
+Abstract:
+
+    Z3 Managed API: Set Sorts
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2012-11-23
+
+Notes:
+    
+--*/
+
+using System;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Z3
+{
+    /// <summary>
+    /// Set sorts.
+    /// </summary>
+    [ContractVerification(true)]
+    public class SetSort : Sort
+    {
+        #region Internal
+        internal SetSort(Context ctx, IntPtr obj)
+            : base(ctx, obj)
+        {
+            Contract.Requires(ctx != null);
+        }
+        internal SetSort(Context ctx, Sort ty)
+            : base(ctx, Native.Z3_mk_set_sort(ctx.nCtx, ty.NativeObject))
+        {
+            Contract.Requires(ctx != null);
+            Contract.Requires(ty != null);
+        }
+        #endregion
+    }
+}

src/api/dotnet/Solver.cs

@@ -272,7 +272,7 @@ namespace Microsoft.Z3
             Contract.Requires(ctx != null);
         }
 
-        internal class DecRefQueue : Z3.DecRefQueue
+        internal class DecRefQueue : IDecRefQueue
         {
             public override void IncRef(Context ctx, IntPtr obj)
             {

src/api/dotnet/Sort.cs

@@ -98,9 +98,11 @@ namespace Microsoft.Z3
         /// </summary>
         public Symbol Name
         {
-            get {
+            get
+            {
                 Contract.Ensures(Contract.Result<Symbol>() != null);
-                return Symbol.Create(Context, Native.Z3_get_sort_name(Context.nCtx, NativeObject)); }
+                return Symbol.Create(Context, Native.Z3_get_sort_name(Context.nCtx, NativeObject));
+            }
         }
 
         /// <summary>
@@ -118,14 +120,14 @@ namespace Microsoft.Z3
         internal protected Sort(Context ctx) : base(ctx) { Contract.Requires(ctx != null); }
         internal Sort(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
 
-        #if DEBUG
+#if DEBUG
         internal override void CheckNativeObject(IntPtr obj)
         {
             if (Native.Z3_get_ast_kind(Context.nCtx, obj) != (uint)Z3_ast_kind.Z3_SORT_AST)
                 throw new Z3Exception("Underlying object is not a sort");
             base.CheckNativeObject(obj);
         }
-        #endif
+#endif
 
         [ContractVerification(true)]
         new internal static Sort Create(Context ctx, IntPtr obj)
@@ -150,596 +152,4 @@ namespace Microsoft.Z3
         }
         #endregion
     }    
-
-    /// <summary>
-    /// A Boolean sort.
-    /// </summary>
-    public class BoolSort : Sort
-    {
-        #region Internal
-        internal BoolSort(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
-        internal BoolSort(Context ctx) : base(ctx, Native.Z3_mk_bool_sort(ctx.nCtx)) { Contract.Requires(ctx != null); }
-        #endregion
-    };
-
-    /// <summary>
-    /// An arithmetic sort, i.e., Int or Real.
-    /// </summary>
-    public class ArithSort : Sort
-    {
-        #region Internal
-        internal ArithSort(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
-        #endregion
-    };
-
-    /// <summary>
-    ///  An Integer sort
-    /// </summary>
-    public class IntSort : ArithSort
-    {
-        #region Internal
-        internal IntSort(Context ctx, IntPtr obj)
-            : base(ctx, obj)
-        {
-            Contract.Requires(ctx != null);
-        }
-        internal IntSort(Context ctx)
-            : base(ctx, Native.Z3_mk_int_sort(ctx.nCtx))
-        {
-            Contract.Requires(ctx != null);
-        }
-        #endregion
-    }
-
-    /// <summary>
-    /// A real sort
-    /// </summary>
-    public class RealSort : ArithSort
-    {
-        #region Internal
-        internal RealSort(Context ctx, IntPtr obj)
-            : base(ctx, obj)
-        {
-            Contract.Requires(ctx != null);
-        }
-        internal RealSort(Context ctx)
-            : base(ctx, Native.Z3_mk_real_sort(ctx.nCtx))
-        {
-            Contract.Requires(ctx != null);
-        }
-        #endregion
-    }
-
-    /// <summary>
-    /// Bit-vector sorts.
-    /// </summary>
-    public class BitVecSort : Sort
-    {
-        /// <summary>
-        /// The size of the bit-vector sort.
-        /// </summary>
-        public uint Size
-        {
-            get { return Native.Z3_get_bv_sort_size(Context.nCtx, NativeObject); }
-        }
-
-        #region Internal
-        internal BitVecSort(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
-        internal BitVecSort(Context ctx, uint size) : base(ctx, Native.Z3_mk_bv_sort(ctx.nCtx, size)) { Contract.Requires(ctx != null); }
-        #endregion
-    };
-
-    /// <summary>
-    /// Array sorts.
-    /// </summary>
-    [ContractVerification(true)]
-    public class ArraySort : Sort
-    {
-        /// <summary>
-        /// The domain of the array sort.
-        /// </summary>
-        public Sort Domain
-        {
-            get {
-                Contract.Ensures(Contract.Result<Sort>() != null);
-
-                return Sort.Create(Context, Native.Z3_get_array_sort_domain(Context.nCtx, NativeObject)); }
-        }
-
-        /// <summary>
-        /// The range of the array sort.
-        /// </summary>
-        public Sort Range
-        {
-            get {
-                Contract.Ensures(Contract.Result<Sort>() != null);
-
-                return Sort.Create(Context, Native.Z3_get_array_sort_range(Context.nCtx, NativeObject)); }
-        }
-
-        #region Internal
-        internal ArraySort(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
-        internal ArraySort(Context ctx, Sort domain, Sort range)
-            : base(ctx, Native.Z3_mk_array_sort(ctx.nCtx, domain.NativeObject, range.NativeObject))
-        {
-            Contract.Requires(ctx != null);
-            Contract.Requires(domain != null);
-            Contract.Requires(range != null);
-        }
-        #endregion
-    };
-
-    /// <summary>
-    /// Datatype sorts.
-    /// </summary>
-    [ContractVerification(true)]
-    public class DatatypeSort : Sort
-    {
-        /// <summary>
-        /// The number of constructors of the datatype sort.
-        /// </summary>
-        public uint NumConstructors
-        {
-            get { return Native.Z3_get_datatype_sort_num_constructors(Context.nCtx, NativeObject); }
-        }
-
-        /// <summary>
-        /// The constructors.
-        /// </summary>
-        public FuncDecl[] Constructors
-        {
-            get
-            {
-                Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
-
-                uint n = NumConstructors;
-                FuncDecl[] res = new FuncDecl[n];
-                for (uint i = 0; i < n; i++)
-                    res[i] = new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor(Context.nCtx, NativeObject, i));
-                return res;
-            }
-        }
-
-        /// <summary>
-        /// The recognizers.
-        /// </summary>
-        public FuncDecl[] Recognizers
-        {
-            get
-            {
-                Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
-
-                uint n = NumConstructors;
-                FuncDecl[] res = new FuncDecl[n];
-                for (uint i = 0; i < n; i++)
-                    res[i] = new FuncDecl(Context, Native.Z3_get_datatype_sort_recognizer(Context.nCtx, NativeObject, i));
-                return res;
-            }
-        }
-
-        /// <summary>
-        /// The constructor accessors.
-        /// </summary>
-        public FuncDecl[][] Accessors
-        {
-            get
-            {
-                Contract.Ensures(Contract.Result<FuncDecl[][]>() != null);
-
-                uint n = NumConstructors;
-                FuncDecl[][] res = new FuncDecl[n][];
-                for (uint i = 0; i < n; i++)
-                {
-                    FuncDecl fd = new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor(Context.nCtx, NativeObject, i));
-                    uint ds = fd.DomainSize;
-                    FuncDecl[] tmp = new FuncDecl[ds];
-                    for (uint j = 0; j < ds; j++)
-                        tmp[j] = new FuncDecl(Context, Native.Z3_get_datatype_sort_constructor_accessor(Context.nCtx, NativeObject, i, j));
-                    res[i] = tmp;
-                }
-                return res;
-            }
-        }
-
-        #region Internal
-        internal DatatypeSort(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
-
-        internal DatatypeSort(Context ctx, Symbol name, Constructor[] constructors)
-            : base(ctx, Native.Z3_mk_datatype(ctx.nCtx, name.NativeObject, (uint)constructors.Length, ArrayToNative(constructors)))
-        {
-            Contract.Requires(ctx != null);
-            Contract.Requires(name != null);
-            Contract.Requires(constructors != null);
-        }
-        #endregion
-    };
-
-    /// <summary>
-    /// Uninterpreted Sorts
-    /// </summary>
-    public class UninterpretedSort : Sort
-    {
-        #region Internal
-        internal UninterpretedSort(Context ctx, IntPtr obj)
-            : base(ctx, obj)
-        {
-            Contract.Requires(ctx != null);
-        }
-        internal UninterpretedSort(Context ctx, Symbol s)
-            : base(ctx, Native.Z3_mk_uninterpreted_sort(ctx.nCtx, s.NativeObject))
-        {
-            Contract.Requires(ctx != null);
-            Contract.Requires(s != null);
-        }
-        #endregion
-    }
-
-    /// <summary>
-    /// Tuple sorts.
-    /// </summary>
-    [ContractVerification(true)]
-    public class TupleSort : Sort
-    {
-        /// <summary>
-        /// The constructor function of the tuple.
-        /// </summary>
-        public FuncDecl MkDecl
-        {
-            get {
-                Contract.Ensures(Contract.Result<FuncDecl>() != null);
-
-                return new FuncDecl(Context, Native.Z3_get_tuple_sort_mk_decl(Context.nCtx, NativeObject)); }
-        }
-
-        /// <summary>
-        /// The number of fields in the tuple.
-        /// </summary>
-        public uint NumFields
-        {
-            get { return Native.Z3_get_tuple_sort_num_fields(Context.nCtx, NativeObject); }
-        }
-
-        /// <summary>
-        /// The field declarations.
-        /// </summary>
-        public FuncDecl[] FieldDecls
-        {
-            get
-            {
-                Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
-
-                uint n = NumFields;
-                FuncDecl[] res = new FuncDecl[n];
-                for (uint i = 0; i < n; i++)
-                    res[i] = new FuncDecl(Context, Native.Z3_get_tuple_sort_field_decl(Context.nCtx, NativeObject, i));
-                return res;
-            }
-        }
-
-        #region Internal
-        internal TupleSort(Context ctx, Symbol name, uint numFields, Symbol[] fieldNames, Sort[] fieldSorts)
-            : base(ctx)
-        {
-            Contract.Requires(ctx != null);
-            Contract.Requires(name != null);
-
-            IntPtr t = IntPtr.Zero;
-            NativeObject = Native.Z3_mk_tuple_sort(ctx.nCtx, name.NativeObject, numFields,
-                                                   Symbol.ArrayToNative(fieldNames), AST.ArrayToNative(fieldSorts),
-                                                   ref t, new IntPtr[numFields]);
-        }
-        #endregion
-    };
-
-    /// <summary>
-    /// Enumeration sorts.
-    /// </summary>
-    [ContractVerification(true)]
-    public class EnumSort : Sort
-    {
-        /// <summary>
-        /// The function declarations of the constants in the enumeration.
-        /// </summary>
-        public FuncDecl[] ConstDecls
-        {
-            get {
-                Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
-
-                return _constdecls; }
-        }
-
-        /// <summary>
-        /// The constants in the enumeration.
-        /// </summary>
-        public Expr[] Consts
-        {
-            get {
-                Contract.Ensures(Contract.Result<Expr[]>() != null);
-
-                return _consts; }
-        }
-
-        /// <summary>
-        /// The test predicates for the constants in the enumeration.
-        /// </summary>
-        public FuncDecl[] TesterDecls
-        {
-            get {
-                Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
-                
-                return _testerdecls;
-            }
-        }
-
-        #region Object Invariant
-
-        [ContractInvariantMethod]
-        private void ObjectInvariant()
-        {
-            Contract.Invariant(this._constdecls != null);
-            Contract.Invariant(this._testerdecls != null);
-            Contract.Invariant(this._consts != null);
-        }
-
-        
-        #endregion
-
-        #region Internal
-        readonly private FuncDecl[] _constdecls = null, _testerdecls = null;
-        readonly private Expr[] _consts = null;
-
-        internal EnumSort(Context ctx, Symbol name, Symbol[] enumNames)
-            : base(ctx)
-        {
-            Contract.Requires(ctx != null);
-            Contract.Requires(name != null);
-            Contract.Requires(enumNames != null);
-
-            int n = enumNames.Length;
-            IntPtr[] n_constdecls = new IntPtr[n];
-            IntPtr[] n_testers = new IntPtr[n];
-            NativeObject = Native.Z3_mk_enumeration_sort(ctx.nCtx, name.NativeObject, (uint)n,
-                                                         Symbol.ArrayToNative(enumNames), n_constdecls, n_testers);
-            _constdecls = new FuncDecl[n];            
-            for (uint i = 0; i < n; i++)            
-                _constdecls[i] = new FuncDecl(ctx, n_constdecls[i]);
-            _testerdecls = new FuncDecl[n];
-            for (uint i = 0; i < n; i++)
-                _testerdecls[i] = new FuncDecl(ctx, n_testers[i]);
-            _consts = new Expr[n];
-            for (uint i = 0; i < n; i++)
-                _consts[i] = ctx.MkApp(_constdecls[i]);
-        }
-        #endregion
-    };
-
-    /// <summary>
-    /// List sorts.
-    /// </summary>
-    [ContractVerification(true)]
-    public class ListSort : Sort
-    {
-        /// <summary>
-        /// The declaration of the nil function of this list sort.
-        /// </summary>
-        public FuncDecl NilDecl { get {
-            Contract.Ensures(Contract.Result<FuncDecl>() != null);
-            return nilDecl; } }
-
-        /// <summary>
-        /// The empty list.
-        /// </summary>
-        public Expr Nil
-        {
-            get
-            {
-                Contract.Ensures(Contract.Result<Expr>() != null);
-                return nilConst;
-            }
-        }
-
-        /// <summary>
-        /// The declaration of the isNil function of this list sort.
-        /// </summary>
-        public FuncDecl IsNilDecl
-        {
-            get
-            {
-                Contract.Ensures(Contract.Result<FuncDecl>() != null);
-                return isNilDecl;
-            }
-        }
-
-        /// <summary>
-        /// The declaration of the cons function of this list sort.
-        /// </summary>
-        public FuncDecl ConsDecl
-        {
-            get
-            {
-                Contract.Ensures(Contract.Result<FuncDecl>() != null);
-                return consDecl;
-            }
-        }
-
-        /// <summary>
-        /// The declaration of the isCons function of this list sort.
-        /// </summary>
-        /// 
-        public FuncDecl IsConsDecl
-        {
-            get
-            {
-                Contract.Ensures(Contract.Result<FuncDecl>() != null);
-                return isConsDecl;
-            }
-        }
-
-        /// <summary>
-        /// The declaration of the head function of this list sort.
-        /// </summary>
-        public FuncDecl HeadDecl
-        {
-            get
-            {
-                Contract.Ensures(Contract.Result<FuncDecl>() != null);
-                return headDecl;
-            }
-        }
-
-        /// <summary>
-        /// The declaration of the tail function of this list sort.
-        /// </summary>
-        public FuncDecl TailDecl
-        {
-            get
-            {
-                Contract.Ensures(Contract.Result<FuncDecl>() != null);
-                return tailDecl;
-            }
-        }
-
-        #region Object Invariant
-
-        [ContractInvariantMethod]
-        private void ObjectInvariant()
-        {
-            Contract.Invariant(nilConst != null);
-            Contract.Invariant(nilDecl != null);
-            Contract.Invariant(isNilDecl != null);
-            Contract.Invariant(consDecl != null);
-            Contract.Invariant(isConsDecl != null);
-            Contract.Invariant(headDecl != null);
-            Contract.Invariant(tailDecl != null);
-        }
-
-        
-        #endregion
-
-        #region Internal
-        readonly private FuncDecl nilDecl, isNilDecl, consDecl, isConsDecl, headDecl, tailDecl;
-        readonly private Expr nilConst;
-
-        internal ListSort(Context ctx, Symbol name, Sort elemSort)
-            : base(ctx)
-        {
-            Contract.Requires(ctx != null);
-            Contract.Requires(name != null);
-            Contract.Requires(elemSort != null);
-
-            IntPtr inil = IntPtr.Zero,
-                   iisnil = IntPtr.Zero,
-                   icons = IntPtr.Zero,
-                   iiscons = IntPtr.Zero,
-                   ihead = IntPtr.Zero,
-                   itail = IntPtr.Zero;
-
-            NativeObject = Native.Z3_mk_list_sort(ctx.nCtx, name.NativeObject, elemSort.NativeObject,
-                                                  ref inil, ref iisnil, ref icons, ref iiscons, ref ihead, ref itail);
-            nilDecl = new FuncDecl(ctx, inil);
-            isNilDecl = new FuncDecl(ctx, iisnil);
-            consDecl = new FuncDecl(ctx, icons);
-            isConsDecl = new FuncDecl(ctx, iiscons);
-            headDecl = new FuncDecl(ctx, ihead);
-            tailDecl = new FuncDecl(ctx, itail);
-            nilConst = ctx.MkConst(nilDecl);
-        }
-        #endregion
-    };
-
-    /// <summary>
-    /// Relation sorts.
-    /// </summary>
-    [ContractVerification(true)]
-    public class RelationSort : Sort
-    {
-        /// <summary>
-        /// The arity of the relation sort.
-        /// </summary>
-        public uint Arity
-        {
-            get { return Native.Z3_get_relation_arity(Context.nCtx, NativeObject); }
-        }
-
-        /// <summary>
-        /// The sorts of the columns of the relation sort.
-        /// </summary>
-        public Sort[] ColumnSorts
-        {
-            get
-            {
-                Contract.Ensures(Contract.Result<Sort[]>() != null);
-
-                if (m_columnSorts != null)
-                    return m_columnSorts;
-
-                uint n = Arity;
-                Sort[] res = new Sort[n];
-                for (uint i = 0; i < n; i++)
-                    res[i] = Sort.Create(Context, Native.Z3_get_relation_column(Context.nCtx, NativeObject, i));
-                return res;
-            }
-        }
-
-        #region Internal
-        private Sort[] m_columnSorts = null;
-
-        internal RelationSort(Context ctx, IntPtr obj)
-            : base(ctx, obj)
-        {
-            Contract.Requires(ctx != null);
-        }        
-        #endregion
-    }
-
-    /// <summary>
-    /// Finite domain sorts.
-    /// </summary>
-    [ContractVerification(true)]
-    public class FiniteDomainSort : Sort
-    {
-        /// <summary>
-        /// The size of the finite domain sort.
-        /// </summary>
-        public ulong Size
-        {
-            get { ulong res = 0; Native.Z3_get_finite_domain_sort_size(Context.nCtx, NativeObject, ref res); return res; }
-        }
-
-        #region Internal
-        internal FiniteDomainSort(Context ctx, IntPtr obj)
-            : base(ctx, obj)
-        {
-            Contract.Requires(ctx != null);
-        }
-        internal FiniteDomainSort(Context ctx, Symbol name, ulong size)
-            : base(ctx, Native.Z3_mk_finite_domain_sort(ctx.nCtx, name.NativeObject, size))
-        {
-            Contract.Requires(ctx != null);
-            Contract.Requires(name != null);
-
-        }
-        #endregion
-    }
-
-    /// <summary>
-    /// Set sorts.
-    /// </summary>
-    [ContractVerification(true)]
-    public class SetSort : Sort
-    {
-        #region Internal
-        internal SetSort(Context ctx, IntPtr obj)
-            : base(ctx, obj)
-        {
-            Contract.Requires(ctx != null);
-        }
-        internal SetSort(Context ctx, Sort ty)
-            : base(ctx, Native.Z3_mk_set_sort(ctx.nCtx, ty.NativeObject))
-        {
-            Contract.Requires(ctx != null);
-            Contract.Requires(ty != null);
-        }
-        #endregion
-    }
 }

src/api/dotnet/Statistics.cs

@@ -86,8 +86,18 @@ namespace Microsoft.Z3
             readonly private bool m_is_double = false;
             readonly private uint m_uint = 0;
             readonly private double m_double = 0.0;
-            internal Entry(string k, uint v) { Key = k; m_is_uint = true; m_uint = v; }
+            internal Entry(string k, uint v)
-            internal Entry(string k, double v) { Key = k; m_is_double = true; m_double = v; }
+            {
+                Key = k;
+                m_is_uint = true;
+                m_uint = v;
+            }
+            internal Entry(string k, double v)
+            {
+                Key = k;
+                m_is_double = true;
+                m_double = v;
+            }
             #endregion
         }
 
@@ -177,7 +187,7 @@ namespace Microsoft.Z3
             Contract.Requires(ctx != null);
         }
 
-        internal class DecRefQueue : Z3.DecRefQueue
+        internal class DecRefQueue : IDecRefQueue
         {
             public override void IncRef(Context ctx, IntPtr obj)
             {

src/api/dotnet/StringSymbol.cs

@@ -0,0 +1,73 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    StringSymbol.cs
+
+Abstract:
+
+    Z3 Managed API: String Symbols
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2012-11-23
+
+Notes:
+    
+--*/
+
+using System;
+using System.Runtime.InteropServices;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Z3
+{
+
+    /// <summary>
+    /// Named symbols
+    /// </summary>
+    [ContractVerification(true)]
+    public class StringSymbol : Symbol
+    {
+        /// <summary>
+        /// The string value of the symbol.
+        /// </summary>
+        /// <remarks>Throws an exception if the symbol is not of string kind.</remarks>
+        public string String
+        {
+            get
+            {
+                Contract.Ensures(Contract.Result<string>() != null);
+
+                if (!IsStringSymbol())
+                    throw new Z3Exception("String requested from non-String symbol");
+                return Native.Z3_get_symbol_string(Context.nCtx, NativeObject);
+            }
+        }
+
+        #region Internal
+        internal StringSymbol(Context ctx, IntPtr obj)
+            : base(ctx, obj)
+        {
+            Contract.Requires(ctx != null);
+        }
+
+        internal StringSymbol(Context ctx, string s)
+            : base(ctx, Native.Z3_mk_string_symbol(ctx.nCtx, s))
+        {
+            Contract.Requires(ctx != null);
+        }
+
+#if DEBUG
+        internal override void CheckNativeObject(IntPtr obj)
+        {
+            if ((Z3_symbol_kind)Native.Z3_get_symbol_kind(Context.nCtx, obj) != Z3_symbol_kind.Z3_STRING_SYMBOL)
+                throw new Z3Exception("Symbol is not of string kind");
+
+            base.CheckNativeObject(obj);
+        }
+#endif
+        #endregion
+    }
+}

src/api/dotnet/Symbol.cs

@@ -90,92 +90,4 @@ namespace Microsoft.Z3
         }
         #endregion
     }
-
-    /// <summary>
-    /// Numbered symbols
-    /// </summary>
-    [ContractVerification(true)]
-    public class IntSymbol : Symbol
-    {
-        /// <summary>
-        /// The int value of the symbol.
-        /// </summary>
-        /// <remarks>Throws an exception if the symbol is not of int kind. </remarks>
-        public int Int
-        {
-            get
-            {
-                if (!IsIntSymbol())
-                    throw new Z3Exception("Int requested from non-Int symbol");
-                return Native.Z3_get_symbol_int(Context.nCtx, NativeObject);
-            }
-        }
-
-        #region Internal
-        internal IntSymbol(Context ctx, IntPtr obj)
-            : base(ctx, obj)
-        {
-            Contract.Requires(ctx != null);
-        }
-        internal IntSymbol(Context ctx, int i)
-            : base(ctx, Native.Z3_mk_int_symbol(ctx.nCtx, i))
-        {
-            Contract.Requires(ctx != null);
-        }
-
-        #if DEBUG
-        internal override void CheckNativeObject(IntPtr obj)
-        {
-            if ((Z3_symbol_kind)Native.Z3_get_symbol_kind(Context.nCtx, obj) != Z3_symbol_kind.Z3_INT_SYMBOL)
-                throw new Z3Exception("Symbol is not of integer kind");
-            base.CheckNativeObject(obj);
-        }
-        #endif
-        #endregion
-    }
-
-    /// <summary>
-    /// Named symbols
-    /// </summary>
-    [ContractVerification(true)]
-    public class StringSymbol : Symbol
-    {
-        /// <summary>
-        /// The string value of the symbol.
-        /// </summary>
-        /// <remarks>Throws an exception if the symbol is not of string kind.</remarks>
-        public string String
-        {
-            get
-            {
-                Contract.Ensures(Contract.Result<string>() != null);
-
-                if (!IsStringSymbol())
-                    throw new Z3Exception("String requested from non-String symbol");
-                return Native.Z3_get_symbol_string(Context.nCtx, NativeObject);                
-            }
-        }
-
-        #region Internal
-        internal StringSymbol(Context ctx, IntPtr obj) : base(ctx, obj) 
-        {            
-            Contract.Requires(ctx != null);
-        }
-
-        internal StringSymbol(Context ctx, string s) : base(ctx, Native.Z3_mk_string_symbol(ctx.nCtx, s)) 
-        {
-            Contract.Requires(ctx != null);
-        }
-
-        #if DEBUG
-        internal override void CheckNativeObject(IntPtr obj)
-        {
-            if ((Z3_symbol_kind)Native.Z3_get_symbol_kind(Context.nCtx, obj) != Z3_symbol_kind.Z3_STRING_SYMBOL)
-                throw new Z3Exception("Symbol is not of string kind");
-
-            base.CheckNativeObject(obj);
-        }
-        #endif
-        #endregion
-    }
 }

src/api/dotnet/Tactic.cs

@@ -112,7 +112,7 @@ namespace Microsoft.Z3
             Contract.Requires(ctx != null);
         }
 
-        internal class DecRefQueue : Z3.DecRefQueue
+        internal class DecRefQueue : IDecRefQueue
         {
             public override void IncRef(Context ctx, IntPtr obj)
             {

src/api/dotnet/TupleSort.cs

@@ -0,0 +1,83 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    TupleSort.cs
+
+Abstract:
+
+    Z3 Managed API: Tuple Sorts
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2012-11-23
+
+Notes:
+    
+--*/
+
+using System;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Z3
+{
+    /// <summary>
+    /// Tuple sorts.
+    /// </summary>
+    [ContractVerification(true)]
+    public class TupleSort : Sort
+    {
+        /// <summary>
+        /// The constructor function of the tuple.
+        /// </summary>
+        public FuncDecl MkDecl
+        {
+            get
+            {
+                Contract.Ensures(Contract.Result<FuncDecl>() != null);
+
+                return new FuncDecl(Context, Native.Z3_get_tuple_sort_mk_decl(Context.nCtx, NativeObject));
+            }
+        }
+
+        /// <summary>
+        /// The number of fields in the tuple.
+        /// </summary>
+        public uint NumFields
+        {
+            get { return Native.Z3_get_tuple_sort_num_fields(Context.nCtx, NativeObject); }
+        }
+
+        /// <summary>
+        /// The field declarations.
+        /// </summary>
+        public FuncDecl[] FieldDecls
+        {
+            get
+            {
+                Contract.Ensures(Contract.Result<FuncDecl[]>() != null);
+
+                uint n = NumFields;
+                FuncDecl[] res = new FuncDecl[n];
+                for (uint i = 0; i < n; i++)
+                    res[i] = new FuncDecl(Context, Native.Z3_get_tuple_sort_field_decl(Context.nCtx, NativeObject, i));
+                return res;
+            }
+        }
+
+        #region Internal
+        internal TupleSort(Context ctx, Symbol name, uint numFields, Symbol[] fieldNames, Sort[] fieldSorts)
+            : base(ctx)
+        {
+            Contract.Requires(ctx != null);
+            Contract.Requires(name != null);
+
+            IntPtr t = IntPtr.Zero;
+            NativeObject = Native.Z3_mk_tuple_sort(ctx.nCtx, name.NativeObject, numFields,
+                                                   Symbol.ArrayToNative(fieldNames), AST.ArrayToNative(fieldSorts),
+                                                   ref t, new IntPtr[numFields]);
+        }
+        #endregion
+    };
+}

src/api/dotnet/UninterpretedSort.cs

@@ -0,0 +1,44 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    UninterpretedSort.cs
+
+Abstract:
+
+    Z3 Managed API: Uninterpreted Sorts
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2012-11-23
+
+Notes:
+    
+--*/
+
+using System;
+using System.Diagnostics.Contracts;
+
+namespace Microsoft.Z3
+{
+    /// <summary>
+    /// Uninterpreted Sorts
+    /// </summary>
+    public class UninterpretedSort : Sort
+    {
+        #region Internal
+        internal UninterpretedSort(Context ctx, IntPtr obj)
+            : base(ctx, obj)
+        {
+            Contract.Requires(ctx != null);
+        }
+        internal UninterpretedSort(Context ctx, Symbol s)
+            : base(ctx, Native.Z3_mk_uninterpreted_sort(ctx.nCtx, s.NativeObject))
+        {
+            Contract.Requires(ctx != null);
+            Contract.Requires(s != null);
+        }
+        #endregion
+    }
+}

src/ast/ast.cpp

@@ -1814,6 +1814,11 @@ bool ast_manager::coercion_needed(func_decl * decl, unsigned num_args, expr * co
         }
     }
     else {
+        if (decl->get_arity() != num_args) {
+            // Invalid input: unexpected number of arguments for non-associative operator.
+            // So, there is no point in coercing the input arguments.
+            return false; 
+        }
         for (unsigned i = 0; i < num_args; i++) {
             sort * d = decl->get_domain(i);
             if (d->get_family_id() == m_arith_family_id && d != get_sort(args[i]))