diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index 86c23a799..4ae6b6106 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -2043,7 +2043,15 @@ 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) {
-    SASSERT(decl->get_arity() == num_args || decl->is_right_associative() || decl->is_left_associative() || decl->is_chainable());
+    if (decl->get_arity() != num_args && 
+        !decl->is_right_associative() && 
+        !decl->is_left_associative() && 
+        !decl->is_chainable()) {
+        std::ostringstream buffer;
+        buffer << "Wrong number of arguments (" << num_args 
+               << ") passed to function " << mk_pp(decl, *this);        
+        throw ast_exception(buffer.str().c_str());
+    }
     app * r = 0;
     if (num_args > 2 && !decl->is_flat_associative()) {
         if (decl->is_right_associative()) {
diff --git a/src/math/euclid/euclidean_solver.cpp b/src/math/euclid/euclidean_solver.cpp
index 718dbb052..02ff1591e 100644
--- a/src/math/euclid/euclidean_solver.cpp
+++ b/src/math/euclid/euclidean_solver.cpp
@@ -717,7 +717,7 @@ struct euclidean_solver::imp {
                 elim_unit();
             else
                 decompose_and_elim();
-            TRACE("euclidean_solver_step", display(tout);); 
+            TRACE("euclidean_solver", display(tout);); 
             if (inconsistent()) return false;
         }
         return true;
diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h
index b600dd3c0..45c615e0c 100644
--- a/src/smt/theory_arith_int.h
+++ b/src/smt/theory_arith_int.h
@@ -1041,8 +1041,8 @@ namespace smt {
                     num_args = 1;
                     args     = &n;
                 }
-                for (unsigned j = 0; j < num_args; j++) {
-                    expr * arg = args[j];
+                for (unsigned i = 0; i < num_args; i++) {
+                    expr * arg = args[i];
                     expr * pp;
                     rational a_val;
                     get_monomial(arg, a_val, pp);