Merge branch 'pure' of https://github.com/Z3Prover/z3

src/api/api_opt.cpp

@@ -126,9 +126,11 @@ extern "C" {
         lbool r = l_undef;
         cancel_eh<opt::context> eh(*to_optimize_ptr(o));
         unsigned timeout = to_optimize_ptr(o)->get_params().get_uint("timeout", mk_c(c)->get_timeout());
+        unsigned rlimit = mk_c(c)->get_rlimit();
         api::context::set_interruptable si(*(mk_c(c)), eh);        
         {
             scoped_timer timer(timeout, &eh);
+            scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit);
             try {
                 r = to_optimize_ptr(o)->optimize();
             }

src/tactic/fpa/fpa2bv_model_converter.cpp

@@ -179,8 +179,6 @@ expr_ref fpa2bv_model_converter::convert_bv2rm(model * bv_mdl, func_decl * var,
 void fpa2bv_model_converter::convert(model * bv_mdl, model * float_mdl) {
     fpa_util fu(m);
     bv_util bu(m);
-    unsynch_mpz_manager & mpzm = fu.fm().mpz_manager();
-    unsynch_mpq_manager & mpqm = fu.fm().mpq_manager();
 
     TRACE("fpa2bv_mc", tout << "BV Model: " << std::endl;
     for (unsigned i = 0; i < bv_mdl->get_num_constants(); i++)

src/test/ddnf.cpp

@@ -123,7 +123,7 @@ datalog::ddnf_core* populate_ddnf(char const* file, ptr_vector<tbv>& tbvs) {
 
 
 static void read_args(char ** argv, int argc, int& i) {
-    if (argc = i + 2) {
+    if (argc == i + 2) {
         g_file = argv[i + 1];
         ++i;
         return;

src/test/dl_query.cpp

@@ -212,6 +212,7 @@ void tst_dl_query() {
     //params.m_dl_default_relation = symbol("tr_hashtable");
 
     //dl_query_test_wpa(params);
+    return;
 
 
     ast_manager m;

src/test/doc.cpp

@@ -181,7 +181,6 @@ class test_doc_cls {
         expr_ref result(m);
         expr_ref_vector conjs(m);
         unsigned n = m2.num_tbits();
-        tbv_manager& tm = m2.tbvm();
         SASSERT(n <= m_vars.size());
         for (unsigned i = 0; i < n; ++i) {
             switch (t[i]) {

src/test/old_interval.cpp

@@ -172,7 +172,6 @@ public:
 
 static void tst2() {
     typedef basic_interval_manager<unsynch_mpz_manager, false> mpzi_manager;
-    typedef mpzi_manager::interval mpzi;
     typedef mpzi_manager::scoped_interval scoped_mpzi;
 
     unsynch_mpz_manager nm;

src/test/quant_solve.cpp

@@ -238,6 +238,7 @@ static void test_quant_solve1() {
     test_quant_solver(m, "(exists ((c Cell)) (= (cell c c) c1))", false);
     test_quant_solver(m, "(exists ((c Cell)) (= (cell c (cdr c1)) c1))", false);
 
+
     test_quant_solver(m, "(exists ((t Tuple)) (= (tuple a P r1) t))");
     test_quant_solver(m, "(exists ((t Tuple)) (= a (first t)))");
     test_quant_solver(m, "(exists ((t Tuple)) (= P (second t)))");
@@ -253,11 +254,13 @@ void tst_quant_solve() {
 
     test_quant_solve1();   
 
+#if 0
     memory::finalize();
 #ifdef _WINDOWS
     _CrtDumpMemoryLeaks();
 #endif
     exit(0);
+#endif
 }
 
 

src/test/simplex.cpp

@@ -24,35 +24,35 @@ static vector<R> vec(int i, int j) {
     return nv;
 }
 
-static vector<R> vec(int i, int j, int k) {
-    vector<R> nv = vec(i, j);
-    nv.push_back(R(k));
-    return nv;
-}
+// static vector<R> vec(int i, int j, int k) {
+//     vector<R> nv = vec(i, j);
+//     nv.push_back(R(k));
+//     return nv;
+// }
 
-static vector<R> vec(int i, int j, int k, int l) {
-    vector<R> nv = vec(i, j, k);
-    nv.push_back(R(l));
-    return nv;
-}
+// static vector<R> vec(int i, int j, int k, int l) {
+//     vector<R> nv = vec(i, j, k);
+//     nv.push_back(R(l));
+//     return nv;
+// }
 
-static vector<R> vec(int i, int j, int k, int l, int x) {
-    vector<R> nv = vec(i, j, k, l);
-    nv.push_back(R(x));
-    return nv;
-}
+/// static vector<R> vec(int i, int j, int k, int l, int x) {
+///     vector<R> nv = vec(i, j, k, l);
+///     nv.push_back(R(x));
+///     return nv;
+/// }
 
-static vector<R> vec(int i, int j, int k, int l, int x, int y) {
-    vector<R> nv = vec(i, j, k, l, x);
-    nv.push_back(R(y));
-    return nv;
-}
+// static vector<R> vec(int i, int j, int k, int l, int x, int y) {
+//     vector<R> nv = vec(i, j, k, l, x);
+//     nv.push_back(R(y));
+//     return nv;
+// }
 
-static vector<R> vec(int i, int j, int k, int l, int x, int y, int z) {
-    vector<R> nv = vec(i, j, k, l, x, y);
-    nv.push_back(R(z));
-    return nv;
-}
+// static vector<R> vec(int i, int j, int k, int l, int x, int y, int z) {
+//     vector<R> nv = vec(i, j, k, l, x, y);
+//     nv.push_back(R(z));
+//     return nv;
+// }
 
 
 
@@ -148,7 +148,7 @@ void tst_simplex() {
         coeffs.push_back(mpz(i+1));
     }
 
-    Simplex::row r = S.add_row(1, coeffs.size(), vars.c_ptr(), coeffs.c_ptr());
+    // Simplex::row r = S.add_row(1, coeffs.size(), vars.c_ptr(), coeffs.c_ptr());
     is_sat = S.make_feasible();
     std::cout << "feasible: " << is_sat << "\n";
     S.display(std::cout);

src/util/hwf.cpp

@@ -85,8 +85,9 @@ hwf_manager::~hwf_manager()
 {
 }
 
-#define RAW(X) (*reinterpret_cast<const uint64*>(&(X)))
-#define DBL(X) (*reinterpret_cast<const double*>(&(X)))
+// #define RAW(X) (*reinterpret_cast<const uint64*>(&(X)))
+#define RAW(X) ({ uint64 tmp; memcpy(&tmp, &(X), sizeof(uint64)); tmp; })
+#define DBL(X) ({ double tmp; memcpy(&tmp, &(X), sizeof(double)); tmp; })
 
 void hwf_manager::set(hwf & o, int value) {
     o.value = (double) value;
@@ -166,7 +167,7 @@ void hwf_manager::set(hwf & o, bool sign, uint64 significand, int exponent) {
     uint64 raw = (sign?0x8000000000000000ull:0);
     raw |= (((uint64)exponent) + 1023) << 52;
     raw |= significand;
-    o.value = *reinterpret_cast<double*>(&raw);
+    memcpy(&o.value, &raw, sizeof(double));
 }
 
 void hwf_manager::set(hwf & o, hwf const & x) {

src/util/mpfx.cpp

@@ -199,8 +199,9 @@ void mpfx_manager::set(mpfx & n, uint64 v) {
     else {
         allocate_if_needed(n);
         n.m_sign              = 0;
-        unsigned * _v         = reinterpret_cast<unsigned*>(&v);
         unsigned * w          = words(n);
+        unsigned * _v         = 0;
+        memcpy(_v, &v, sizeof(unsigned*));
         for (unsigned i = 0; i < m_total_sz; i++) 
             w[i] = 0;
         w[m_frac_part_sz]     = _v[0];
@@ -679,7 +680,8 @@ int64 mpfx_manager::get_int64(mpfx const & n) const {
     SASSERT(is_int64(n));
     unsigned * w = words(n);
     w += m_frac_part_sz;
-    uint64 r = *reinterpret_cast<uint64*>(w);
+    uint64 r = 0;
+    memcpy(&r, w, sizeof(uint64));
     if (r == 0x8000000000000000ull) {
         SASSERT(is_neg(n));
         return INT64_MIN;
@@ -693,7 +695,9 @@ uint64 mpfx_manager::get_uint64(mpfx const & n) const {
     SASSERT(is_uint64(n));
     unsigned * w = words(n);
     w += m_frac_part_sz;
-    return *reinterpret_cast<uint64*>(w);
+    uint64 r = 0;
+    memcpy(&r, w, sizeof(uint64));
+    return r;
 }
 
 template<bool SYNCH>

src/util/prime_generator.cpp

@@ -67,7 +67,9 @@ void prime_generator::process_next_k_numbers(uint64 k) {
             if (todo[k1] < p) {
                 m_primes.push_back(todo[k1]);
             }
-            break;
+            else {
+                break;
+            }
         }
         unsigned k2 = 0;
         for (; k1 < todo_sz; k1++, k2++) {