diff --git a/src/muz/rel/dl_sparse_table.cpp b/src/muz/rel/dl_sparse_table.cpp
index 52d9618b8..c9bdec0b6 100644
--- a/src/muz/rel/dl_sparse_table.cpp
+++ b/src/muz/rel/dl_sparse_table.cpp
@@ -1066,11 +1066,14 @@ namespace datalog {
 
             unsigned res_fact_size = res->m_fact_size;
             unsigned res_data_size = res_fact_size*t.row_count();
+            if (res_fact_size != 0 && (res_data_size / res_fact_size) != t.row_count()) {
+                throw default_exception("multiplication overflow");
+            }
 
             res->m_data.resize_data(res_data_size);
 
-            //here we can separate data creatin and insertion into hashmap, since we know
-            //that no row will become duplicit
+            //here we can separate data creating and insertion into hashmap, since we know
+            //that no row will become duplicate
 
             //create the data
             const char* t_ptr = t.m_data.begin();
diff --git a/src/muz/rel/dl_sparse_table.h b/src/muz/rel/dl_sparse_table.h
index 010277b6b..5c5f95a75 100644
--- a/src/muz/rel/dl_sparse_table.h
+++ b/src/muz/rel/dl_sparse_table.h
@@ -275,6 +275,9 @@ namespace datalog {
         //the following two operations allow breaking of the object invariant!
         void resize_data(unsigned sz) {
             m_data_size = sz;
+            if (sz + sizeof(uint64) < sz) {
+                throw default_exception("overflow resizing data section for sparse table");
+            }
             m_data.resize(sz + sizeof(uint64));
         }
 
diff --git a/src/test/vector.cpp b/src/test/vector.cpp
index 0a3904954..86ae997ca 100644
--- a/src/test/vector.cpp
+++ b/src/test/vector.cpp
@@ -19,7 +19,7 @@ Revision History:
 #include"vector.h"
 
 static void tst1() {
-    vector<int> v1;
+    svector<int> v1;
     SASSERT(v1.empty());
     for (unsigned i = 0; i < 1000; i++) {
         v1.push_back(i + 3);
@@ -30,8 +30,8 @@ static void tst1() {
     for (unsigned i = 0; i < 1000; i++) {
         SASSERT(static_cast<unsigned>(v1[i]) == i + 3);
     }
-    vector<int>::iterator it = v1.begin();
-    vector<int>::iterator end = v1.end();
+    svector<int>::iterator it = v1.begin();
+    svector<int>::iterator end = v1.end();
     for (int i = 0; it != end; ++it, ++i) {
         SASSERT(*it == i + 3);
     }
@@ -42,6 +42,18 @@ static void tst1() {
     }
     SASSERT(v1.empty());
     SASSERT(v1.size() == 0);
+    unsigned i = 1000000000;
+    while (true) {
+        std::cout << "resize " << i << "\n";
+        try {            
+            v1.resize(i);
+        }
+        catch (z3_exception& e) {
+            std::cout << e.msg() << "\n";
+            break;
+        }
+        i *= 2;
+    }
 }
 
 void tst_vector() {
diff --git a/src/util/vector.h b/src/util/vector.h
index c9ed900a9..8bfe7c703 100644
--- a/src/util/vector.h
+++ b/src/util/vector.h
@@ -29,6 +29,7 @@ Revision History:
 #include<memory.h>
 #include"memory_manager.h"
 #include"hash.h"
+#include"z3_exception.h"
 
 // disable warning for constant 'if' expressions.
 // these are used heavily in templates.
@@ -67,9 +68,14 @@ class vector {
         else {
             SASSERT(capacity() > 0);
             unsigned old_capacity = reinterpret_cast<unsigned *>(m_data)[CAPACITY_IDX];
+            unsigned old_capacity_T = sizeof(T) * old_capacity + sizeof(unsigned) * 2;
             unsigned new_capacity = (3 * old_capacity + 1) >> 1;
+            unsigned new_capacity_T  = sizeof(T) * new_capacity + sizeof(unsigned) * 2;
             unsigned size         = reinterpret_cast<unsigned *>(m_data)[SIZE_IDX];
-            unsigned * mem        = reinterpret_cast<unsigned*>(memory::allocate(sizeof(T) * new_capacity + sizeof(unsigned) * 2));
+            if (new_capacity <= old_capacity || new_capacity_T <= old_capacity_T) {
+                throw default_exception("Overflow encountered when expanding vector");
+            }
+            unsigned * mem        = reinterpret_cast<unsigned*>(memory::allocate(new_capacity_T));
             *mem                  = new_capacity; 
             mem ++;
             *mem                  = size;