Added some thread safety wisdom to the README.md, but it needs a rewr…

…ite by BD.

README.md

@@ -194,6 +194,22 @@ make
 sudo make install
 ```
 
+#### Support for Thread Safety
+
+The Yices library is not thread safe by default, but can be made thread safe by
+configuring and following some simple programming priciples.
+
+If configured with the switch `--enable-thread-safety` the Yices library will be thread
+safe in the following restricted sense: as long as the creation and manipulation of
+each contexts, and model is restricted to a single thread, there should be no races.
+In particular separate threads that each create their own contexts can manipulate and check
+them without impeding other thread's progress.
+It is also recommended that the user themselves should syncronize any access to any global
+ctx_config_t or param_t objects.
+
+Currently  `--enable-mcsat` and `--enable-thread-safety` are incompatible. We hope to
+fix this shortly.
+
 3. You may need to provide `LDFLAGS/CPPFLAGS` if `./configure` fails to
   find the libpoly library. Other options may be useful too.  Try
   `./configure --help` to see what's there.

src/terms/mpq_stores.c

@@ -55,7 +55,6 @@ void init_mpqstore(mpq_store_t *s, uint32_t n) {
  * Allocate an mpq in s
  */
 static mpq_t *_o_mpqstore_alloc(mpq_store_t *s) {
-  void *tmp;
   uint32_t i;
   mpq_bank_t *new_bank;
   mpq_link_t *obj;
@@ -70,18 +69,17 @@ static mpq_t *_o_mpqstore_alloc(mpq_store_t *s) {
 
   i = s->free_index;
   if (i == 0) {
-    new_bank = (mpq_bank_t *) safe_malloc(sizeof(mpq_bank_t) + s->blocklen * sizeof(mpq_link_t));
+    new_bank = (mpq_bank_t *)safe_malloc(sizeof(mpq_bank_t) + s->blocklen * sizeof(mpq_link_t));
     new_bank->h.next = s->bnk;
     s->bnk = new_bank;
     i = s->blocklen;
   }
 
   i --;
   s->free_index = i;
-  tmp = s->bnk->block + i;
+  obj = s->bnk->block + i;
 
-  // only initialize when we give  it out
-  obj = (mpq_link_t *)tmp;
+  // only initialize when we give it out
   mpq_init2(obj->mpq, 64);
   obj->h.next = NULL; //sanity check: when returned it should still be NULL
 
@@ -106,7 +104,7 @@ static void _o_delete_mpqstore(mpq_store_t *s) {
   while (b != NULL) {
     next = b->h.next;
     for (i=k; i<s->blocklen; i++) {
-      obj = (mpq_link_t *) (b->block + i);
+      obj = b->block + i;
       mpq_clear(obj->mpq);
     }
     safe_free(b);