diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index eaf4e4777..0aee3f7d8 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -2134,31 +2134,31 @@ namespace Microsoft.Z3
         /// <summary>
         /// Create an empty set.
         /// </summary>
-        public Expr MkEmptySet(Sort domain)
+        public ArrayExpr MkEmptySet(Sort domain)
         {
             Contract.Requires(domain != null);
             Contract.Ensures(Contract.Result<Expr>() != null);
 
             CheckContextMatch(domain);
-            return Expr.Create(this, Native.Z3_mk_empty_set(nCtx, domain.NativeObject));
+            return (ArrayExpr)Expr.Create(this, Native.Z3_mk_empty_set(nCtx, domain.NativeObject));
         }
 
         /// <summary>
         /// Create the full set.
         /// </summary>
-        public Expr MkFullSet(Sort domain)
+        public ArrayExpr MkFullSet(Sort domain)
         {
             Contract.Requires(domain != null);
             Contract.Ensures(Contract.Result<Expr>() != null);
 
             CheckContextMatch(domain);
-            return Expr.Create(this, Native.Z3_mk_full_set(nCtx, domain.NativeObject));
+            return (ArrayExpr)Expr.Create(this, Native.Z3_mk_full_set(nCtx, domain.NativeObject));
         }
 
         /// <summary>
         /// Add an element to the set.
         /// </summary>
-        public Expr MkSetAdd(Expr set, Expr element)
+        public ArrayExpr MkSetAdd(ArrayExpr set, Expr element)
         {
             Contract.Requires(set != null);
             Contract.Requires(element != null);
@@ -2166,14 +2166,14 @@ namespace Microsoft.Z3
 
             CheckContextMatch(set);
             CheckContextMatch(element);
-            return Expr.Create(this, Native.Z3_mk_set_add(nCtx, set.NativeObject, element.NativeObject));
+            return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_add(nCtx, set.NativeObject, element.NativeObject));
         }
 
 
         /// <summary>
         /// Remove an element from a set.
         /// </summary>
-        public Expr MkSetDel(Expr set, Expr element)
+        public ArrayExpr MkSetDel(ArrayExpr set, Expr element)
         {
             Contract.Requires(set != null);
             Contract.Requires(element != null);
@@ -2181,38 +2181,38 @@ namespace Microsoft.Z3
 
             CheckContextMatch(set);
             CheckContextMatch(element);
-            return Expr.Create(this, Native.Z3_mk_set_del(nCtx, set.NativeObject, element.NativeObject));
+            return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_del(nCtx, set.NativeObject, element.NativeObject));
         }
 
         /// <summary>
         /// Take the union of a list of sets.
         /// </summary>
-        public Expr MkSetUnion(params Expr[] args)
+        public ArrayExpr MkSetUnion(params ArrayExpr[] args)
         {
             Contract.Requires(args != null);
             Contract.Requires(Contract.ForAll(args, a => a != null));
 
             CheckContextMatch(args);
-            return Expr.Create(this, Native.Z3_mk_set_union(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
+            return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_union(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
         }
 
         /// <summary>
         /// Take the intersection of a list of sets.
         /// </summary>
-        public Expr MkSetIntersection(params Expr[] args)
+        public ArrayExpr MkSetIntersection(params ArrayExpr[] args)
         {
             Contract.Requires(args != null);
             Contract.Requires(Contract.ForAll(args, a => a != null));
             Contract.Ensures(Contract.Result<Expr>() != null);
 
             CheckContextMatch(args);
-            return Expr.Create(this, Native.Z3_mk_set_intersect(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
+            return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_intersect(nCtx, (uint)args.Length, AST.ArrayToNative(args)));
         }
 
         /// <summary>
         /// Take the difference between two sets.
         /// </summary>
-        public Expr MkSetDifference(Expr arg1, Expr arg2)
+        public ArrayExpr MkSetDifference(ArrayExpr arg1, ArrayExpr arg2)
         {
             Contract.Requires(arg1 != null);
             Contract.Requires(arg2 != null);
@@ -2220,25 +2220,25 @@ namespace Microsoft.Z3
 
             CheckContextMatch(arg1);
             CheckContextMatch(arg2);
-            return Expr.Create(this, Native.Z3_mk_set_difference(nCtx, arg1.NativeObject, arg2.NativeObject));
+            return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_difference(nCtx, arg1.NativeObject, arg2.NativeObject));
         }
 
         /// <summary>
         /// Take the complement of a set.
         /// </summary>
-        public Expr MkSetComplement(Expr arg)
+        public ArrayExpr MkSetComplement(ArrayExpr arg)
         {
             Contract.Requires(arg != null);
             Contract.Ensures(Contract.Result<Expr>() != null);
 
             CheckContextMatch(arg);
-            return Expr.Create(this, Native.Z3_mk_set_complement(nCtx, arg.NativeObject));
+            return (ArrayExpr)Expr.Create(this, Native.Z3_mk_set_complement(nCtx, arg.NativeObject));
         }
 
         /// <summary>
         /// Check for set membership.
         /// </summary>
-        public BoolExpr MkSetMembership(Expr elem, Expr set)
+        public BoolExpr MkSetMembership(Expr elem, ArrayExpr set)
         {
             Contract.Requires(elem != null);
             Contract.Requires(set != null);
@@ -2252,7 +2252,7 @@ namespace Microsoft.Z3
         /// <summary>
         /// Check for subsetness of sets.
         /// </summary>
-        public BoolExpr MkSetSubset(Expr arg1, Expr arg2)
+        public BoolExpr MkSetSubset(ArrayExpr arg1, ArrayExpr arg2)
         {
             Contract.Requires(arg1 != null);
             Contract.Requires(arg2 != null);
diff --git a/src/api/java/AST.java b/src/api/java/AST.java
index 436a9fdcb..6b5493bf9 100644
--- a/src/api/java/AST.java
+++ b/src/api/java/AST.java
@@ -22,10 +22,8 @@ import com.microsoft.z3.enumerations.Z3_ast_kind;
 /**
  * The abstract syntax tree (AST) class.
  **/
-public class AST extends Z3Object
+public class AST extends Z3Object implements Comparable
 {
-    /* Overloaded operators are not translated. */
-
     /**
      * Object comparison.
      * 
@@ -35,7 +33,7 @@ public class AST extends Z3Object
     {
         AST casted = null;
 
-        try
+	try
         {
             casted = AST.class.cast(o);
         } catch (ClassCastException e)
@@ -43,8 +41,13 @@ public class AST extends Z3Object
             return false;
         }
 
-        return this.getNativeObject() == casted.getNativeObject();
-    }
+	return  
+	    (this == casted) || 
+	    (this != null) &&
+	    (casted != null) &&
+	    (getContext().nCtx() == casted.getContext().nCtx()) &&
+	    (Native.isEqAst(getContext().nCtx(), getNativeObject(), casted.getNativeObject()));
+}
 
     /**
      * Object Comparison. 
diff --git a/src/api/java/Context.java b/src/api/java/Context.java
index b2d77e792..bec5da024 100644
--- a/src/api/java/Context.java
+++ b/src/api/java/Context.java
@@ -1725,32 +1725,31 @@ public class Context extends IDisposable
     /**
      * Create an empty set.
      **/
-    public Expr mkEmptySet(Sort domain)
+    public ArrayExpr mkEmptySet(Sort domain)
     {
         checkContextMatch(domain);
-        return Expr.create(this,
+        return (ArrayExpr)Expr.create(this,
                 Native.mkEmptySet(nCtx(), domain.getNativeObject()));
     }
 
     /**
      * Create the full set.
      **/
-    public Expr mkFullSet(Sort domain)
+    public ArrayExpr mkFullSet(Sort domain)
     {
         checkContextMatch(domain);
-        return Expr.create(this,
+        return (ArrayExpr)Expr.create(this,
                 Native.mkFullSet(nCtx(), domain.getNativeObject()));
     }
 
     /**
      * Add an element to the set.
      **/
-    public Expr mkSetAdd(Expr set, Expr element)
+    public ArrayExpr mkSetAdd(ArrayExpr set, Expr element)
     {
         checkContextMatch(set);
         checkContextMatch(element);
-        return Expr.create(
-                this,
+        return (ArrayExpr)Expr.create(this,
                 Native.mkSetAdd(nCtx(), set.getNativeObject(),
                         element.getNativeObject()));
     }
@@ -1758,12 +1757,11 @@ public class Context extends IDisposable
     /**
      * Remove an element from a set.
      **/
-    public Expr mkSetDel(Expr set, Expr element)
+    public ArrayExpr mkSetDel(ArrayExpr set, Expr element)
     {
         checkContextMatch(set);
         checkContextMatch(element);
-        return Expr.create(
-                this,
+        return (ArrayExpr)Expr.create(this,
                 Native.mkSetDel(nCtx(), set.getNativeObject(),
                         element.getNativeObject()));
     }
@@ -1771,11 +1769,10 @@ public class Context extends IDisposable
     /**
      * Take the union of a list of sets.
      **/
-    public Expr mkSetUnion(Expr... args)
+    public ArrayExpr mkSetUnion(ArrayExpr... args)
     {
         checkContextMatch(args);
-        return Expr.create(
-                this,
+        return (ArrayExpr)Expr.create(this,
                 Native.mkSetUnion(nCtx(), (int) args.length,
                         AST.arrayToNative(args)));
     }
@@ -1783,11 +1780,10 @@ public class Context extends IDisposable
     /**
      * Take the intersection of a list of sets.
      **/
-    public Expr mkSetIntersection(Expr... args)
+    public ArrayExpr mkSetIntersection(ArrayExpr... args)
     {
         checkContextMatch(args);
-        return Expr.create(
-                this,
+        return (ArrayExpr)Expr.create(this,
                 Native.mkSetIntersect(nCtx(), (int) args.length,
                         AST.arrayToNative(args)));
     }
@@ -1795,12 +1791,11 @@ public class Context extends IDisposable
     /**
      * Take the difference between two sets.
      **/
-    public Expr mkSetDifference(Expr arg1, Expr arg2)
+    public ArrayExpr mkSetDifference(ArrayExpr arg1, ArrayExpr arg2)
     {
         checkContextMatch(arg1);
         checkContextMatch(arg2);
-        return Expr.create(
-                this,
+        return (ArrayExpr)Expr.create(this,
                 Native.mkSetDifference(nCtx(), arg1.getNativeObject(),
                         arg2.getNativeObject()));
     }
@@ -1808,22 +1803,21 @@ public class Context extends IDisposable
     /**
      * Take the complement of a set.
      **/
-    public Expr mkSetComplement(Expr arg)
+    public ArrayExpr mkSetComplement(ArrayExpr arg)
     {
         checkContextMatch(arg);
-        return Expr.create(this,
+        return (ArrayExpr)Expr.create(this,
                 Native.mkSetComplement(nCtx(), arg.getNativeObject()));
     }
 
     /**
      * Check for set membership.
      **/
-    public BoolExpr mkSetMembership(Expr elem, Expr set)
+    public BoolExpr mkSetMembership(Expr elem, ArrayExpr set)
     {
         checkContextMatch(elem);
         checkContextMatch(set);
-        return (BoolExpr) Expr.create(
-                this,
+        return (BoolExpr) Expr.create(this,
                 Native.mkSetMember(nCtx(), elem.getNativeObject(),
                         set.getNativeObject()));
     }
@@ -1831,12 +1825,11 @@ public class Context extends IDisposable
     /**
      * Check for subsetness of sets.
      **/
-    public BoolExpr mkSetSubset(Expr arg1, Expr arg2)
+    public BoolExpr mkSetSubset(ArrayExpr arg1, ArrayExpr arg2)
     {
         checkContextMatch(arg1);
         checkContextMatch(arg2);
-        return (BoolExpr) Expr.create(
-                this,
+        return (BoolExpr) Expr.create(this,
                 Native.mkSetSubset(nCtx(), arg1.getNativeObject(),
                         arg2.getNativeObject()));
     }
diff --git a/src/api/java/FuncDecl.java b/src/api/java/FuncDecl.java
index 28cdf2a2d..bc2baab91 100644
--- a/src/api/java/FuncDecl.java
+++ b/src/api/java/FuncDecl.java
@@ -26,22 +26,6 @@ import com.microsoft.z3.enumerations.Z3_parameter_kind;
  **/
 public class FuncDecl extends AST
 {
-    /**
-     * Comparison operator.
-     * 
-     * @return True if {@code a"/> and <paramref name="b} share the
-     *         same context and are equal, false otherwise.
-     **/
-    /* Overloaded operators are not translated. */
-
-    /**
-     * Comparison operator.
-     * 
-     * @return True if {@code a"/> and <paramref name="b} do not
-     *         share the same context or are not equal, false otherwise.
-     **/
-    /* Overloaded operators are not translated. */
-
     /**
      * Object comparison.
      **/
@@ -55,7 +39,12 @@ public class FuncDecl extends AST
             return false;
         }
 
-        return this.getNativeObject() == casted.getNativeObject();
+	return  
+	    (this == casted) || 
+	    (this != null) &&
+	    (casted != null) &&
+	    (getContext().nCtx() == casted.getContext().nCtx()) &&
+	    (Native.isEqFuncDecl(getContext().nCtx(), getNativeObject(), casted.getNativeObject()));
     }
 
     /**
diff --git a/src/api/java/Sort.java b/src/api/java/Sort.java
index b118a5dc2..db6bee80e 100644
--- a/src/api/java/Sort.java
+++ b/src/api/java/Sort.java
@@ -25,8 +25,6 @@ import com.microsoft.z3.enumerations.Z3_sort_kind;
  **/
 public class Sort extends AST
 {
-    /* Overloaded operators are not translated. */
-
     /**
      * Equality operator for objects of type Sort. 
      * @param o
@@ -42,7 +40,12 @@ public class Sort extends AST
             return false;
         }
 
-        return this.getNativeObject() == casted.getNativeObject();
+	return  
+	    (this == casted) || 
+	    (this != null) &&
+	    (casted != null) &&
+	    (getContext().nCtx() == casted.getContext().nCtx()) &&
+	    (Native.isEqSort(getContext().nCtx(), getNativeObject(), casted.getNativeObject()));
     }
 
     /**
diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index 59efb2a89..2881f1b62 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -2046,8 +2046,14 @@ inline app * ast_manager::mk_app_core(func_decl * decl, expr * arg1, expr * arg2
 }
 
 app * ast_manager::mk_app(func_decl * decl, unsigned num_args, expr * const * args) {
-    if (decl->get_arity() != num_args && !decl->is_right_associative() && 
-        !decl->is_left_associative() && !decl->is_chainable()) {
+    bool type_error = 
+        decl->get_arity() != num_args && !decl->is_right_associative() && 
+        !decl->is_left_associative() && !decl->is_chainable();
+
+    type_error |= (decl->get_arity() != num_args && num_args < 2 && 
+                   decl->get_family_id() == m_basic_family_id && !decl->is_associative());
+
+    if (type_error) {
         std::ostringstream buffer;
         buffer << "Wrong number of arguments (" << num_args 
                << ") passed to function " << mk_pp(decl, *this);        
diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp
index baba7b701..389f785ab 100644
--- a/src/ast/fpa/fpa2bv_converter.cpp
+++ b/src/ast/fpa/fpa2bv_converter.cpp
@@ -2975,7 +2975,7 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg
     exp_m_lz = m_bv_util.mk_bv_sub(m_bv_util.mk_sign_extend(2, exp),
                                    m_bv_util.mk_zero_extend(2, lz));
     shift = m_bv_util.mk_bv_sub(exp_m_lz,
-                                m_bv_util.mk_numeral(bv_sz - 1, ebits + 2));
+                                m_bv_util.mk_numeral(bv_sz, ebits + 2));
     shift_neg = m_bv_util.mk_bv_neg(shift);
     bv0_e2 = m_bv_util.mk_numeral(0, ebits + 2);
     shift_abs = m.mk_ite(m_bv_util.mk_sle(shift, bv0_e2), shift_neg, shift);
@@ -2987,8 +2987,8 @@ void fpa2bv_converter::mk_to_sbv(func_decl * f, unsigned num, expr * const * arg
     // sig is of the form +- [1].[sig][r][g][s] ... and at least bv_sz + 3 long    
     //           [1][ ... sig ... ][r][g][ ... s ...]
     // [    ... ubv ...    ][r][g][  ... s ...      ]
-    expr_ref max_shift(m);
-    max_shift = m_bv_util.mk_numeral(sig_sz, sig_sz);
+    // expr_ref max_shift(m);
+    // max_shift = m_bv_util.mk_numeral(sig_sz, sig_sz);
     shift_abs = m_bv_util.mk_zero_extend(sig_sz - ebits - 2, shift_abs);
     SASSERT(m_bv_util.get_bv_size(shift_abs) == sig_sz);
     dbg_decouple("fpa2bv_to_sbv_shift_abs", shift_abs);
@@ -3440,7 +3440,7 @@ void fpa2bv_converter::mk_rounding_mode(func_decl * f, expr_ref & result)
 
 void fpa2bv_converter::dbg_decouple(const char * prefix, expr_ref & e) {    
     #ifdef Z3DEBUG
-    return;
+    // return;
     // CMW: This works only for quantifier-free formulas.
     expr_ref new_e(m);
     new_e = m.mk_fresh_const(prefix, m.get_sort(e));
diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp
index 0b28c4277..c59480ee2 100644
--- a/src/ast/fpa_decl_plugin.cpp
+++ b/src/ast/fpa_decl_plugin.cpp
@@ -629,7 +629,6 @@ func_decl * fpa_decl_plugin::mk_to_sbv(decl_kind k, unsigned num_parameters, par
     symbol name("fp.to_sbv");
     sort * bvs = m_bv_plugin->mk_sort(BV_SORT, 1, parameters);
     return m_manager->mk_func_decl(name, arity, domain, bvs, func_decl_info(m_family_id, k, num_parameters, parameters));
-
 }
 
 func_decl * fpa_decl_plugin::mk_to_real(decl_kind k, unsigned num_parameters, parameter const * parameters,
diff --git a/src/smt/tactic/ctx_solver_simplify_tactic.cpp b/src/smt/tactic/ctx_solver_simplify_tactic.cpp
index 98b7592c8..622d67a34 100644
--- a/src/smt/tactic/ctx_solver_simplify_tactic.cpp
+++ b/src/smt/tactic/ctx_solver_simplify_tactic.cpp
@@ -125,7 +125,7 @@ protected:
             m_solver.assert_expr(fml1);
             lbool is_sat = m_solver.check();
             TRACE("ctx_solver_simplify_tactic", tout << "is non-equivalence sat?: " << is_sat << "\n";);
-            if (is_sat != l_false) {
+            if (is_sat == l_true) {
                 TRACE("ctx_solver_simplify_tactic", 
                       tout << "result is not equivalent to input\n";
                       tout << mk_pp(fml1, m) << "\n";);
diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h
index 397f6683b..ebdd1386c 100644
--- a/src/smt/theory_arith_aux.h
+++ b/src/smt/theory_arith_aux.h
@@ -1479,9 +1479,9 @@ namespace smt {
 
         SASSERT(max_gain.is_minus_one() || !max_gain.is_neg());
         SASSERT(min_gain.is_minus_one() || !min_gain.is_neg());
-        SASSERT(!is_int(x_i) || min_gain.is_pos());
-        SASSERT(!is_int(x_i) || min_gain.is_int());
-        SASSERT(!is_int(x_i) || max_gain.is_int());
+        //SASSERT(!is_int(x_i) || min_gain.is_pos());
+        //SASSERT(!is_int(x_i) || min_gain.is_int());
+        //SASSERT(!is_int(x_i) || max_gain.is_int());
         return is_tighter;
     }
 
diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index 2b91452a9..c47585606 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -3065,6 +3065,10 @@ namespace smt {
         SASSERT(v != null_theory_var);
         inf_numeral const & val = get_value(v);
         rational num = val.get_rational().to_rational() + m_epsilon.to_rational() * val.get_infinitesimal().to_rational();
+        if (is_int(v) && !num.is_int()) {
+            TRACE("arith", tout << "Truncating non-integer value. This is possible for non-linear constraints v" << v << " " << num << "\n";);
+            num = floor(num);
+        }
         return alloc(expr_wrapper_proc, m_factory->mk_value(num, is_int(v)));
     }