diff options
| author | Tim King <taking@google.com> | 2015-11-28 00:28:43 -0500 |
|---|---|---|
| committer | Tim King <taking@google.com> | 2015-12-02 00:00:02 -0500 |
| commit | 269dacb4b06f6dae5c220dc70a1f1e67728d1f62 (patch) | |
| tree | 6d1f155510e886ced67c1de1fba5676be377a023 /src | |
| parent | a39d025ce314d7f191f72258fad00ca19e134b5b (diff) | |
Guarding the destruction of the a linux specific variable on WIN32.
Diffstat (limited to 'src')
| -rw-r--r-- | src/main/util.cpp | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/main/util.cpp b/src/main/util.cpp index 927802496..f0cab25fa 100644 --- a/src/main/util.cpp +++ b/src/main/util.cpp @@ -290,9 +290,11 @@ void cvc4_init() throw(Exception) { } void cvc4_shutdown() throw () { +#ifndef __WIN32__ free(cvc4StackBase); cvc4StackBase = NULL; cvc4StackSize = 0; +#endif /* __WIN32__ */ } }/* CVC4::main namespace */ |