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

contrib/cmake/src/tactic/core/CMakeLists.txt

@@ -3,6 +3,7 @@ z3_add_component(core_tactics
     blast_term_ite_tactic.cpp
     cofactor_elim_term_ite.cpp
     cofactor_term_ite_tactic.cpp
+    collect_statistics_tactic.cpp  
     ctx_simplify_tactic.cpp
     der_tactic.cpp
     distribute_forall_tactic.cpp

src/api/api_config_params.cpp

@@ -37,7 +37,7 @@ extern "C" {
         catch (z3_exception & ex) {
             // The error handler is only available for contexts
             // Just throw a warning.
-            warning_msg(ex.msg());
+            warning_msg("%s", ex.msg());
         }
     }
 
@@ -62,7 +62,7 @@ extern "C" {
         catch (z3_exception & ex) {
             // The error handler is only available for contexts
             // Just throw a warning.
-            warning_msg(ex.msg());
+            warning_msg("%s", ex.msg());
             return Z3_FALSE;
         }
     }
@@ -88,7 +88,7 @@ extern "C" {
         catch (z3_exception & ex) {
             // The error handler is only available for contexts
             // Just throw a warning.
-            warning_msg(ex.msg());
+            warning_msg("%s", ex.msg());
         }
     }
 

src/ast/ast.cpp

@@ -1965,7 +1965,7 @@ bool ast_manager::check_sorts(ast const * n) const {
         return true;
     }
     catch (ast_exception & ex) {
-        warning_msg(ex.msg());
+        warning_msg("%s", ex.msg());
         return false;
     }
 }

src/ast/rewriter/bv_trailing.cpp

@@ -67,10 +67,8 @@ struct bv_trailing::imp {
         }
         expr_ref out1(m);
         expr_ref out2(m);
-        DEBUG_CODE(
+        VERIFY(min == remove_trailing(e1, min, out1, TRAILING_DEPTH));
-            const unsigned rm1 = remove_trailing(e1, min, out1, TRAILING_DEPTH);
+        VERIFY(min == remove_trailing(e2, min, out2, TRAILING_DEPTH));
-            const unsigned rm2 = remove_trailing(e2, min, out2, TRAILING_DEPTH);
-            SASSERT(rm1 == min && rm2 == min););
         const bool are_eq = m.are_equal(out1, out2);
         result = are_eq ? m.mk_true() : m.mk_eq(out1, out2);
         return are_eq ? BR_DONE : BR_REWRITE2;

src/ast/well_sorted.cpp

@@ -66,7 +66,7 @@ struct well_sorted_proc {
                 strm << "Expected sort: " << mk_pp(expected_sort, m_manager) << "\n";
                 strm << "Actual sort:   " << mk_pp(actual_sort, m_manager) << "\n";
                 strm << "Function sort: " << mk_pp(decl, m_manager) << ".";
-                warning_msg(strm.str().c_str());
+                warning_msg("%s", strm.str().c_str());
                 m_error = true;
                 return;
             }

src/muz/pdr/pdr_reachable_cache.cpp

@@ -109,7 +109,12 @@ namespace pdr {
             UNREACHABLE();
             break;
         }
-        if (found) m_stats.m_hits++; m_stats.m_miss++;
+        if (found) {
+            m_stats.m_hits++; 
+        }
+        else {
+            m_stats.m_miss++;
+        }
         return found;
     }
 

src/muz/rel/dl_base.cpp

@@ -391,7 +391,7 @@ namespace datalog {
             std::ostringstream buffer;
             buffer << "creating large table of size " << upper_bound;
             if (p) buffer << " for relation " << p->get_name();
-            warning_msg(buffer.str().c_str());
+            warning_msg("%s", buffer.str().c_str());
         }
 
         for(table_element i = 0; i < upper_bound; i++) {

src/parsers/smt2/smt2parser.cpp

@@ -1034,7 +1034,7 @@ namespace smt2 {
                 else {
                     std::ostringstream str;
                     str << "unknown attribute " << id;
-                    warning_msg(str.str().c_str());
+                    warning_msg("%s", str.str().c_str());
                     next();
                     // just consume the 
                     consume_sexpr();

src/parsers/smt2/smt2scanner.cpp

@@ -23,10 +23,12 @@ namespace smt2 {
 
     void scanner::next() {
         if (m_cache_input)
-            m_cache.push_back(m_curr);
+            m_cache.push_back(m_curr);                
-        SASSERT(m_curr != EOF);
+        SASSERT(!m_at_eof);
         if (m_interactive) {
             m_curr = m_stream.get();
+            if (m_stream.eof())
+                m_at_eof = true;
         }
         else if (m_bpos < m_bend) {
             m_curr = m_buffer[m_bpos];
@@ -37,7 +39,7 @@ namespace smt2 {
             m_bend = static_cast<unsigned>(m_stream.gcount());
             m_bpos = 0;
             if (m_bpos == m_bend) {
-                m_curr = EOF;
+                m_at_eof = true;
             }
             else {
                 m_curr = m_buffer[m_bpos];
@@ -52,7 +54,7 @@ namespace smt2 {
         next();
         while (true) {
             char c = curr();
-            if (c == EOF)
+            if (m_at_eof)
                 return;
             if (c == '\n') {
                 new_line();
@@ -70,7 +72,7 @@ namespace smt2 {
         next();
         while (true) {
             char c = curr();
-            if (c == EOF) {
+            if (m_at_eof) {
                 throw scanner_exception("unexpected end of quoted symbol", m_line, m_spos);
             }
             else if (c == '\n') {
@@ -167,7 +169,7 @@ namespace smt2 {
         m_string.reset();
         while (true) {
             char c = curr();
-            if (c == EOF)
+            if (m_at_eof)
                 throw scanner_exception("unexpected end of string", m_line, m_spos);
             if (c == '\n') {
                 new_line();
@@ -237,10 +239,11 @@ namespace smt2 {
         }
     }
 
-    scanner::scanner(cmd_context & ctx, std::istream& stream, bool interactive):
+    scanner::scanner(cmd_context & ctx, std::istream& stream, bool interactive) :
         m_interactive(interactive),
         m_spos(0),
         m_curr(0), // avoid Valgrind warning
+        m_at_eof(false),
         m_line(1),
         m_pos(0),
         m_bv_size(UINT_MAX),
@@ -289,9 +292,13 @@ namespace smt2 {
     }
 
     scanner::token scanner::scan() {
-        while (true) {
+        while (true) {            
             signed char c = curr();
             m_pos = m_spos;
+
+            if (m_at_eof)                
+                return EOF_TOKEN;
+
             switch (m_normalized[(unsigned char) c]) {
             case ' ':
                 next();
@@ -327,8 +334,6 @@ namespace smt2 {
                     return read_symbol();
                 else
                     return read_signed_number();
-            case -1:
-                return EOF_TOKEN;
             default: {
                 scanner_exception ex("unexpected character", m_line, m_spos);
                 next();

src/parsers/smt2/smt2scanner.h

@@ -34,6 +34,7 @@ namespace smt2 {
         bool               m_interactive;
         int                m_spos; // position in the current line of the stream
         char               m_curr;  // current char;
+        bool               m_at_eof;
         
         int                m_line;  // line
         int                m_pos;   // start position of the token

src/smt/theory_fpa.cpp

@@ -691,7 +691,10 @@ namespace smt {
         m_rw.reset();
         m_th_rw.reset();        
         m_trail_stack.pop_scope(m_trail_stack.get_num_scopes());        
-        if (m_factory) dealloc(m_factory); m_factory = 0;
+        if (m_factory) {
+            dealloc(m_factory); 
+            m_factory = 0;
+        }
         ast_manager & m = get_manager();
         dec_ref_map_key_values(m, m_conversions);
         dec_ref_collection_values(m, m_is_added_to_model);

src/smt/theory_utvpi_def.h

@@ -250,7 +250,7 @@ namespace smt {
             std::stringstream msg;
             msg << "found non utvpi logic expression:\n" << mk_pp(n, get_manager()) << "\n";
             TRACE("utvpi", tout << msg.str(););
-            warning_msg(msg.str().c_str());
+            warning_msg("%s", msg.str().c_str());
             get_context().push_trail(value_trail<context, bool>(m_non_utvpi_exprs));
             m_non_utvpi_exprs = true;
         }

src/tactic/probe.cpp

@@ -287,14 +287,14 @@ struct is_non_qfbv_predicate {
         if (fid == m.get_basic_family_id())
             return;
         if (fid == u.get_family_id()) {
-			if (n->get_decl_kind() == OP_BSDIV0 ||
+            if (n->get_decl_kind() == OP_BSDIV0 ||
-				n->get_decl_kind() == OP_BUDIV0 ||
+                n->get_decl_kind() == OP_BUDIV0 ||
-				n->get_decl_kind() == OP_BSREM0 ||
+                n->get_decl_kind() == OP_BSREM0 ||
-				n->get_decl_kind() == OP_BUREM0 ||
+                n->get_decl_kind() == OP_BUREM0 ||
-				n->get_decl_kind() == OP_BSMOD0)
+                n->get_decl_kind() == OP_BSMOD0)
-				throw found();
+                throw found();
-			return;
+            return;
-		}
+        }
         if (is_uninterp_const(n))
             return;
         throw found();

src/util/warning.cpp

@@ -167,4 +167,3 @@ void warning_msg(const char * msg, ...) {
         va_end(args);
     }
 }
-