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/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)));
     }