From 1239c8f8e885f82a89e965f229c65c67f731e631 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 27 Jul 2016 11:20:31 -0700
Subject: [PATCH] update MSF example

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 .../Properties/AssemblyInfo.cs                | 36 +++++++++++++++++++
 .../Z3BaseSolver.cs                           |  8 ++---
 2 files changed, 40 insertions(+), 4 deletions(-)
 create mode 100644 examples/msf/SolverFoundation.Plugin.Z3/Properties/AssemblyInfo.cs

diff --git a/examples/msf/SolverFoundation.Plugin.Z3/Properties/AssemblyInfo.cs b/examples/msf/SolverFoundation.Plugin.Z3/Properties/AssemblyInfo.cs
new file mode 100644
index 000000000..6d495a895
--- /dev/null
+++ b/examples/msf/SolverFoundation.Plugin.Z3/Properties/AssemblyInfo.cs
@@ -0,0 +1,36 @@
+using System.Reflection;
+using System.Runtime.CompilerServices;
+using System.Runtime.InteropServices;
+
+// General Information about an assembly is controlled through the following 
+// set of attributes. Change these attribute values to modify the information
+// associated with an assembly.
+[assembly: AssemblyTitle("SolverFoundation.Plugin.Z3")]
+[assembly: AssemblyDescription("")]
+[assembly: AssemblyConfiguration("")]
+[assembly: AssemblyCompany("Microsoft")]
+[assembly: AssemblyProduct("SolverFoundation.Plugin.Z3")]
+[assembly: AssemblyCopyright("Copyright © Microsoft 2010")]
+[assembly: AssemblyTrademark("")]
+[assembly: AssemblyCulture("")]
+
+// Setting ComVisible to false makes the types in this assembly not visible 
+// to COM components.  If you need to access a type in this assembly from 
+// COM, set the ComVisible attribute to true on that type.
+[assembly: ComVisible(false)]
+
+// The following GUID is for the ID of the typelib if this project is exposed to COM
+[assembly: Guid("ed1476c0-96de-4d2c-983d-3888b140c3ad")]
+
+// Version information for an assembly consists of the following four values:
+//
+//      Major Version
+//      Minor Version 
+//      Build Number
+//      Revision
+//
+// You can specify all the values or you can default the Build and Revision Numbers 
+// by using the '*' as shown below:
+// [assembly: AssemblyVersion("1.0.*")]
+[assembly: AssemblyVersion("1.0.0.0")]
+[assembly: AssemblyFileVersion("1.0.0.0")]
diff --git a/examples/msf/SolverFoundation.Plugin.Z3/Z3BaseSolver.cs b/examples/msf/SolverFoundation.Plugin.Z3/Z3BaseSolver.cs
index af8bc92a2..1c82406be 100644
--- a/examples/msf/SolverFoundation.Plugin.Z3/Z3BaseSolver.cs
+++ b/examples/msf/SolverFoundation.Plugin.Z3/Z3BaseSolver.cs
@@ -47,7 +47,7 @@ namespace Microsoft.SolverFoundation.Plugin.Z3
         private Dictionary<int, Expr> _variables = new Dictionary<int, Expr>();
 
         /// <summary>A map from MSF variable ids to Z3 goal ids</summary>
-        private Dictionary<IGoal, uint> _goals = new Dictionary<IGoal, uint>();
+        private Dictionary<IGoal, Optimize.Handle> _goals = new Dictionary<IGoal, Optimize.Handle>();
 
         internal Z3BaseSolver(IRowVariableModel model)
         {
@@ -64,7 +64,7 @@ namespace Microsoft.SolverFoundation.Plugin.Z3
             get { return _variables; }
         }
 
-        internal Dictionary<IGoal, uint> Goals
+        internal Dictionary<IGoal, Optimize.Handle> Goals
         {
             get { return _goals; }
         }
@@ -332,7 +332,7 @@ namespace Microsoft.SolverFoundation.Plugin.Z3
                             // Remember all objective values
                             foreach (var pair in _goals)
                             {
-                                var optimalValue = Utils.ToRational(_optSolver.GetUpper(pair.Value));
+                                var optimalValue = Utils.ToRational(pair.Value.Upper);
                                 _model.SetValue(pair.Key.Index, optimalValue);
                             }
                             model.Dispose();
@@ -356,7 +356,7 @@ namespace Microsoft.SolverFoundation.Plugin.Z3
                                     // Remember all objective values
                                     foreach (var pair in _goals)
                                     {
-                                        var optimalValue = Utils.ToRational(_optSolver.GetUpper(pair.Value));
+                                        var optimalValue = Utils.ToRational(pair.Value.Upper);
                                         _model.SetValue(pair.Key.Index, optimalValue);
                                     }
                                     subOptimalModel.Dispose();