From 7a0d49cb32c91a8fa16717dc20e72ac3bc262a56 Mon Sep 17 00:00:00 2001
From: "U-REDMOND\\kenmcmil" <kenmcmil@A3539013.redmond.corp.microsoft.com>
Date: Thu, 28 Mar 2013 11:18:20 -0700
Subject: [PATCH] porting to windows

---
 src/api/z3_api.h       | 11 ++++-------
 src/interp/iz3base.cpp |  2 +-
 src/interp/iz3base.h   |  2 +-
 src/interp/iz3foci.cpp |  3 ++-
 4 files changed, 8 insertions(+), 10 deletions(-)

diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index a64f1473d..6d8f34c6c 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -7788,7 +7788,7 @@ END_MLAPI_EXCLUDE
     def_API('Z3_interpolation_profile', STRING, (_in(CONTEXT),))
   */
 
-  Z3_string Z3_API Z3_interpolation_profile(Z3_context ctx);
+  Z3_string Z3_API Z3_interpolation_profile(__in Z3_context ctx);
   
   /**
      \brief Read an interpolation problem from file.
@@ -7824,8 +7824,7 @@ END_MLAPI_EXCLUDE
   */
   
 
-  int Z3_API
-  Z3_read_interpolation_problem(__in Z3_context ctx,
+  int Z3_API Z3_read_interpolation_problem(__in Z3_context ctx,
 				__out int *num, 
 				__out_ecount(*num) Z3_ast **cnsts, 
 				__out_ecount(*num) int **parents,
@@ -7853,8 +7852,7 @@ END_MLAPI_EXCLUDE
 
   */
   
-  int Z3_API
-  Z3_check_interpolant(Z3_context ctx, int num, Z3_ast *cnsts, int *parents, Z3_ast *interps, const char **error,
+  int Z3_API Z3_check_interpolant(Z3_context ctx, int num, Z3_ast *cnsts, int *parents, Z3_ast *interps, const char **error,
                                        int num_theory, Z3_ast *theory);
 
   /** Write an interpolation problem to file suitable for reading with
@@ -7870,8 +7868,7 @@ END_MLAPI_EXCLUDE
 
   */
 
-  void Z3_API
-  Z3_write_interpolation_problem(Z3_context ctx,
+  void Z3_API  Z3_write_interpolation_problem(Z3_context ctx,
 				 int num, 
 				 Z3_ast *cnsts, 
 				 int *parents,
diff --git a/src/interp/iz3base.cpp b/src/interp/iz3base.cpp
index 5350a8fb3..0fdce156a 100755
--- a/src/interp/iz3base.cpp
+++ b/src/interp/iz3base.cpp
@@ -247,7 +247,7 @@ bool iz3base::is_sat(ast f){
 }
 
 
-void iz3base::find_children(const hash_set<ast> &cnsts_set,
+void iz3base::find_children(const stl_ext::hash_set<ast> &cnsts_set,
 			    const ast &tree,
 			    std::vector<ast> &cnsts,
 			    std::vector<int> &parents,
diff --git a/src/interp/iz3base.h b/src/interp/iz3base.h
index c8d4b3c9e..da0a3ce4a 100755
--- a/src/interp/iz3base.h
+++ b/src/interp/iz3base.h
@@ -145,7 +145,7 @@ class iz3base : public iz3mgr, public scopes {
   ast simplify_and(std::vector<ast> &conjuncts);
   ast simplify_with_lit_rec(ast n, ast lit, stl_ext::hash_map<ast,ast> &memo, int depth);
   ast simplify_with_lit(ast n, ast lit);  
-  void find_children(const hash_set<ast> &cnsts_set,
+  void find_children(const stl_ext::hash_set<ast> &cnsts_set,
 		     const ast &tree,
 		     std::vector<ast> &cnsts,
 		     std::vector<int> &parents,
diff --git a/src/interp/iz3foci.cpp b/src/interp/iz3foci.cpp
index 38f588ce3..251599041 100755
--- a/src/interp/iz3foci.cpp
+++ b/src/interp/iz3foci.cpp
@@ -307,7 +307,8 @@ public:
 
   int interpolate(const std::vector<ast> &cnsts, std::vector<ast> &itps){
     assert((int)cnsts.size() == frames);
-    foci = foci2::create("lia");
+    std::string lia("lia");
+    foci = foci2::create(lia);
     if(!foci){
       std::cerr << "iZ3: cannot find foci lia solver.\n";
       assert(0);