diff --git a/RELEASE_NOTES b/RELEASE_NOTES
index 5ce4d2682..86e7039dd 100644
--- a/RELEASE_NOTES
+++ b/RELEASE_NOTES
@@ -427,11 +427,11 @@ Version 3.0
 
 - New Bitvector (QF_BV) solver. The new solver is only available when using the new SMT2 front-end.
 
-- Major performace improvements. 
+- Major performance improvements.
 
 - New preprocessing stack.
 
-- Performance improvements for linear and nonlinear arithmetic. The improvements are only available when using the the SMT2 front-end.
+- Performance improvements for linear and nonlinear arithmetic. The improvements are only available when using the SMT2 front-end.
 
 - Added API for parsing SMT2 files.
 
@@ -772,7 +772,7 @@ This release also introduces some new preprocessing features:
 
 - More efficient destructive equality resolution DER=true.
         
-- DISTRIBUTE_FORALL=true (distributes universal quatifiers over conjunctions, this transformation may affect pattern inference). 
+- DISTRIBUTE_FORALL=true (distributes universal quantifiers over conjunctions, this transformation may affect pattern inference).
 
 - Rewriter that uses universally quantified equations PRE_DEMODULATOR=true (yes, the option name is not good, we will change it in a future release).
 
@@ -842,7 +842,7 @@ This release introduces the following features:
 
 It fixes the following bugs:
 
-- Incorrect simplification of map over store in the extendted array theory. Reported by Catalin Hritcu.
+- Incorrect simplification of map over store in the extended array theory. Reported by Catalin Hritcu.
 
 - Incomplete handling of equality propagation with constant arrays. Reported by Catalin Hritcu.
 
@@ -886,7 +886,7 @@ Version 2.0
   proof object.
 
 - Proof Objects.
-  The #Z3_check_assumptions retuns a proof object if 
+  The #Z3_check_assumptions returns a proof object if
   the configuration flag PROOF_MODE is set to 1 or 2.
 
 - Partial support for non-linear arithmetic. 
@@ -899,4 +899,4 @@ Version 2.0
   The theory of well-founded recursive data-types is supported
   over the binary APIs. It supports ground satisfiability checking
   for tuples, enumeration types (scalars), 
-  lists and mututally recursive data-types.
+  lists and mutually recursive data-types.
diff --git a/src/api/api_context.h b/src/api/api_context.h
index a2321d7fe..7009250cc 100644
--- a/src/api/api_context.h
+++ b/src/api/api_context.h
@@ -51,7 +51,7 @@ namespace api {
     class context : public tactic_manager {
         struct add_plugins {  add_plugins(ast_manager & m); };
         context_params             m_params;
-        bool                       m_user_ref_count; //!< if true, the user is responsible for managing referenc counters.
+        bool                       m_user_ref_count; //!< if true, the user is responsible for managing reference counters.
         scoped_ptr<ast_manager>    m_manager;
         add_plugins                m_plugins;
 
@@ -158,7 +158,7 @@ namespace api {
         // Create a numeral of the given sort
         expr * mk_numeral_core(rational const & n, sort * s);
         
-        // Return a conjuction that will be exposed to the "external" world.
+        // Return a conjunction that will be exposed to the "external" world.
         expr * mk_and(unsigned num_exprs, expr * const * exprs);
 
         // Hack for preventing an AST for being GC when ref-count is not used
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 89b051eb5..49f6cfbf3 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -187,8 +187,8 @@ namespace z3 {
            \brief The C++ API uses by defaults exceptions on errors. 
            For applications that don't work well with exceptions (there should be only few)
            you have the ability to turn off exceptions. The tradeoffs are that applications
-           have to very careful about using check_error() after calls that may result in an errornous
-           state.
+           have to very careful about using check_error() after calls that may result in an
+           erroneous state.
          */
         void set_enable_exceptions(bool f) { m_enable_exceptions = f; }
 
@@ -213,7 +213,7 @@ namespace z3 {
 
         /**
            \brief Interrupt the current procedure being executed by any object managed by this context.
-           This is a soft interruption: there is no guarantee the object will actualy stop.
+           This is a soft interruption: there is no guarantee the object will actually stop.
         */
         void interrupt() { Z3_interrupt(m_ctx); }
 
@@ -709,7 +709,7 @@ namespace z3 {
 
            It only makes sense to use this function if the caller can ensure that
            the result is an integer or if exceptions are enabled. 
-           If exceptions are disabled, then use the the is_numeral_i function.
+           If exceptions are disabled, then use the is_numeral_i function.
            
            \pre is_numeral()
         */
@@ -729,7 +729,7 @@ namespace z3 {
 
            It only makes sense to use this function if the caller can ensure that
            the result is an integer or if exceptions are enabled. 
-           If exceptions are disabled, then use the the is_numeral_u function.           
+           If exceptions are disabled, then use the is_numeral_u function.
            \pre is_numeral()
         */
         unsigned get_numeral_uint() const {
diff --git a/src/api/dotnet/Statistics.cs b/src/api/dotnet/Statistics.cs
index cf4b703fe..c94af625c 100644
--- a/src/api/dotnet/Statistics.cs
+++ b/src/api/dotnet/Statistics.cs
@@ -56,7 +56,7 @@ namespace Microsoft.Z3
             public bool IsDouble { get { return m_is_double; } }
 
             /// <summary>
-            /// The string representation of the the entry's value.
+            /// The string representation of the entry's value.
             /// </summary>
             public string Value
             {
diff --git a/src/api/java/Context.java b/src/api/java/Context.java
index 7e73fc15e..ba96209b3 100644
--- a/src/api/java/Context.java
+++ b/src/api/java/Context.java
@@ -934,7 +934,7 @@ public class Context implements AutoCloseable {
      * exposed. It follows the semantics prescribed by the SMT-LIB standard.
      * 
      * You can take the floor of a real by creating an auxiliary integer Term
-     * {@code k} and and asserting
+     * {@code k} and asserting
      * {@code MakeInt2Real(k) &lt;= t1 &lt; MkInt2Real(k)+1}. The argument
      * must be of integer sort. 
      **/
diff --git a/src/api/java/Statistics.java b/src/api/java/Statistics.java
index 356cbeadb..d509424ed 100644
--- a/src/api/java/Statistics.java
+++ b/src/api/java/Statistics.java
@@ -65,7 +65,7 @@ public class Statistics extends Z3Object {
         }
 
         /**
-         * The string representation of the the entry's value.
+         * The string representation of the entry's value.
          * 
          * @throws Z3Exception
          **/
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 4896a475d..c28a14c3b 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -5741,7 +5741,7 @@ class ModelRef(Z3PPObject):
             return None
 
     def num_sorts(self):
-        """Return the number of unintepreted sorts that contain an interpretation in the model `self`.
+        """Return the number of uninterpreted sorts that contain an interpretation in the model `self`.
 
         >>> A = DeclareSort('A')
         >>> a, b = Consts('a b', A)
@@ -5756,7 +5756,7 @@ class ModelRef(Z3PPObject):
         return int(Z3_model_get_num_sorts(self.ctx.ref(), self.model))
 
     def get_sort(self, idx):
-        """Return the unintepreted sort at position `idx` < self.num_sorts().
+        """Return the uninterpreted sort at position `idx` < self.num_sorts().
 
         >>> A = DeclareSort('A')
         >>> B = DeclareSort('B')
@@ -5796,7 +5796,7 @@ class ModelRef(Z3PPObject):
         return [ self.get_sort(i) for i in range(self.num_sorts()) ]
 
     def get_universe(self, s):
-        """Return the intepretation for the uninterpreted sort `s` in the model `self`.
+        """Return the interpretation for the uninterpreted sort `s` in the model `self`.
 
         >>> A = DeclareSort('A')
         >>> a, b = Consts('a b', A)
@@ -5816,7 +5816,7 @@ class ModelRef(Z3PPObject):
             return None
 
     def __getitem__(self, idx):
-        """If `idx` is an integer, then the declaration at position `idx` in the model `self` is returned. If `idx` is a declaration, then the actual interpreation is returned.
+        """If `idx` is an integer, then the declaration at position `idx` in the model `self` is returned. If `idx` is a declaration, then the actual interpretation is returned.
 
         The elements can be retrieved using position or the actual declaration.
 
@@ -5860,7 +5860,7 @@ class ModelRef(Z3PPObject):
         return None
 
     def decls(self):
-        """Return a list with all symbols that have an interpreation in the model `self`.
+        """Return a list with all symbols that have an interpretation in the model `self`.
         >>> f = Function('f', IntSort(), IntSort())
         >>> x = Int('x')
         >>> s = Solver()
diff --git a/src/api/z3_fixedpoint.h b/src/api/z3_fixedpoint.h
index dc98fdb30..a651993ce 100644
--- a/src/api/z3_fixedpoint.h
+++ b/src/api/z3_fixedpoint.h
@@ -363,7 +363,7 @@ extern "C" {
     void Z3_API Z3_fixedpoint_set_reduce_assign_callback(
         Z3_context c ,Z3_fixedpoint d, Z3_fixedpoint_reduce_assign_callback_fptr cb);
 
-    /** \brief Register a callback for buildling terms based on the relational operators. */
+    /** \brief Register a callback for building terms based on the relational operators. */
     void Z3_API Z3_fixedpoint_set_reduce_app_callback(
         Z3_context c, Z3_fixedpoint d, Z3_fixedpoint_reduce_app_callback_fptr cb);
 
diff --git a/src/api/z3_fpa.h b/src/api/z3_fpa.h
index e92b728d7..358a3c619 100644
--- a/src/api/z3_fpa.h
+++ b/src/api/z3_fpa.h
@@ -433,7 +433,7 @@ extern "C" {
         \param c logical context
         \param rm term of RoundingMode sort
         \param t1 term of FloatingPoint sort
-        \param t2 term of FloatingPoint sor
+        \param t2 term of FloatingPoint sort
         \param t3 term of FloatingPoint sort
 
         The result is round((t1 * t2) + t3)
diff --git a/src/ast/format.cpp b/src/ast/format.cpp
index 835892121..6c2a02989 100644
--- a/src/ast/format.cpp
+++ b/src/ast/format.cpp
@@ -151,7 +151,7 @@ namespace format_ns {
     }
     
     format * mk_int(ast_manager & m, int i) {
-        static char buffer[128];
+        char buffer[128];
 #ifdef _WINDOWS
         sprintf_s(buffer, ARRAYSIZE(buffer), "%d", i);
 #else
@@ -161,7 +161,7 @@ namespace format_ns {
     }
     
     format * mk_unsigned(ast_manager & m, unsigned u) {
-        static char buffer[128];
+        char buffer[128];
 #ifdef _WINDOWS
         sprintf_s(buffer, ARRAYSIZE(buffer), "%u", u);
 #else
diff --git a/src/ast/proofs/proof_utils.cpp b/src/ast/proofs/proof_utils.cpp
index 58500cb79..722bfe14e 100644
--- a/src/ast/proofs/proof_utils.cpp
+++ b/src/ast/proofs/proof_utils.cpp
@@ -83,7 +83,7 @@ class reduce_hypotheses {
     // map from unit literals to their hypotheses-free derivations
     obj_map<expr, proof*> m_units;
 
-    // -- all hypotheses in the the proof
+    // -- all hypotheses in the proof
     obj_hashtable<expr> m_hyps;
 
     // marks hypothetical proofs
@@ -192,7 +192,7 @@ class reduce_hypotheses {
                 res = mk_lemma_core(args.get(0), m.get_fact(p));
                 compute_mark1(res);
             } else if (m.is_unit_resolution(p)) {
-                // unit: reduce untis; reduce the first premise; rebuild unit resolution
+                // unit: reduce units; reduce the first premise; rebuild unit resolution
                 res = mk_unit_resolution_core(args.size(), args.c_ptr());
                 compute_mark1(res);
             } else  {
@@ -340,7 +340,7 @@ void reduce_hypotheses(proof_ref &pr) {
 class reduce_hypotheses0 {
     typedef obj_hashtable<expr> expr_set;
     ast_manager&          m;
-    // reference for any expression created by the tranformation
+    // reference for any expression created by the transformation
     expr_ref_vector       m_refs;
     // currently computed result
     obj_map<proof,proof*> m_cache;
@@ -352,7 +352,7 @@ class reduce_hypotheses0 {
     unsigned_vector       m_limits;
     // map from proofs to active hypotheses
     obj_map<proof, expr_set*> m_hypmap;
-    // refernce train for hypotheses sets
+    // reference train for hypotheses sets
     ptr_vector<expr_set>  m_hyprefs;
     ptr_vector<expr>      m_literals;
     
@@ -492,7 +492,7 @@ public:
             // replace result by m_units[m.get_fact (p)] if defined
             // AG: This is the main step. Replace a hypothesis by a derivation of its consequence
             if (!m_units.find(m.get_fact(p), result)) {
-                // restore ther result back to p
+                // restore the result back to p
                 result = p.get();
             }
             // compute hypothesis of the result
diff --git a/src/ast/proofs/proof_utils.h b/src/ast/proofs/proof_utils.h
index b953c834d..455f39c4f 100644
--- a/src/ast/proofs/proof_utils.h
+++ b/src/ast/proofs/proof_utils.h
@@ -88,7 +88,7 @@ class elim_aux_assertions {
 
     app_ref m_aux;
 public:
-    elim_aux_assertions(app_ref aux) : m_aux(aux) {}
+    elim_aux_assertions(app_ref const& aux) : m_aux(aux) {}
 
     void mk_or_core(expr_ref_vector &args, expr_ref &res)
     {
diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp
index 65c8860b1..572abc8fe 100644
--- a/src/cmd_context/basic_cmds.cpp
+++ b/src/cmd_context/basic_cmds.cpp
@@ -761,7 +761,7 @@ public:
         return m_array_fid;
     }
     virtual char const * get_usage() const { return "<symbol> (<sort>+) <func-decl-ref>"; }
-    virtual char const * get_descr(cmd_context & ctx) const { return "declare a new array map operator with name <symbol> using the given function declaration.\n<func-decl-ref> ::= <symbol>\n                  | (<symbol> (<sort>*) <sort>)\n                  | ((_ <symbol> <numeral>+) (<sort>*) <sort>)\nThe last two cases are used to disumbiguate between declarations with the same name and/or select (indexed) builtin declarations.\nFor more details about the the array map operator, see 'Generalized and Efficient Array Decision Procedures' (FMCAD 2009).\nExample: (declare-map set-union (Int) (or (Bool Bool) Bool))\nDeclares a new function (declare-fun set-union ((Array Int Bool) (Array Int Bool)) (Array Int Bool)).\nThe instance of the map axiom for this new declaration is:\n(forall ((a1 (Array Int Bool)) (a2 (Array Int Bool)) (i Int)) (= (select (set-union a1 a2) i) (or (select a1 i) (select a2 i))))"; }
+    virtual char const * get_descr(cmd_context & ctx) const { return "declare a new array map operator with name <symbol> using the given function declaration.\n<func-decl-ref> ::= <symbol>\n                  | (<symbol> (<sort>*) <sort>)\n                  | ((_ <symbol> <numeral>+) (<sort>*) <sort>)\nThe last two cases are used to disumbiguate between declarations with the same name and/or select (indexed) builtin declarations.\nFor more details about the array map operator, see 'Generalized and Efficient Array Decision Procedures' (FMCAD 2009).\nExample: (declare-map set-union (Int) (or (Bool Bool) Bool))\nDeclares a new function (declare-fun set-union ((Array Int Bool) (Array Int Bool)) (Array Int Bool)).\nThe instance of the map axiom for this new declaration is:\n(forall ((a1 (Array Int Bool)) (a2 (Array Int Bool)) (i Int)) (= (select (set-union a1 a2) i) (or (select a1 i) (select a2 i))))"; }
     virtual unsigned get_arity() const { return 3; }
     virtual void prepare(cmd_context & ctx) { m_name = symbol::null; m_domain.reset(); }
     virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const {
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index 99d6c8284..212de585a 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -125,7 +125,7 @@ class stream_ref {
     std::ostream * m_stream;
     bool           m_owner;
 public:
-    stream_ref(std::string n, std::ostream & d):m_default_name(n), m_default(d), m_name(n), m_stream(&d), m_owner(false) {}
+    stream_ref(const std::string& n, std::ostream & d):m_default_name(n), m_default(d), m_name(n), m_stream(&d), m_owner(false) {}
     ~stream_ref() { reset(); }
     void set(char const * name);
     void set(std::ostream& strm);
diff --git a/src/duality/duality.h b/src/duality/duality.h
index 657fa18b4..28cf96df3 100644
--- a/src/duality/duality.h
+++ b/src/duality/duality.h
@@ -66,7 +66,7 @@ namespace Duality {
 
         bool is_variable(const Term &t);
 
-        FuncDecl SuffixFuncDecl(Term t, int n);
+        FuncDecl SuffixFuncDecl(const Term &t, int n);
 
 
         Term SubstRecHide(hash_map<ast, Term> &memo, const Term &t, int number);
diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp
index 5dc2283ae..9dae5eba9 100755
--- a/src/duality/duality_rpfp.cpp
+++ b/src/duality/duality_rpfp.cpp
@@ -2157,7 +2157,7 @@ namespace Duality {
         std::vector<Term> la_pos_vars;
         bool fixing;
     
-        void IndexLAcoeff(const Term &coeff1, const Term &coeff2, Term t, int id) {
+        void IndexLAcoeff(const Term &coeff1, const Term &coeff2, const Term &t, int id) {
             Term coeff = coeff1 * coeff2;
             coeff = coeff.simplify();
             Term is_pos = (coeff >= ctx.int_val(0));
@@ -3303,7 +3303,7 @@ namespace Duality {
     // This returns a new FuncDel with same sort as top-level function
     // of term t, but with numeric suffix appended to name.
 
-    Z3User::FuncDecl Z3User::SuffixFuncDecl(Term t, int n)
+    Z3User::FuncDecl Z3User::SuffixFuncDecl(const Term &t, int n)
     {
         std::string name = t.decl().name().str() + "_" + string_of_int(n);
         std::vector<sort> sorts;
diff --git a/src/duality/duality_solver.cpp b/src/duality/duality_solver.cpp
index 1711b65ad..59e68e046 100644
--- a/src/duality/duality_solver.cpp
+++ b/src/duality/duality_solver.cpp
@@ -107,14 +107,14 @@ namespace Duality {
 
     struct InternalError {
         std::string msg;
-        InternalError(const std::string _msg)
+        InternalError(const std::string & _msg)
             : msg(_msg) {}
     };
 
 
-    /** This is the main solver. It takes anarbitrary (possibly cyclic)
+    /** This is the main solver. It takes an arbitrary (possibly cyclic)
         RPFP and either annotates it with a solution, or returns a
-        counterexample derivation in the form of an embedd RPFP tree. */
+        counterexample derivation in the form of an embedded RPFP tree. */
 
     class Duality : public Solver {
 
diff --git a/src/duality/duality_wrapper.h b/src/duality/duality_wrapper.h
index 96c49b36b..18b6948d5 100644
--- a/src/duality/duality_wrapper.h
+++ b/src/duality/duality_wrapper.h
@@ -191,7 +191,7 @@ namespace Duality {
         sort int_sort();
         sort real_sort();
         sort bv_sort(unsigned sz);
-        sort array_sort(sort d, sort r);
+        sort array_sort(const sort & d, const sort & r);
 
         func_decl function(symbol const & name, unsigned arity, sort const * domain, sort const & range);
         func_decl function(char const * name, unsigned arity, sort const * domain, sort const & range);
@@ -763,11 +763,11 @@ namespace Duality {
         unsigned size() const;
         func_decl operator[](unsigned i) const;
 
-        expr get_const_interp(func_decl f) const {
+        expr get_const_interp(const func_decl & f) const {
             return ctx().cook(m_model->get_const_interp(to_func_decl(f.raw())));
         }
 
-        func_interp get_func_interp(func_decl f) const {
+        func_interp get_func_interp(const func_decl & f) const {
             return func_interp(ctx(),m_model->get_func_interp(to_func_decl(f.raw())));
         }
 
@@ -1169,7 +1169,7 @@ namespace Duality {
         ::sort *s = m().mk_sort(m_arith_fid, REAL_SORT);
         return sort(*this, s);
     }
-    inline sort context::array_sort(sort d, sort r) {
+    inline sort context::array_sort(const sort & d, const sort & r) {
         parameter params[2]  = { parameter(d), parameter(to_sort(r)) };
         ::sort * s =  m().mk_sort(m_array_fid, ARRAY_SORT, 2, params);
         return sort(*this, s);
@@ -1274,11 +1274,11 @@ namespace Duality {
     class TermTree {
     public:
 
-        TermTree(expr _term){
+        TermTree(const expr &_term){
             term = _term;
         }
 
-        TermTree(expr _term, const std::vector<TermTree *> &_children){
+        TermTree(const expr &_term, const std::vector<TermTree *> &_children){
             term = _term;
             children = _children;
         }
@@ -1302,9 +1302,9 @@ namespace Duality {
             return num;
         }
 
-        inline void setTerm(expr t){term = t;}
+        inline void setTerm(const expr &t){term = t;}
 
-        inline void addTerm(expr t){terms.push_back(t);}
+        inline void addTerm(const expr &t){terms.push_back(t);}
 
         inline void setChildren(const std::vector<TermTree *> & _children){
             children = _children;
diff --git a/src/math/polynomial/polynomial.h b/src/math/polynomial/polynomial.h
index b09af94bc..c4dedb043 100644
--- a/src/math/polynomial/polynomial.h
+++ b/src/math/polynomial/polynomial.h
@@ -233,7 +233,7 @@ namespace polynomial {
 
         /**
            \brief Install a "delete polynomial" event handler.
-           The even hanlder is not owned by the polynomial manager.
+           The event handler is not owned by the polynomial manager.
            If eh = 0, then it uninstall the event handler.
         */
         void add_del_eh(del_eh * eh);
@@ -426,7 +426,7 @@ namespace polynomial {
         polynomial * flip_sign_if_lm_neg(polynomial const * p);
 
         /**
-           \breif Return the gcd g of p and q.
+           \brief Return the gcd g of p and q.
         */
         void gcd(polynomial const * p, polynomial const * q, polynomial_ref & g);
 
@@ -853,7 +853,7 @@ namespace polynomial {
         void resultant(polynomial const * p, polynomial const * q, var x, polynomial_ref & r);
         
         /**
-           \brief Stroe in r the discriminant of p with respect to variable x.
+           \brief Store in r the discriminant of p with respect to variable x.
            discriminant(p, x, r) == resultant(p, derivative(p, x), x, r)
         */
         void discriminant(polynomial const * p, var x, polynomial_ref & r);
@@ -959,7 +959,7 @@ namespace polynomial {
         }
 
         /**
-           \brief Apply substiution [x -> p/q] in r.
+           \brief Apply substitution [x -> p/q] in r.
            That is, given r \in Z[x, y_1, .., y_m] return
            polynomial q^k * r(p/q, y_1, .., y_m), where k is the maximal degree of x in r.
         */
diff --git a/src/math/polynomial/upolynomial_factorization.cpp b/src/math/polynomial/upolynomial_factorization.cpp
index 11a37648a..a1f6e6ec1 100644
--- a/src/math/polynomial/upolynomial_factorization.cpp
+++ b/src/math/polynomial/upolynomial_factorization.cpp
@@ -152,7 +152,7 @@ public:
     }
 
     /**
-       \brief 'Disagonalizes' the matrix using only column operations. The reusling matrix will have -1 at pivot 
+       \brief 'Diagonalizes' the matrix using only column operations. The resulting matrix will have -1 at pivot
        elements. Returns the rank of the null space.
     */
     unsigned diagonalize() {
@@ -170,7 +170,7 @@ public:
                     m_column_pivot[j] = i;
                     m_row_pivot[i] = j;
 
-                    // found a pivot, to make it -1 we compute the multuplier -p^-1
+                    // found a pivot, to make it -1 we compute the multiplier -p^-1
                     m_zpm.set(multiplier, get(i, j));
                     m_zpm.inv(multiplier);
                     m_zpm.neg(multiplier);
@@ -201,7 +201,7 @@ public:
     }
 
     /**
-       If rank of the matrix is n - r, we are interested in linearly indeprendent vectors v_1, ..., v_r (the basis of 
+       If rank of the matrix is n - r, we are interested in linearly independent vectors v_1, ..., v_r (the basis of
        the null space), such that v_k A = 0. This method will give one at a time. The method returns true if vector has
        been computed properly. The first vector [1, 0, ..., 0] is ignored (m_null_row starts from 1).       
     */
@@ -417,7 +417,7 @@ bool zp_factor_square_free_berlekamp(zp_manager & upm, numeral_vector const & f,
     // construct the berlekamp Q matrix to get the null space
     berlekamp_matrix Q_I(upm, f);
     
-    // copy the inital polynomial to factors
+    // copy the initial polynomial to factors
     unsigned first_factor = factors.distinct_factors();
     factors.push_back(f, 1);
 
@@ -473,7 +473,7 @@ bool zp_factor_square_free_berlekamp(zp_manager & upm, numeral_vector const & f,
                 // get the gcd
                 upm.gcd(v_k.size(), v_k.c_ptr(), current_factor.size(), current_factor.c_ptr(), gcd);
 
-                // if the gcd is 1, or the the gcd is f, we just ignroe it
+                // if the gcd is 1, or the gcd is f, we just ignore it
                 if (gcd.size() != 1 && gcd.size() != current_factor.size()) {
                 
                     // get the divisor also (no need to normalize the div, both are monic)
@@ -568,13 +568,13 @@ bool check_hansel_lift(z_manager & upm, numeral_vector const & C,
 }
 
 /**
-   Performs a Hensel lift of A and B in Z_a to Z_b, where p is prime and and a = p^{a_k}, b = p^{b_k},
+   Performs a Hensel lift of A and B in Z_a to Z_b, where p is prime and a = p^{a_k}, b = p^{b_k},
    r = (a, b), with the following assumptions:
    
-     (1) UA + VB = 1 (mod a) 
+     (1) UA + VB = 1 (mod a)
      (2) C = A*B (mod b)
-     (3) (l(A), r) = 1 (importand in order to divide by A, i.e. to invert l(A))
-     (4) deg(A) + deg(B) = deg(C)     
+     (3) (l(A), r) = 1 (important in order to divide by A, i.e. to invert l(A))
+     (4) deg(A) + deg(B) = deg(C)
 
    The output of is two polynomials A1, B1  such that A1 = A (mod b), B1 = B (mod b), 
    l(A1) = l(A), deg(A1) = deg(A), deg(B1) = deg(B) and C = A1 B1 (mod b*r). Such A1, B1 are unique if 
@@ -625,7 +625,7 @@ void hensel_lift(z_manager & upm, numeral const & a, numeral const & b, numeral
     // having (1) AU + BV = 1 (mod r) and (5) AT + BS = f (mod r), we know that 
     // A*(fU) + B*(fV) = f (mod r), i.e. T = fU, S = fV is a solution
     // but we also know that we need an S with deg(S) <= deg(A) so we can do the following
-    // we know that l(A) is invertible so we can find the exact remainder of fV with A, i.e. find the qotient 
+    // we know that l(A) is invertible so we can find the exact remainder of fV with A, i.e. find the quotient
     // t in the division and set
     // A*(fU + tB) + B*(fV - tA) = f 
     // T = fU + tB, S = fU - tA
@@ -1093,7 +1093,7 @@ bool factor_square_free(z_manager & upm, numeral_vector const & f, factors & fs,
             continue;
         }
     
-        // if it's not square free, we also try somehting else 
+        // if it's not square free, we also try something else
         scoped_numeral_vector f_pp_zp(nm);
         to_zp_manager(zp_upm, f_pp, f_pp_zp);
 
@@ -1170,7 +1170,7 @@ bool factor_square_free(z_manager & upm, numeral_vector const & f, factors & fs,
     zp_numeral_manager & zpe_nm = zpe_upm.m();
     
     zp_factors zpe_fs(zpe_upm);
-    // this might give something bigger than p^e, but the lifting proocedure will update the zpe_nm
+    // this might give something bigger than p^e, but the lifting procedure will update the zpe_nm
     // zp factors are monic, so will be the zpe factors, i.e. f_pp = zpe_fs * lc(f_pp) (mod p^e)
     hensel_lift(upm, f_pp, zp_fs, e, zpe_fs); 
     
@@ -1182,7 +1182,7 @@ bool factor_square_free(z_manager & upm, numeral_vector const & f, factors & fs,
     scoped_numeral f_pp_lc(nm);
     zpe_nm.set(f_pp_lc, f_pp.back());
     
-    // we always keep in f_pp the the actual primitive part f_pp*lc(f_pp)
+    // we always keep in f_pp the actual primitive part f_pp*lc(f_pp)
     upm.mul(f_pp, f_pp_lc);
     
     // now we go through the combinations of factors to check construct the factorization
@@ -1287,7 +1287,7 @@ bool factor_square_free(z_manager & upm, numeral_vector const & f, factors & fs,
         fs.push_back(f_pp, k);
     } 
     else {
-        // if a constant it must be 1 (it was primitve)
+        // if a constant it must be 1 (it was primitive)
         SASSERT(f_pp.size() == 1 && nm.is_one(f_pp.back()));
     }
 
diff --git a/src/math/polynomial/upolynomial_factorization.h b/src/math/polynomial/upolynomial_factorization.h
index 6fe0f2be6..c33f1844d 100644
--- a/src/math/polynomial/upolynomial_factorization.h
+++ b/src/math/polynomial/upolynomial_factorization.h
@@ -34,12 +34,12 @@ namespace upolynomial {
     typedef manager::scoped_numeral scoped_numeral;
 
     /**
-       \breif Factor f into f = f_1^k_1 * ... * p_n^k_n, such that p_i are square-free and coprime.
+       \brief Factor f into f = f_1^k_1 * ... * p_n^k_n, such that p_i are square-free and coprime.
     */
     void zp_square_free_factor(zp_manager & zp_upm, numeral_vector const & f, zp_factors & sq_free_factors);
 
     /**
-       \brief Factor the monic square-free polynomial f from Z_p[x]. Returns true if factorization was sucesseful, or false 
+       \brief Factor the monic square-free polynomial f from Z_p[x]. Returns true if factorization was successful, or false
        if f is an irreducible square-free polynomial in Z_p[x].
     */
     bool zp_factor_square_free(zp_manager & zp_upm, numeral_vector const & f, zp_factors & factors);
@@ -55,17 +55,17 @@ namespace upolynomial {
     bool zp_factor_square_free_berlekamp(zp_manager & zp_upm, numeral_vector const & f, zp_factors & factors, bool randomized = true);
 
     /**
-       \brief Factor the polynomial f from Z_p[x]. Returns true if factorization was sucesseful, or false if f is
+       \brief Factor the polynomial f from Z_p[x]. Returns true if factorization was successful, or false if f is
        an irreducible polynomial in Z_p[x]
     */
     bool zp_factor(zp_manager & zp_upm, numeral_vector const & f, zp_factors & factors);
 
     /**
-        \brief Performs a Hensel lift of A and B in Z_a to Z_b, where p is prime and and a = p^{a_k}, b = p^{b_k},
+        \brief Performs a Hensel lift of A and B in Z_a to Z_b, where p is prime and a = p^{a_k}, b = p^{b_k},
         r = (a, b), with the following assumptions:
          * UA + VB = 1 (mod a) 
          * C = AB (mod b)
-         * (l(A), r) = 1 (importand in order to divide by A, i.e. to invert l(A))
+         * (l(A), r) = 1 (important in order to divide by A, i.e. to invert l(A))
         the output of is two polynomials A1, B1 (replacing A and B) such that A1 = A (mod b), B1 = B (mod b), 
         l(A1) = l(A), deg(A1) = deg(A), deg(B1) = deg(B) and C = A1 B1 (mod b*r). Such A1, B1 are unique if 
         r is prime. See [3] p. 138.
@@ -82,7 +82,7 @@ namespace upolynomial {
     void hensel_lift(z_manager & upm, numeral_vector const & f, zp_factors const & factors_p, unsigned e, zp_factors & factors_pe);
 
     /**
-       \brief Factor the square-free polynomial f from Z[x]. Returns true if factorization was sucesseful, or false if 
+       \brief Factor the square-free polynomial f from Z[x]. Returns true if factorization was successful, or false if
        f is an irreducible polynomial in Z[x]. The vector of factors is cleared.
     */
     bool factor_square_free(z_manager & upm, numeral_vector const & f, factors & fs, factor_params const & ps = factor_params());
diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp
index 39e044ec3..78860bdde 100644
--- a/src/muz/base/dl_context.cpp
+++ b/src/muz/base/dl_context.cpp
@@ -400,7 +400,7 @@ namespace datalog {
         }
         uint64 res;
         if (!try_get_sort_constant_count(srt, res)) {
-            sort_size sz = srt->get_num_elements();
+            const sort_size & sz = srt->get_num_elements();
             if (sz.is_finite()) {
                 res = sz.size();
             }
@@ -411,7 +411,7 @@ namespace datalog {
         return res;
     }
 
-    void context::set_argument_names(const func_decl * pred, svector<symbol> var_names)
+    void context::set_argument_names(const func_decl * pred, const svector<symbol> & var_names)
     {
         SASSERT(!m_argument_var_names.contains(pred));
         m_argument_var_names.insert(pred, var_names);
diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h
index 129277514..0fb68d396 100644
--- a/src/muz/base/dl_context.h
+++ b/src/muz/base/dl_context.h
@@ -368,7 +368,7 @@ namespace datalog {
            These names are used when printing out the relations to make the output conform 
            to the one of bddbddb.
         */
-        void set_argument_names(const func_decl * pred, svector<symbol> var_names);
+        void set_argument_names(const func_decl * pred, const svector<symbol> & var_names);
         symbol get_argument_name(const func_decl * pred, unsigned arg_index);
 
         void set_predicate_representation(func_decl * pred, unsigned relation_name_cnt, 
diff --git a/src/muz/base/dl_util.cpp b/src/muz/base/dl_util.cpp
index 787dc6cfa..715964e3a 100644
--- a/src/muz/base/dl_util.cpp
+++ b/src/muz/base/dl_util.cpp
@@ -547,7 +547,7 @@ namespace datalog {
     //
     // -----------------------------------
 
-    void get_file_names(std::string directory, std::string extension, bool traverse_subdirs, 
+    void get_file_names(std::string directory, const std::string & extension, bool traverse_subdirs,
             string_vector & res) {
 
         if(directory[directory.size()-1]!='\\' && directory[directory.size()-1]!='/') {
@@ -595,7 +595,7 @@ namespace datalog {
 #endif
     }
 
-    bool file_exists(std::string name) {
+    bool file_exists(const std::string & name) {
         struct stat st;
         if(stat(name.c_str(),&st) == 0) {
             return true;
@@ -603,7 +603,7 @@ namespace datalog {
         return false;
     }
 
-    bool is_directory(std::string name) {
+    bool is_directory(const std::string & name) {
         if(!file_exists(name)) {
             return false;
         }
@@ -612,7 +612,7 @@ namespace datalog {
         return (status.st_mode&S_IFDIR)!=0;
     }
 
-    std::string get_file_name_without_extension(std::string name) {
+    std::string get_file_name_without_extension(const std::string & name) {
         size_t slash_index = name.find_last_of("\\/");
         size_t dot_index = name.rfind('.');
         size_t ofs = (slash_index==std::string::npos) ? 0 : slash_index+1;
diff --git a/src/muz/base/dl_util.h b/src/muz/base/dl_util.h
index 6b689fd17..32f016f63 100644
--- a/src/muz/base/dl_util.h
+++ b/src/muz/base/dl_util.h
@@ -290,7 +290,7 @@ namespace datalog {
     }
 
     template<class T>
-    void project_out_vector_columns(T & container, const unsigned_vector removed_cols) {
+    void project_out_vector_columns(T & container, const unsigned_vector & removed_cols) {
         project_out_vector_columns(container, removed_cols.size(), removed_cols.c_ptr());
     }
 
@@ -342,7 +342,7 @@ namespace datalog {
     }
 
     template<class T>
-    void permutate_by_cycle(T & container, const unsigned_vector permutation_cycle) {
+    void permutate_by_cycle(T & container, const unsigned_vector & permutation_cycle) {
         permutate_by_cycle(container, permutation_cycle.size(), permutation_cycle.c_ptr());
     }
 
@@ -578,13 +578,13 @@ namespace datalog {
     //
     // -----------------------------------
 
-    void get_file_names(std::string directory, std::string extension, bool traverse_subdirs, 
+    void get_file_names(std::string directory, const std::string & extension, bool traverse_subdirs, 
         string_vector & res);
 
-    bool file_exists(std::string name);
-    bool is_directory(std::string name);
+    bool file_exists(const std::string & name);
+    bool is_directory(const std::string & name);
 
-    std::string get_file_name_without_extension(std::string name);
+    std::string get_file_name_without_extension(const std::string & name);
 
     // -----------------------------------
     //
diff --git a/src/muz/fp/datalog_parser.cpp b/src/muz/fp/datalog_parser.cpp
index 7191f1931..f839c5c5a 100644
--- a/src/muz/fp/datalog_parser.cpp
+++ b/src/muz/fp/datalog_parser.cpp
@@ -1303,7 +1303,7 @@ private:
         }
     }
 
-    void parse_rules_file(std::string fname) {
+    void parse_rules_file(const std::string & fname) {
         SASSERT(file_exists(fname));
         flet<std::string> flet_cur_file(m_current_file, fname);
 
@@ -1347,7 +1347,7 @@ private:
         return true;
     }
 
-    void parse_rel_file(std::string fname) {
+    void parse_rel_file(const std::string & fname) {
         SASSERT(file_exists(fname));
 
         IF_VERBOSE(10, verbose_stream() << "Parsing relation file " << fname << "\n";);
@@ -1496,7 +1496,7 @@ private:
         return true;
     }
 
-    void parse_map_file(std::string fname) {
+    void parse_map_file(const std::string & fname) {
         SASSERT(file_exists(fname));
 
         IF_VERBOSE(10, verbose_stream() << "Parsing map file " << fname << "\n";);
diff --git a/src/muz/rel/aig_exporter.cpp b/src/muz/rel/aig_exporter.cpp
index bc98ab1f8..3fed47f80 100644
--- a/src/muz/rel/aig_exporter.cpp
+++ b/src/muz/rel/aig_exporter.cpp
@@ -32,7 +32,7 @@ namespace datalog {
             predicates.insert(I->first);
         }
 
-        // reserve pred id = 0 for initalization purposes
+        // reserve pred id = 0 for initialization purposes
         unsigned num_preds = (unsigned)predicates.size() + 1;
 
         // poor's man round-up log2
diff --git a/src/muz/rel/dl_finite_product_relation.cpp b/src/muz/rel/dl_finite_product_relation.cpp
index c036d3cfd..163ba1b0b 100644
--- a/src/muz/rel/dl_finite_product_relation.cpp
+++ b/src/muz/rel/dl_finite_product_relation.cpp
@@ -1924,7 +1924,7 @@ namespace datalog {
         }
     }
 
-    void finite_product_relation::extract_table_fact(const relation_fact rf, table_fact & tf) const {
+    void finite_product_relation::extract_table_fact(const relation_fact & rf, table_fact & tf) const {
         const relation_signature & sig = get_signature();
         relation_manager & rmgr = get_manager();
 
@@ -1940,7 +1940,7 @@ namespace datalog {
         tf.push_back(0);
     }
 
-    void finite_product_relation::extract_other_fact(const relation_fact rf, relation_fact & of) const {
+    void finite_product_relation::extract_other_fact(const relation_fact & rf, relation_fact & of) const {
         of.reset();
         unsigned o_sz = m_other_sig.size();
         for(unsigned i=0; i<o_sz; i++) {
diff --git a/src/muz/rel/dl_finite_product_relation.h b/src/muz/rel/dl_finite_product_relation.h
index 946296df1..e13b7fcf9 100644
--- a/src/muz/rel/dl_finite_product_relation.h
+++ b/src/muz/rel/dl_finite_product_relation.h
@@ -281,11 +281,11 @@ namespace datalog {
            \brief Extract the values of table non-functional columns from the relation fact.
            The value of the functional column which determines index of the inner relation is undefined.
          */
-        void extract_table_fact(const relation_fact rf, table_fact & tf) const;
+        void extract_table_fact(const relation_fact & rf, table_fact & tf) const;
         /**
            \brief Extract the values of the inner relation columns from the relation fact.
          */
-        void extract_other_fact(const relation_fact rf, relation_fact & of) const;
+        void extract_other_fact(const relation_fact & rf, relation_fact & of) const;
 
         relation_base * mk_empty_inner();
         relation_base * mk_full_inner(func_decl* pred);
diff --git a/src/muz/rel/dl_instruction.cpp b/src/muz/rel/dl_instruction.cpp
index fb718d8b8..26139fb7c 100644
--- a/src/muz/rel/dl_instruction.cpp
+++ b/src/muz/rel/dl_instruction.cpp
@@ -168,7 +168,7 @@ namespace datalog {
     }
 
 
-    void instruction::display_indented(execution_context const & _ctx, std::ostream & out, std::string indentation) const {
+    void instruction::display_indented(execution_context const & _ctx, std::ostream & out, const std::string & indentation) const {
         out << indentation;
         rel_context const& ctx = _ctx.get_rel_context();
         display_head_impl(_ctx, out);
@@ -190,7 +190,7 @@ namespace datalog {
         func_decl_ref m_pred;
         reg_idx m_reg;
     public:
-        instr_io(bool store, func_decl_ref pred, reg_idx reg)
+        instr_io(bool store, func_decl_ref const& pred, reg_idx reg)
             : m_store(store), m_pred(pred), m_reg(reg) {}
         virtual bool perform(execution_context & ctx) {
             log_verbose(ctx);            
@@ -348,7 +348,7 @@ namespace datalog {
             out << "while";
             print_container(m_controls, out);
         }
-        virtual void display_body_impl(execution_context const & ctx, std::ostream & out, std::string indentation) const {
+        virtual void display_body_impl(execution_context const & ctx, std::ostream & out, const std::string & indentation) const {
             m_body->display_indented(ctx, out, indentation+"    ");
         }
     };
@@ -1182,7 +1182,7 @@ namespace datalog {
         }
     }
 
-    void instruction_block::display_indented(execution_context const& _ctx, std::ostream & out, std::string indentation) const {
+    void instruction_block::display_indented(execution_context const& _ctx, std::ostream & out, const std::string & indentation) const {
         rel_context const& ctx = _ctx.get_rel_context();
         instr_seq_type::const_iterator it = m_data.begin();
         instr_seq_type::const_iterator end = m_data.end();
diff --git a/src/muz/rel/dl_instruction.h b/src/muz/rel/dl_instruction.h
index 56dd249a5..d2e1c30f5 100644
--- a/src/muz/rel/dl_instruction.h
+++ b/src/muz/rel/dl_instruction.h
@@ -150,7 +150,7 @@ namespace datalog {
             return m_reg_annotation.find(reg, res);
         }
 
-        void set_register_annotation(reg_idx reg, std::string str) {
+        void set_register_annotation(reg_idx reg, const std::string & str) {
             m_reg_annotation.insert(reg, str);
         }
 
@@ -233,7 +233,7 @@ namespace datalog {
 
            Each line must be prepended by \c indentation and ended by a newline character.
         */
-        virtual void display_body_impl(execution_context const & ctx, std::ostream & out, std::string indentation) const {}
+        virtual void display_body_impl(execution_context const & ctx, std::ostream & out, const std::string & indentation) const {}
         void log_verbose(execution_context& ctx);
 
     public:
@@ -249,7 +249,7 @@ namespace datalog {
         void display(execution_context const& ctx, std::ostream & out) const {
             display_indented(ctx, out, "");
         }
-        void display_indented(execution_context const & ctx, std::ostream & out, std::string indentation) const;
+        void display_indented(execution_context const & ctx, std::ostream & out, const std::string & indentation) const;
 
         static instruction * mk_load(ast_manager & m, func_decl * pred, reg_idx tgt);
         /**
@@ -359,7 +359,7 @@ namespace datalog {
         void display(execution_context const & ctx, std::ostream & out) const {
             display_indented(ctx, out, "");
         }
-        void display_indented(execution_context const & ctx, std::ostream & out, std::string indentation) const;
+        void display_indented(execution_context const & ctx, std::ostream & out, const std::string & indentation) const;
 
         unsigned num_instructions() const { return m_data.size(); }
     };
diff --git a/src/muz/rel/dl_mk_explanations.cpp b/src/muz/rel/dl_mk_explanations.cpp
index c4fb57eeb..ca04ca099 100644
--- a/src/muz/rel/dl_mk_explanations.cpp
+++ b/src/muz/rel/dl_mk_explanations.cpp
@@ -454,7 +454,7 @@ namespace datalog {
             : m_manager(ctx.get_manager()), 
               m_subst(ctx.get_var_subst()), 
               m_col_idx(col_idx), 
-              m_new_rule(new_rule) {}
+              m_new_rule(std::move(new_rule)) {}
 
         virtual void operator()(relation_base & r0) {
             explanation_relation & r = static_cast<explanation_relation &>(r0);
diff --git a/src/muz/rel/dl_product_relation.cpp b/src/muz/rel/dl_product_relation.cpp
index 8a2029748..1a91d6828 100644
--- a/src/muz/rel/dl_product_relation.cpp
+++ b/src/muz/rel/dl_product_relation.cpp
@@ -488,7 +488,7 @@ namespace datalog {
         ptr_vector<relation_transformer_fn> m_transforms;
     public:
         transform_fn(relation_signature s, unsigned num_trans, relation_transformer_fn** trans):
-          m_sig(s),
+          m_sig(std::move(s)),
           m_transforms(num_trans, trans) {}
 
           ~transform_fn() { dealloc_ptr_vector_content(m_transforms); }
diff --git a/src/muz/rel/dl_relation_manager.h b/src/muz/rel/dl_relation_manager.h
index 610c523e1..088b246e4 100644
--- a/src/muz/rel/dl_relation_manager.h
+++ b/src/muz/rel/dl_relation_manager.h
@@ -289,7 +289,7 @@ namespace datalog {
         relation_transformer_fn * mk_permutation_rename_fn(const relation_base & t, 
             const unsigned * permutation);
         relation_transformer_fn * mk_permutation_rename_fn(const relation_base & t, 
-                const unsigned_vector permutation) {
+                const unsigned_vector & permutation) {
             SASSERT(t.get_signature().size()==permutation.size());
             return mk_permutation_rename_fn(t, permutation.c_ptr());
         }
@@ -343,7 +343,7 @@ namespace datalog {
 
         relation_mutator_fn * mk_filter_identical_fn(const relation_base & t, unsigned col_cnt, 
             const unsigned * identical_cols);
-        relation_mutator_fn * mk_filter_identical_fn(const relation_base & t, const unsigned_vector identical_cols) {
+        relation_mutator_fn * mk_filter_identical_fn(const relation_base & t, const unsigned_vector & identical_cols) {
             return mk_filter_identical_fn(t, identical_cols.size(), identical_cols.c_ptr());
         }
 
@@ -468,7 +468,7 @@ namespace datalog {
            of column number.
         */
         table_transformer_fn * mk_permutation_rename_fn(const table_base & t, const unsigned * permutation);
-        table_transformer_fn * mk_permutation_rename_fn(const table_base & t, const unsigned_vector permutation) {
+        table_transformer_fn * mk_permutation_rename_fn(const table_base & t, const unsigned_vector & permutation) {
             SASSERT(t.get_signature().size()==permutation.size());
             return mk_permutation_rename_fn(t, permutation.c_ptr());
         }
@@ -522,7 +522,7 @@ namespace datalog {
 
         table_mutator_fn * mk_filter_identical_fn(const table_base & t, unsigned col_cnt, 
             const unsigned * identical_cols);
-        table_mutator_fn * mk_filter_identical_fn(const table_base & t, const unsigned_vector identical_cols) {
+        table_mutator_fn * mk_filter_identical_fn(const table_base & t, const unsigned_vector & identical_cols) {
             return mk_filter_identical_fn(t, identical_cols.size(), identical_cols.c_ptr());
         }
 
diff --git a/src/muz/rel/dl_sieve_relation.cpp b/src/muz/rel/dl_sieve_relation.cpp
index 0d70212e2..7e274cbef 100644
--- a/src/muz/rel/dl_sieve_relation.cpp
+++ b/src/muz/rel/dl_sieve_relation.cpp
@@ -67,7 +67,7 @@ namespace datalog {
     }
 
     relation_base * sieve_relation::complement(func_decl* p) const {
-        //this is not precisely a complement, because we still treat the ignored collumns as
+        //this is not precisely a complement, because we still treat the ignored columns as
         //full, but it should give reasonable results inside the product relation
         relation_base * new_inner = get_inner().complement(p);
         return get_plugin().mk_from_inner(get_signature(), m_inner_cols.c_ptr(), new_inner);
diff --git a/src/muz/rel/dl_sieve_relation.h b/src/muz/rel/dl_sieve_relation.h
index 021c9d8df..e369e04aa 100644
--- a/src/muz/rel/dl_sieve_relation.h
+++ b/src/muz/rel/dl_sieve_relation.h
@@ -108,7 +108,7 @@ namespace datalog {
 
         sieve_relation * mk_from_inner(const relation_signature & s, const bool * inner_columns, 
             relation_base * inner_rel);
-        sieve_relation * mk_from_inner(const relation_signature & s, const svector<bool> inner_columns, 
+        sieve_relation * mk_from_inner(const relation_signature & s, const svector<bool> & inner_columns, 
                 relation_base * inner_rel) {
             SASSERT(inner_columns.size()==s.size());
             return mk_from_inner(s, inner_columns.c_ptr(), inner_rel);
diff --git a/src/muz/rel/dl_sparse_table.h b/src/muz/rel/dl_sparse_table.h
index a699cf165..d3481dc7f 100644
--- a/src/muz/rel/dl_sparse_table.h
+++ b/src/muz/rel/dl_sparse_table.h
@@ -424,7 +424,7 @@ namespace datalog {
 
         /**
             \c array \c removed_cols contains column indexes to be removed in ascending order and
-            is terminated by a number greated than the highest column index of a join the the two tables. 
+            is terminated by a number greater than the highest column index of a join the two tables.
             This is to simplify the traversal of the array when building facts.
          */
         static void concatenate_rows(const column_layout & layout1, const column_layout & layout2,
@@ -436,7 +436,7 @@ namespace datalog {
            columns from t2 using indexing.
 
            \c array \c removed_cols contains column indexes to be removed in ascending order and
-           is terminated by a number greated than the highest column index of a join the the two tables. 
+           is terminated by a number greater than the highest column index of a join the two tables.
            This is to simplify the traversal of the array when building facts.
 
            \c tables_swapped value means that the resulting facts should contain facts from t2 first,
diff --git a/src/muz/rel/dl_table_relation.cpp b/src/muz/rel/dl_table_relation.cpp
index d8f1c7314..b8cf8e724 100644
--- a/src/muz/rel/dl_table_relation.cpp
+++ b/src/muz/rel/dl_table_relation.cpp
@@ -240,7 +240,7 @@ namespace datalog {
 
             const table_relation & tr_src = static_cast<const table_relation &>(src);
             relation_manager & rmgr = tr_src.get_manager();
-            relation_signature sig = tr_src.get_signature();
+            const relation_signature & sig = tr_src.get_signature();
             SASSERT(tgt.get_signature()==sig);
             SASSERT(!delta || delta->get_signature()==sig);
             
diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index b057730d8..28ff7d787 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -3418,7 +3418,7 @@ expr_ref context::get_constraints (unsigned level)
     return m_pm.mk_and (constraints);
 }
 
-void context::add_constraints (unsigned level, expr_ref c)
+void context::add_constraints (unsigned level, const expr_ref& c)
 {
     if (!c.get()) { return; }
     if (m.is_true(c)) { return; }
diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h
index cb422d08f..898c1639e 100644
--- a/src/muz/spacer/spacer_context.h
+++ b/src/muz/spacer/spacer_context.h
@@ -833,7 +833,7 @@ public:
     pob& get_root() const { return m_pob_queue.get_root(); }
 
     expr_ref get_constraints (unsigned lvl);
-    void add_constraints (unsigned lvl, expr_ref c);
+    void add_constraints (unsigned lvl, const expr_ref& c);
 };
 
 inline bool pred_transformer::use_native_mbp () {return ctx.use_native_mbp ();}
diff --git a/src/muz/spacer/spacer_matrix.cpp b/src/muz/spacer/spacer_matrix.cpp
index 3cc83996c..ea9b3cb32 100644
--- a/src/muz/spacer/spacer_matrix.cpp
+++ b/src/muz/spacer/spacer_matrix.cpp
@@ -42,7 +42,7 @@ namespace spacer
         return m_num_cols;
     }
 
-    rational spacer_matrix::get(unsigned int i, unsigned int j)
+    const rational& spacer_matrix::get(unsigned int i, unsigned int j)
     {
         SASSERT(i < m_num_rows);
         SASSERT(j < m_num_cols);
@@ -50,7 +50,7 @@ namespace spacer
         return m_matrix[i][j];
     }
 
-    void spacer_matrix::set(unsigned int i, unsigned int j, rational v)
+    void spacer_matrix::set(unsigned int i, unsigned int j, const rational& v)
     {
         SASSERT(i < m_num_rows);
         SASSERT(j < m_num_cols);
diff --git a/src/muz/spacer/spacer_matrix.h b/src/muz/spacer/spacer_matrix.h
index 4fc418f2b..a93a749ae 100644
--- a/src/muz/spacer/spacer_matrix.h
+++ b/src/muz/spacer/spacer_matrix.h
@@ -25,13 +25,13 @@ namespace spacer {
 
     class spacer_matrix {
     public:
-        spacer_matrix(unsigned m, unsigned n); // m rows, n colums
+        spacer_matrix(unsigned m, unsigned n); // m rows, n columns
 
         unsigned num_rows();
         unsigned num_cols();
 
-        rational get(unsigned i, unsigned j);
-        void set(unsigned i, unsigned j, rational v);
+        const rational& get(unsigned i, unsigned j);
+        void set(unsigned i, unsigned j, const rational& v);
 
         unsigned perform_gaussian_elimination();
 
diff --git a/src/muz/spacer/spacer_unsat_core_learner.cpp b/src/muz/spacer/spacer_unsat_core_learner.cpp
index d478b1e8f..bc066d32d 100644
--- a/src/muz/spacer/spacer_unsat_core_learner.cpp
+++ b/src/muz/spacer/spacer_unsat_core_learner.cpp
@@ -301,7 +301,7 @@ public:
     void operator()(quantifier*) {}
 };
 
-void unsat_core_learner::collect_symbols_b(expr_set axioms_b)
+void unsat_core_learner::collect_symbols_b(const expr_set& axioms_b)
 {
     expr_mark visited;
     collect_pure_proc proc(m_symbols_b);
diff --git a/src/muz/spacer/spacer_unsat_core_learner.h b/src/muz/spacer/spacer_unsat_core_learner.h
index a7c9f6aa7..87238b5fd 100644
--- a/src/muz/spacer/spacer_unsat_core_learner.h
+++ b/src/muz/spacer/spacer_unsat_core_learner.h
@@ -82,7 +82,7 @@ namespace spacer {
     private:
         ptr_vector<unsat_core_plugin> m_plugins;
         func_decl_set m_symbols_b; // symbols, which occur in any b-asserted formula
-        void collect_symbols_b(expr_set axioms_b);
+        void collect_symbols_b(const expr_set& axioms_b);
 
         ast_mark m_a_mark;
         ast_mark m_b_mark;
diff --git a/src/nlsat/nlsat_explain.cpp b/src/nlsat/nlsat_explain.cpp
index 3a6c3f067..8d32a0edf 100644
--- a/src/nlsat/nlsat_explain.cpp
+++ b/src/nlsat/nlsat_explain.cpp
@@ -242,7 +242,7 @@ namespace nlsat {
         }
         
         /**
-           \breif Store in ps the polynomials occurring in the given literals.
+           \brief Store in ps the polynomials occurring in the given literals.
         */
         void collect_polys(unsigned num, literal const * ls, polynomial_ref_vector & ps) {
             ps.reset();
@@ -332,7 +332,7 @@ namespace nlsat {
                 if (!is_zero(lc)) {
                     if (sign(lc) != 0)
                         return;
-                    // lc is not the zero polynomial, but it vanished in the current interpretaion.
+                    // lc is not the zero polynomial, but it vanished in the current interpretation.
                     // so we keep searching...
                     add_zero_assumption(lc);
                 }
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index a87042e2b..375ff7e6f 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -1791,7 +1791,7 @@ namespace smt {
         }
     }
 
-    void context::set_conflict(b_justification js, literal not_l) {
+    void context::set_conflict(const b_justification & js, literal not_l) {
         if (!inconsistent()) {
             TRACE("set_conflict", display_literal_verbose(tout, not_l); display(tout, js); );
             m_conflict = js;
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index e50c03c8a..55d8f03f2 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -897,7 +897,7 @@ namespace smt {
         void trace_assign(literal l, b_justification j, bool decision) const;
 
     public:
-        void assign(literal l, b_justification j, bool decision = false) {
+        void assign(literal l, const b_justification & j, bool decision = false) {
             SASSERT(l != false_literal);
             SASSERT(l != null_literal);
             switch (get_assignment(l)) {
@@ -998,9 +998,9 @@ namespace smt {
 
         void assign_quantifier(quantifier * q);
 
-        void set_conflict(b_justification js, literal not_l);
+        void set_conflict(const b_justification & js, literal not_l);
 
-        void set_conflict(b_justification js) {
+        void set_conflict(const b_justification & js) {
             set_conflict(js, null_literal);
         }
 
diff --git a/src/test/rational.cpp b/src/test/rational.cpp
index 7b5e474f0..0618a01fb 100644
--- a/src/test/rational.cpp
+++ b/src/test/rational.cpp
@@ -387,9 +387,9 @@ static void tst9() {
 
 static void tst10(bool use_ints) {
     if (use_ints) 
-        std::cout << "Testing multiplication performace using small ints\n";
+        std::cout << "Testing multiplication performance using small ints\n";
     else
-        std::cout << "Testing multiplication performace using small rationals\n";
+        std::cout << "Testing multiplication performance using small rationals\n";
     vector<rational> vals;
     vector<rational> vals2;
     vector<float>    fvals;
diff --git a/src/util/gparams.h b/src/util/gparams.h
index 894732890..7ddaf0ccb 100644
--- a/src/util/gparams.h
+++ b/src/util/gparams.h
@@ -47,7 +47,7 @@ public:
        set_global_param('pp.decimal', 'true')
        will set the parameter "decimal" in the module "pp" to true.
        
-       An exception is thrown if the the parameter name is unknown, or if the value is incorrect.
+       An exception is thrown if the parameter name is unknown, or if the value is incorrect.
     */
     static void set(char const * name, char const * value);
     static void set(symbol const & name, char const * value);
@@ -57,7 +57,7 @@ public:
        
        If the parameter is not set, then it just returns 'default'.
 
-       An exception is thrown if the the parameter name is unknown.
+       An exception is thrown if the parameter name is unknown.
     */
     static std::string get_value(char const * name);
     static std::string get_value(symbol const & name);
diff --git a/src/util/mpz.h b/src/util/mpz.h
index f04430e17..f4629958f 100644
--- a/src/util/mpz.h
+++ b/src/util/mpz.h
@@ -187,7 +187,7 @@ class mpz_manager {
 
     /**
        \brief Set \c a with the value stored at m_tmp[IDX], and the given sign.
-       \c sz is an overapproximation of the the size of the number stored at \c tmp.
+       \c sz is an overapproximation of the size of the number stored at \c tmp.
     */
     template<int IDX>
     void set(mpz & a, int sign, unsigned sz);