add missing locks around mpz operations that access object allocator. Use internal skolem constant for theory assumption to hide it from models

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/smt/theory_str.cpp

@@ -7364,7 +7364,7 @@ namespace smt {
         const char* strOverlap = "!!TheoryStrOverlapAssumption!!";
         seq_util m_sequtil(get_manager());
         sort * s = get_manager().mk_bool_sort();
-        m_theoryStrOverlapAssumption_term = expr_ref(get_manager().mk_fresh_const(strOverlap, s), get_manager());
+        m_theoryStrOverlapAssumption_term = expr_ref(mk_fresh_const(strOverlap, s), get_manager());
         assumptions.push_back(get_manager().mk_not(m_theoryStrOverlapAssumption_term));
     }
 
@@ -9239,7 +9239,7 @@ namespace smt {
               );
 
         // ----------------------------------------------------------------------------------------
-
+        
         ptr_vector<expr> orList;
         ptr_vector<expr> andList;
 

src/util/mpz.h

@@ -497,7 +497,9 @@ public:
         STRACE("mpz", tout << "[mpz] 0 - " << to_string(a) << " == ";); 
         if (is_small(a) && a.m_val == INT_MIN) {
             // neg(INT_MIN) is not a small int
+            MPZ_BEGIN_CRITICAL();
             set_big_i64(a, - static_cast<long long>(INT_MIN)); 
+            MPZ_END_CRITICAL();
             return;
         }
 #ifndef _MP_GMP
@@ -518,7 +520,9 @@ public:
             if (a.m_val < 0) {
                 if (a.m_val == INT_MIN) {
                     // abs(INT_MIN) is not a small int
+                    MPZ_BEGIN_CRITICAL();
                     set_big_i64(a, - static_cast<long long>(INT_MIN)); 
+                    MPZ_END_CRITICAL();
                 }
                 else
                     a.m_val = -a.m_val;

src/util/small_object_allocator.cpp

@@ -68,6 +68,8 @@ void small_object_allocator::reset() {
 
 #define MASK ((1 << PTR_ALIGNMENT) - 1)
 
+#include <windows.h>
+
 void small_object_allocator::deallocate(size_t size, void * p) {
     if (size == 0) return;
 
@@ -92,6 +94,7 @@ void small_object_allocator::deallocate(size_t size, void * p) {
     m_free_list[slot_id] = p;
 }
 
+
 void * small_object_allocator::allocate(size_t size) {
     if (size == 0) return 0;
 
@@ -100,8 +103,9 @@ void * small_object_allocator::allocate(size_t size) {
     return memory::allocate(size);
 #endif
     m_alloc_size += size;
-    if (size >= SMALL_OBJ_SIZE - (1 << PTR_ALIGNMENT))
+    if (size >= SMALL_OBJ_SIZE - (1 << PTR_ALIGNMENT)) {
         return memory::allocate(size);
+    }
 #ifdef Z3DEBUG
     size_t osize = size;
 #endif