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

scripts/mk_util.py

@@ -2685,8 +2685,8 @@ def get_full_version_string(major, minor, build, revision):
     if GIT_HASH:
         res += " " + GIT_HASH
     if GIT_DESCRIBE:
-        branch = check_output(['git', 'rev-parse', '--abbrev-ref', 'HEAD', '--long'])
+        branch = check_output(['git', 'rev-parse', '--abbrev-ref', 'HEAD'])
-        res += " master " + check_output(['git', 'describe'])
+        res += " " + branch + " " + check_output(['git', 'describe'])
     return '"' + res + '"'
 
 # Update files with the version number

src/ast/rewriter/rewriter_def.h

@@ -189,7 +189,6 @@ bool rewriter_tpl<Config>::constant_fold(app * t, frame & fr) {
             result_stack().shrink(fr.m_spos);
             result_stack().push_back(arg);
             fr.m_state = REWRITE_BUILTIN;
-            unsigned max_depth = fr.m_max_depth;
             if (visit<false>(arg, fr.m_max_depth)) {
                 m_r = result_stack().back();
                 result_stack().pop_back();

src/cmd_context/cmd_context.cpp

@@ -739,8 +739,11 @@ void cmd_context::insert_rec_fun(func_decl* f, expr_ref_vector const& binding, s
     lhs = m().mk_app(f, binding.size(), binding.c_ptr());
     eq  = m().mk_eq(lhs, e);
     if (!ids.empty()) {
-        expr* pat = m().mk_pattern(lhs);
+        if (!is_app(e)) {
-        eq  = m().mk_forall(ids.size(), f->get_domain(), ids.c_ptr(), eq, 0, m().rec_fun_qid(), symbol::null, 1, &pat);
+            throw cmd_exception("Z3 only supports recursive definitions that are proper terms (not binders or variables)");
+        }
+        expr* pats[2] = { m().mk_pattern(lhs), m().mk_pattern(to_app(e)) };
+        eq  = m().mk_forall(ids.size(), f->get_domain(), ids.c_ptr(), eq, 0, m().rec_fun_qid(), symbol::null, 2, pats);
     }
 
     //

src/sat/sat_solver.cpp

@@ -816,7 +816,7 @@ namespace sat {
         m_params.set_sym("phase", saved_phase);
         int finished_id = -1;
         std::string        ex_msg;
-        par_exception_kind ex_kind;
+        par_exception_kind ex_kind = DEFAULT_EX;
         unsigned error_code = 0;
         lbool result = l_undef;
         #pragma omp parallel for

src/smt/smt_context.cpp

@@ -4217,39 +4217,17 @@ namespace smt {
                 TRACE("context", tout << mk_pp(e, m) << "\n";);
                 quantifier* q = to_quantifier(e);
                 if (!m.is_rec_fun_def(q)) continue;
-                SASSERT(q->get_num_patterns() == 1);
+                SASSERT(q->get_num_patterns() == 2);
                 expr* fn = to_app(q->get_pattern(0))->get_arg(0);
+                expr* body = to_app(q->get_pattern(1))->get_arg(0);
                 SASSERT(is_app(fn));
                 func_decl* f = to_app(fn)->get_decl();
-                expr* eq = q->get_expr();
-                expr_ref body(m);
-                if (is_fun_def(fn, q->get_expr(), body)) {
                 func_interp* fi = alloc(func_interp, m, f->get_arity());
                 fi->set_else(body);
                 m_model->register_decl(f, fi);            
             }
         }
     }
-    }
-
-    bool context::is_fun_def(expr* f, expr* body, expr_ref& result) {
-        expr* t1, *t2, *t3;
-        if (m_manager.is_eq(body, t1, t2) || m_manager.is_iff(body, t1, t2)) {
-            if (t1 == f) return result = t2, true;
-            if (t2 == f) return result = t1, true;
-            return false;
-        }
-        if (m_manager.is_ite(body, t1, t2, t3)) {
-            expr_ref body1(m_manager), body2(m_manager);
-            if (is_fun_def(f, t2, body1) && is_fun_def(f, t3, body2)) {
-                // f is not free in t1
-                result = m_manager.mk_ite(t1, body1, body2);
-                return true;
-            }
-        }
-        return false;
-    }
-
 
 };
 

src/smt/smt_context.h

@@ -1167,8 +1167,6 @@ namespace smt {
 
         void add_rec_funs_to_model();
 
-        bool is_fun_def(expr* f, expr* q, expr_ref& body);
-
     public:
         bool can_propagate() const;
 

src/smt/smt_context_pp.cpp

@@ -613,7 +613,7 @@ namespace smt {
             out << "justification ";
             literal_vector lits;
             const_cast<conflict_resolution&>(*m_conflict_resolution).justification2literals(j.get_justification(), lits);
-            display_literals_verbose(out, lits.size(), lits.c_ptr());
+            display_literals(out, lits.size(), lits.c_ptr());
             break;
         }
         default:

src/smt/smt_model_checker.cpp

@@ -318,7 +318,7 @@ namespace smt {
 
     bool model_checker::check_rec_fun(quantifier* q) {
         TRACE("model_checker", tout << mk_pp(q, m) << "\n";);
-        SASSERT(q->get_num_patterns() == 1);
+        SASSERT(q->get_num_patterns() == 2); // first pattern is the function, second is the body.
         expr* fn = to_app(q->get_pattern(0))->get_arg(0);
         SASSERT(is_app(fn));
         func_decl* f = to_app(fn)->get_decl();

src/util/hwf.cpp

@@ -52,8 +52,10 @@ Revision History:
 
 #ifdef USE_INTRINSICS
 #include <emmintrin.h>
+#if defined(_MSC_VER) || defined(__SSE4_1__)
 #include <smmintrin.h>
 #endif
+#endif
 
 hwf_manager::hwf_manager() :
     m_mpz_manager(m_mpq_manager)
@@ -304,7 +306,9 @@ void hwf_manager::round_to_integral(mpf_rounding_mode rm, hwf const & x, hwf & o
     // According to the Intel Architecture manual, the x87-instrunction FRNDINT is the
     // same in 32-bit and 64-bit mode. The _mm_round_* intrinsics are SSE4 extensions.
 #ifdef _WINDOWS
-#ifdef USE_INTRINSICS
+#if defined(USE_INTRINSICS) && \
+    (defined(_WINDOWS) && (defined(__AVX__) || defined(_M_X64))) || \
+    (!defined(_WINDOWS) && defined(__SSE4_1__))
     switch (rm) {
     case 0: _mm_store_sd(&o.value, _mm_round_pd(_mm_set_sd(x.value), _MM_FROUND_TO_NEAREST_INT)); break;
     case 2: _mm_store_sd(&o.value, _mm_round_pd(_mm_set_sd(x.value), _MM_FROUND_TO_POS_INF)); break;