diff --git a/src/cmd_context/interpolant_cmds.cpp b/src/cmd_context/interpolant_cmds.cpp
index 318569cd5..7fd44c088 100644
--- a/src/cmd_context/interpolant_cmds.cpp
+++ b/src/cmd_context/interpolant_cmds.cpp
@@ -114,7 +114,7 @@ static void get_interpolant_and_maybe_check(cmd_context & ctx, expr * t, params_
 
   ptr_vector<expr>::const_iterator it  = ctx.begin_assertions();
   ptr_vector<expr>::const_iterator end = ctx.end_assertions();
-  ptr_vector<ast> cnsts(end - it);
+  ptr_vector<ast> cnsts((unsigned)(end - it));
   for (int i = 0; it != end; ++it, ++i)
   cnsts[i] = *it;
     
diff --git a/src/duality/duality_profiling.cpp b/src/duality/duality_profiling.cpp
index 3b392a91a..a4e9e0240 100755
--- a/src/duality/duality_profiling.cpp
+++ b/src/duality/duality_profiling.cpp
@@ -25,6 +25,12 @@ Revision History:
 #include <string.h>
 #include <stdlib.h>
 
+#ifdef WIN32
+#pragma warning(disable:4996)
+#pragma warning(disable:4800)
+#pragma warning(disable:4267)
+#endif
+
 #include "duality_wrapper.h"
 #include "iz3profiling.h"
 
diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp
index 17b93d35b..2d52ab283 100644
--- a/src/duality/duality_rpfp.cpp
+++ b/src/duality/duality_rpfp.cpp
@@ -21,13 +21,21 @@ Revision History:
 
 
 
-#include "duality.h"
-#include "duality_profiling.h"
+#ifdef WIN32
+#pragma warning(disable:4996)
+#pragma warning(disable:4800)
+#pragma warning(disable:4267)
+#endif
+
 #include <algorithm>
 #include <fstream>
 #include <set>
 #include <iterator>
 
+
+#include "duality.h"
+#include "duality_profiling.h"
+
 #ifndef WIN32
 // #define Z3OPS
 #endif
diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp
index 91532960b..973ad769c 100644
--- a/src/duality/duality_solver.cpp
+++ b/src/duality/duality_solver.cpp
@@ -19,6 +19,12 @@ Revision History:
 
 --*/
 
+#ifdef WIN32
+#pragma warning(disable:4996)
+#pragma warning(disable:4800)
+#pragma warning(disable:4267)
+#endif
+
 #include "duality.h"
 #include "duality_profiling.h"
 
@@ -26,6 +32,7 @@ Revision History:
 #include <set>
 #include <map>
 #include <list>
+#include <iterator>
 
 // TODO: make these official options or get rid of them
 
diff --git a/src/duality/duality_wrapper.cpp b/src/duality/duality_wrapper.cpp
index 24f6a5e20..cf2c803cb 100644
--- a/src/duality/duality_wrapper.cpp
+++ b/src/duality/duality_wrapper.cpp
@@ -18,6 +18,13 @@ Revision History:
 
 --*/
 
+#ifdef WIN32
+#pragma warning(disable:4996)
+#pragma warning(disable:4800)
+#pragma warning(disable:4267)
+#pragma warning(disable:4101)
+#endif
+
 #include "duality_wrapper.h"
 #include <iostream>
 #include "smt_solver.h"
diff --git a/src/duality/duality_wrapper.h b/src/duality/duality_wrapper.h
index 94e8d2642..2b0045023 100755
--- a/src/duality/duality_wrapper.h
+++ b/src/duality/duality_wrapper.h
@@ -1466,6 +1466,5 @@ namespace std {
   };
 }
 
-
 #endif
 
diff --git a/src/interp/iz3base.cpp b/src/interp/iz3base.cpp
index f316c22cf..26146bfa3 100755
--- a/src/interp/iz3base.cpp
+++ b/src/interp/iz3base.cpp
@@ -18,6 +18,12 @@ Revision History:
 
 --*/
 
+#ifdef WIN32
+#pragma warning(disable:4996)
+#pragma warning(disable:4800)
+#pragma warning(disable:4267)
+#pragma warning(disable:4101)
+#endif
 
 #include "iz3base.h"
 #include <stdio.h>
diff --git a/src/interp/iz3checker.cpp b/src/interp/iz3checker.cpp
index b4e55af20..d423ba48f 100755
--- a/src/interp/iz3checker.cpp
+++ b/src/interp/iz3checker.cpp
@@ -17,6 +17,13 @@ Revision History:
 
 --*/
 
+#ifdef WIN32
+#pragma warning(disable:4996)
+#pragma warning(disable:4800)
+#pragma warning(disable:4267)
+#pragma warning(disable:4101)
+#endif
+
 #include "iz3base.h"
 #include "iz3checker.h"
 
diff --git a/src/interp/iz3interp.cpp b/src/interp/iz3interp.cpp
index 56dc1ccec..c204cc35d 100755
--- a/src/interp/iz3interp.cpp
+++ b/src/interp/iz3interp.cpp
@@ -18,6 +18,14 @@ Revision History:
 --*/
 
 /* Copyright 2011 Microsoft Research. */
+
+#ifdef WIN32
+#pragma warning(disable:4996)
+#pragma warning(disable:4800)
+#pragma warning(disable:4267)
+#pragma warning(disable:4101)
+#endif
+
 #include <assert.h>
 #include <algorithm>
 #include <stdio.h>
diff --git a/src/interp/iz3mgr.cpp b/src/interp/iz3mgr.cpp
index aa8e8abe3..6664cd2fe 100644
--- a/src/interp/iz3mgr.cpp
+++ b/src/interp/iz3mgr.cpp
@@ -18,6 +18,15 @@ Revision History:
 --*/
 
 
+#ifdef WIN32
+#pragma warning(disable:4996)
+#pragma warning(disable:4800)
+#pragma warning(disable:4267)
+#pragma warning(disable:4101)
+#pragma warning(disable:4805)
+#pragma warning(disable:4800)
+#endif
+
 #include "iz3mgr.h"
 
 #include <stdio.h>
diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h
index 51a9a8697..e974a199b 100644
--- a/src/interp/iz3mgr.h
+++ b/src/interp/iz3mgr.h
@@ -263,6 +263,7 @@ class iz3mgr  {
     default:;    
     }
     assert(0);
+    return 0;
   }
 
   ast arg(const ast &t, int i){
diff --git a/src/interp/iz3profiling.cpp b/src/interp/iz3profiling.cpp
index 262254271..2c4a31d58 100755
--- a/src/interp/iz3profiling.cpp
+++ b/src/interp/iz3profiling.cpp
@@ -17,6 +17,13 @@ Revision History:
 
 --*/
 
+#ifdef WIN32
+#pragma warning(disable:4996)
+#pragma warning(disable:4800)
+#pragma warning(disable:4267)
+#pragma warning(disable:4101)
+#endif
+
 #include "iz3profiling.h"
 
 #include <map>
diff --git a/src/interp/iz3proof.cpp b/src/interp/iz3proof.cpp
index 968a4b25a..3fefea73f 100755
--- a/src/interp/iz3proof.cpp
+++ b/src/interp/iz3proof.cpp
@@ -18,6 +18,12 @@ Revision History:
 --*/
 
 
+#ifdef WIN32
+#pragma warning(disable:4996)
+#pragma warning(disable:4800)
+#pragma warning(disable:4267)
+#pragma warning(disable:4101)
+#endif
 
 #include "iz3proof.h"
 #include "iz3profiling.h"
diff --git a/src/interp/iz3proof_itp.cpp b/src/interp/iz3proof_itp.cpp
index 8b78a7135..61ed78463 100644
--- a/src/interp/iz3proof_itp.cpp
+++ b/src/interp/iz3proof_itp.cpp
@@ -17,6 +17,13 @@ Revision History:
 
 --*/
 
+#ifdef WIN32
+#pragma warning(disable:4996)
+#pragma warning(disable:4800)
+#pragma warning(disable:4267)
+#pragma warning(disable:4101)
+#endif
+
 #include "iz3proof_itp.h"
 
 #ifndef WIN32
diff --git a/src/interp/iz3translate.cpp b/src/interp/iz3translate.cpp
index abddb4bda..6a1b665cf 100755
--- a/src/interp/iz3translate.cpp
+++ b/src/interp/iz3translate.cpp
@@ -17,6 +17,13 @@ Revision History:
 
 --*/
 
+#ifdef WIN32
+#pragma warning(disable:4996)
+#pragma warning(disable:4800)
+#pragma warning(disable:4267)
+#pragma warning(disable:4101)
+#endif
+
 #include "iz3translate.h"
 #include "iz3proof.h"
 #include "iz3profiling.h"
diff --git a/src/interp/iz3translate_direct.cpp b/src/interp/iz3translate_direct.cpp
index 0ce3297af..a85c9a1c5 100755
--- a/src/interp/iz3translate_direct.cpp
+++ b/src/interp/iz3translate_direct.cpp
@@ -20,6 +20,14 @@ Revision History:
 --*/
 
 
+#ifdef WIN32
+#pragma warning(disable:4996)
+#pragma warning(disable:4800)
+#pragma warning(disable:4267)
+#pragma warning(disable:4101)
+#pragma warning(disable:4390)
+#endif
+
 #include "iz3translate.h"
 #include "iz3proof.h"
 #include "iz3profiling.h"
diff --git a/src/muz/duality/duality_dl_interface.cpp b/src/muz/duality/duality_dl_interface.cpp
index 397d50655..248aca163 100644
--- a/src/muz/duality/duality_dl_interface.cpp
+++ b/src/muz/duality/duality_dl_interface.cpp
@@ -38,6 +38,12 @@ Revision History:
 
 // template class symbol_table<family_id>;
 
+#ifdef WIN32
+#pragma warning(disable:4996)
+#pragma warning(disable:4800)
+#pragma warning(disable:4267)
+#pragma warning(disable:4101)
+#endif
 
 #include "duality.h"
 #include "duality_profiling.h"