diff --git a/src/solvers/prop/prop.h b/src/solvers/prop/prop.h
index a6ee4371f2a..fc43f6683ea 100644
--- a/src/solvers/prop/prop.h
+++ b/src/solvers/prop/prop.h
@@ -12,6 +12,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 // decision procedure wrapper for boolean propositional logics
 
+#include <stdint.h>
+
 #include <util/message.h>
 #include <util/threeval.h>
 
diff --git a/src/solvers/sat/satcheck_minisat2.cpp b/src/solvers/sat/satcheck_minisat2.cpp
index 6c8a6b45f3a..bc298ca53ed 100644
--- a/src/solvers/sat/satcheck_minisat2.cpp
+++ b/src/solvers/sat/satcheck_minisat2.cpp
@@ -115,6 +115,8 @@ void satcheck_minisat2_baset<T>::lcnf(const bvt &bv)
   clause_counter++;
 }
 
+#ifndef _WIN32
+
 static Minisat::Solver *solver_to_interrupt=nullptr;
 
 static void interrupt_solver(int signum)
@@ -122,6 +124,8 @@ static void interrupt_solver(int signum)
   solver_to_interrupt->interrupt();
 }
 
+#endif
+
 template<typename T>
 propt::resultt satcheck_minisat2_baset<T>::prop_solve()
 {
@@ -161,6 +165,10 @@ propt::resultt satcheck_minisat2_baset<T>::prop_solve()
         Minisat::vec<Minisat::Lit> solver_assumptions;
         convert(assumptions, solver_assumptions);
 
+        using Minisat::lbool;
+
+#ifndef _WIN32
+
         void (*old_handler)(int)=SIG_ERR;
 
         if(time_limit_seconds!=0)
@@ -173,7 +181,6 @@ propt::resultt satcheck_minisat2_baset<T>::prop_solve()
             alarm(time_limit_seconds);
         }
 
-        using Minisat::lbool;
         lbool solver_result=solver->solveLimited(solver_assumptions);
 
         if(old_handler!=SIG_ERR)
@@ -183,6 +190,19 @@ propt::resultt satcheck_minisat2_baset<T>::prop_solve()
           solver_to_interrupt=solver;
         }
 
+#else // _WIN32
+
+        if(time_limit_seconds!=0)
+        {
+          messaget::warning() <<
+            "Time limit ignored (not supported on Win32 yet)" << messaget::eom;
+        }
+
+        lbool solver_result=
+          solver->solve(solver_assumptions) ? l_True : l_False;
+
+#endif
+
         if(solver_result==l_True)
         {
           messaget::status() <<