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

src/ast/ast.h

@@ -523,7 +523,7 @@ public:
 /**
    The ids of expressions and declarations are in different ranges. 
 */
-const unsigned c_first_decl_id = (1 << 31);
+const unsigned c_first_decl_id = (1u << 31u);
 
 /**
    \brief Superclass for function declarations and sorts.

src/interp/iz3foci.cpp

@@ -19,7 +19,6 @@
 
 #include <sstream>
 #include <iostream>
-#include <assert.h>
 
 #include "iz3hash.h"
 #include "foci2.h"
@@ -197,7 +196,7 @@ public:
                 std::cerr << "iZ3: unsupported Z3 operator in expression\n ";
                 print_expr(std::cerr,t);
                 std::cerr << "\n";
-                assert(0 && "iZ3: unsupported Z3 operator");
+                SASSERT(0 && "iZ3: unsupported Z3 operator");
             }
         }
         return res;
@@ -272,7 +271,7 @@ public:
                 }
                 break;
             default:
-                assert("unknown built-in op");
+                SASSERT(false && "unknown built-in op");
             }
         }
         else if(foci->get_int(i,nval)){
@@ -280,15 +279,15 @@ public:
         }
         else if(foci->get_func(i,f)){
             if(f == select_op){
-                assert(n == 2);
+                SASSERT(n == 2);
                 res = make(Select,args[0],args[1]);
             }
             else if(f == store_op){
-                assert(n == 3);
+                SASSERT(n == 3);
                 res = make(Store,args[0],args[1],args[2]);
             }
             else if(f == mod_op){
-                assert(n == 2);
+                SASSERT(n == 2);
                 res = make(Mod,args[0],args[1]);
             }
             else {
@@ -298,20 +297,20 @@ public:
                 if(bar.second){
                     std::cout << "unknown function symbol:\n";
                     foci->show_ast(i);
-                    assert(0);
+                    SASSERT(0);
                 }
                 res = make(func_decl,args);
             }
         }
         else {
             std::cerr << "iZ3: unknown FOCI expression kind\n";
-            assert(0 && "iZ3: unknown FOCI expression kind");
+            SASSERT(0 && "iZ3: unknown FOCI expression kind");
         }
         return res;
     }
 
     int interpolate(const std::vector<ast> &cnsts, std::vector<ast> &itps){
-        assert((int)cnsts.size() == frames);
+        SASSERT((int)cnsts.size() == frames);
         std::string lia("lia");
 #ifdef _FOCI2
         foci = foci2::create(lia);
@@ -320,7 +319,7 @@ public:
 #endif
         if(!foci){
             std::cerr << "iZ3: cannot find foci lia solver.\n";
-            assert(0);
+            SASSERT(0);
         }
         select_op = foci->mk_func("select");
         store_op = foci->mk_func("store");
@@ -335,7 +334,7 @@ public:
         }
         int res = foci->interpolate(foci_cnsts, foci_itps, foci_parents);
         if(res == 0){
-            assert((int)foci_itps.size() == frames-1);
+            SASSERT((int)foci_itps.size() == frames-1);
             itps.resize(frames-1);
             for(int i = 0; i < frames-1; i++){
                 // foci->show_ast(foci_itps[i]);

src/muz/pdr/pdr_util.cpp

@@ -73,7 +73,7 @@ namespace pdr {
     }
 
     std::string pp_cube(unsigned sz, app * const * lits, ast_manager& m) {
-        return pp_cube(sz, reinterpret_cast<expr * const *>(lits), m);
+        return pp_cube(sz, (expr * const *)(lits), m);
     }
 
     std::string pp_cube(unsigned sz, expr * const * lits, ast_manager& m) {

src/muz/rel/dl_sparse_table.cpp

@@ -293,7 +293,7 @@ namespace datalog {
 
         void key_to_reserve(const key_value & key) const {
             m_keys.ensure_reserve();
-            m_keys.write_into_reserve(reinterpret_cast<char *>(key.c_ptr()));
+            m_keys.write_into_reserve((char *)(key.c_ptr()));
         }
 
         offset_vector & get_matching_offset_vector(const key_value & key) {

src/muz/rel/dl_sparse_table.h

@@ -350,7 +350,7 @@ namespace datalog {
                 *ptr&=m_write_mask;
                 *ptr|=val<<m_small_offset;
             }
-            unsigned const next_ofs() const { return m_offset+m_length; }
+            unsigned next_ofs() const { return m_offset+m_length; }
         };
         class column_layout : public svector<column_info> {
 

src/muz/rel/tbv.cpp

@@ -43,7 +43,7 @@ void tbv_manager::reset() {
     m.reset();
 }
 tbv* tbv_manager::allocate() {
-    tbv* r = reinterpret_cast<tbv*>(m.allocate());
+    tbv* r = static_cast<tbv*>(m.allocate());
     DEBUG_CODE(
         if (s_debug_alloc) {
             TRACE("doc", tout << allocated_tbvs.size() << " " << r << "\n";);

src/test/expr_substitution.cpp

@@ -47,16 +47,23 @@ void tst_expr_substitution() {
     expr_substitution subst(m);
     th_rewriter   rw(m);
 
+    std::cout << mk_pp(c, m) << "\n";
+
     // normalizing c does not help.
     rw(c, d, pr);
-    subst.insert(b, d);
 
-    rw.set_substitution(&subst);
+    std::cout << mk_pp(d, m) << "\n";
 
 
-    enable_trace("th_rewriter_step");
+// This portion diverges. It attempts to replace x by (bvadd #xfc x), which contains x.
-    rw(a, new_a, pr);
+//    subst.insert(b, d);
 
-    std::cout << mk_pp(new_a, m) << "\n";
+//    std::cout << mk_pp(a, m) << "\n";
+//    rw.set_substitution(&subst);
+   
+//    enable_trace("th_rewriter_step");
+//    rw(a, new_a, pr);
+
+//    std::cout << mk_pp(new_a, m) << "\n";
     
 }

src/util/hwf.h

@@ -131,11 +131,11 @@ public:
         return (x.get_raw() & 0x8000000000000000ull) != 0; 
     }
 
-    const uint64 sig(hwf const & x) const { 
+    uint64 sig(hwf const & x) const { 
         return x.get_raw() & 0x000FFFFFFFFFFFFFull;
     }
 
-    const int exp(hwf const & x) const {         
+    int exp(hwf const & x) const {         
         return ((x.get_raw() & 0x7FF0000000000000ull) >> 52) - 1023;
     }