From ff052d41eeb6f0f1c2d9e16bd7bf0df4dd59d1fe Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 28 Nov 2013 13:49:18 -0800
Subject: [PATCH] chore(*): fix cygwin compilation errors

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/library/tactic/cex_builder.cpp   |  4 ++--
 src/library/tactic/proof_builder.cpp |  4 ++--
 src/library/tactic/tactic.cpp        | 10 +++++-----
 src/util/script_exception.cpp        |  1 +
 4 files changed, 10 insertions(+), 9 deletions(-)

diff --git a/src/library/tactic/cex_builder.cpp b/src/library/tactic/cex_builder.cpp
index a3f1d8fa9a..c64a9b657d 100644
--- a/src/library/tactic/cex_builder.cpp
+++ b/src/library/tactic/cex_builder.cpp
@@ -22,9 +22,9 @@ static int mk_cex_builder(lua_State * L) {
     luaref ref(L, 1);
     return push_cex_builder(L,
                             mk_cex_builder([=](name const & n, optional<counterexample> const & cex, assignment const & a) -> counterexample {
-                                    script_state _S(S);
+                                    script_state S_copy(S);
                                     optional<environment> r;
-                                    _S.exec_protected([&]() {
+                                    S_copy.exec_protected([&]() {
                                             ref.push(); // push user-fun on the stack
                                             push_name(L, n);
                                             if (cex)
diff --git a/src/library/tactic/proof_builder.cpp b/src/library/tactic/proof_builder.cpp
index b920a0f45a..1e63e238e0 100644
--- a/src/library/tactic/proof_builder.cpp
+++ b/src/library/tactic/proof_builder.cpp
@@ -83,8 +83,8 @@ static int mk_proof_builder(lua_State * L) {
     return push_proof_builder(L,
                               mk_proof_builder([=](proof_map const & m, assignment const & a) -> expr {
                                       expr r;
-                                      script_state _S(S);
-                                      _S.exec_protected([&]() {
+                                      script_state S_copy(S);
+                                      S_copy.exec_protected([&]() {
                                               ref.push(); // push user-fun on the stack
                                               push_proof_map(L, m);
                                               push_assignment(L, a);
diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp
index d97834399e..e8ed4c42b6 100644
--- a/src/library/tactic/tactic.cpp
+++ b/src/library/tactic/tactic.cpp
@@ -386,13 +386,13 @@ static int mk_lua_tactic01(lua_State * L) {
     luaref ref(L, 1);
     return push_tactic(L,
                        mk_tactic01([=](environment const & env, io_state const & ios, proof_state const & s) -> optional<proof_state> {
-                               script_state _S(S);
+                               script_state S_copy(S);
                                optional<proof_state> r;
                                luaref coref; // Remark: we have to release the reference in a protected block.
                                try {
                                    bool done    = false;
                                    lua_State * co;
-                                   _S.exec_protected([&]() {
+                                   S_copy.exec_protected([&]() {
                                            co = lua_newthread(L); // create a coroutine for executing user-fun
                                            coref = luaref(L, -1);    // make sure co-routine in not deleted
                                            lua_pop(L, 1);
@@ -406,11 +406,11 @@ static int mk_lua_tactic01(lua_State * L) {
                                    while (!done) {
                                        check_interrupted();
                                        std::this_thread::yield(); // give another thread a chance to execute
-                                       _S.exec_protected([&]() {
+                                       S_copy.exec_protected([&]() {
                                                done = resume(co, 0);
                                            });
                                    }
-                                   _S.exec_protected([&]() {
+                                   S_copy.exec_protected([&]() {
                                            if (is_proof_state(co, -1)) {
                                                r = to_proof_state(co, -1);
                                            }
@@ -418,7 +418,7 @@ static int mk_lua_tactic01(lua_State * L) {
                                        });
                                    return r;
                                } catch (...) {
-                                   _S.exec_protected([&]() { coref.release(); });
+                                   S_copy.exec_protected([&]() { coref.release(); });
                                    throw;
                                }
                            }));
diff --git a/src/util/script_exception.cpp b/src/util/script_exception.cpp
index 66f7a348fa..c9491d8e92 100644
--- a/src/util/script_exception.cpp
+++ b/src/util/script_exception.cpp
@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include <sstream>
 #include <string>
+#include <cstdlib>
 #include "util/debug.h"
 #include "util/script_exception.h"