Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

src/ast/ast.cpp

@@ -1850,6 +1850,7 @@ func_decl * ast_manager::mk_func_decl(symbol const & name, unsigned arity, sort
 
 void ast_manager::check_sort(func_decl const * decl, unsigned num_args, expr * const * args) const {
     ast_manager& m = const_cast<ast_manager&>(*this);
+
     if (decl->is_associative()) {
         sort * expected = decl->get_domain(0);
         for (unsigned i = 0; i < num_args; i++) {
@@ -1894,7 +1895,18 @@ void ast_manager::check_sorts_core(ast const * n) const {
     if  (n->get_kind() != AST_APP) 
         return; // nothing else to check...
     app const * a = to_app(n);
-    check_sort(a->get_decl(), a->get_num_args(), a->get_args());
+    func_decl* d = a->get_decl();
+    check_sort(d, a->get_num_args(), a->get_args());
+    if (a->get_num_args() == 2 &&
+        !d->is_flat_associative() && 
+        d->is_right_associative()) {
+        check_sorts_core(a->get_arg(1));
+    }
+    if (a->get_num_args() == 2 &&
+        !d->is_flat_associative() && 
+        d->is_left_associative()) {
+        check_sorts_core(a->get_arg(0));
+    }
 }
 
 bool ast_manager::check_sorts(ast const * n) const {

src/muz/transforms/dl_mk_rule_inliner.cpp

@@ -527,6 +527,9 @@ namespace datalog {
 
 
     bool mk_rule_inliner::do_eager_inlining(rule * r, rule_set const& rules, rule_ref& res) {
+        if (r->has_negation()) {
+            return false;
+        }
 
         SASSERT(rules.is_closed());
         const rule_stratifier& strat = rules.get_stratifier();

src/tactic/arith/lia2pb_tactic.cpp

@@ -71,6 +71,7 @@ class lia2pb_tactic : public tactic {
             if (m_bm.has_lower(n, l, s) &&
                 m_bm.has_upper(n, u, s) &&  
                 l.is_zero() &&
+                !u.is_neg() && 
                 u.get_num_bits() <= m_max_bits) {
                 
                 return true;

src/util/rational.h

@@ -104,7 +104,7 @@ public:
     }
 
     bool is_int32() const {
-        if (is_small()) return true; 
+        if (is_small() && is_int()) return true; 
         // we don't assume that if it is small, then it is int32.
         if (!is_int64()) return false;
         int64 v = get_int64();