diff --git a/CMakeLists.txt b/CMakeLists.txt
index 69a0ca123..f20c4fb10 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -409,6 +409,20 @@ list(APPEND Z3_DEPENDENT_LIBS ${CMAKE_THREAD_LIBS_INIT})
 ################################################################################
 include(${CMAKE_SOURCE_DIR}/cmake/compiler_warnings.cmake)
 
+################################################################################
+# If using Ninja, force color output for Clang and gcc.
+################################################################################
+if (UNIX AND CMAKE_GENERATOR STREQUAL "Ninja")
+  if (CMAKE_CXX_COMPILER_ID STREQUAL "Clang")
+    set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fcolor-diagnostics")
+    set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -fcolor-diagnostics")
+  endif()
+  if (CMAKE_CXX_COMPILER_ID STREQUAL "GNU")
+    set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fdiagnostics-color")
+    set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -fdiagnostics-color")
+  endif()
+endif()
+
 ################################################################################
 # Option to control what type of library we build
 ################################################################################
@@ -434,7 +448,7 @@ else()
 endif()
 
 ################################################################################
-# Postion independent code
+# Position independent code
 ################################################################################
 # This is required because code built in the components will end up in a shared
 # library. If not building a shared library ``-fPIC`` isn't needed and would add
diff --git a/scripts/mk_consts_files.py b/scripts/mk_consts_files.py
index d0502c19d..39d4e9439 100755
--- a/scripts/mk_consts_files.py
+++ b/scripts/mk_consts_files.py
@@ -72,7 +72,7 @@ def main(args):
 
     if count == 0:
         logging.info('No files generated. You need to specific an output directory'
-                     ' for the relevant langauge bindings')
+                     ' for the relevant language bindings')
     # TODO: Add support for other bindings
     return 0
 
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 49f6cfbf3..42467cb22 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -989,7 +989,7 @@ namespace z3 {
 
         /**
            \brief sequence and regular expression operations.
-           + is overloaeded as sequence concatenation and regular expression union.
+           + is overloaded as sequence concatenation and regular expression union.
            concat is overloaded to handle sequences and regular expressions
         */
         expr extract(expr const& offset, expr const& length) const { 
diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index cbd6a1bac..b3b24a6d1 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -2515,7 +2515,7 @@ namespace Microsoft.Z3
 
 
         /// <summary>
-        /// Concatentate sequences.
+        /// Concatenate sequences.
         /// </summary>
         public SeqExpr MkConcat(params SeqExpr[] t)
         {
@@ -3597,7 +3597,7 @@ namespace Microsoft.Z3
         }
 
         /// <summary>
-        /// Create a tactic that fails if the goal is not triviall satisfiable (i.e., empty)
+        /// Create a tactic that fails if the goal is not trivially satisfiable (i.e., empty)
         /// or trivially unsatisfiable (i.e., contains `false').
         /// </summary>
         public Tactic FailIfNotDecided()
@@ -4656,7 +4656,7 @@ namespace Microsoft.Z3
         /// Conversion of a floating-point term into a bit-vector.
         /// </summary>
         /// <remarks>
-        /// Produces a term that represents the conversion of the floating-poiunt term t into a
+        /// Produces a term that represents the conversion of the floating-point term t into a
         /// bit-vector term of size sz in 2's complement format (signed when signed==true). If necessary,
         /// the result will be rounded according to rounding mode rm.
         /// </remarks>
@@ -4677,7 +4677,7 @@ namespace Microsoft.Z3
         /// Conversion of a floating-point term into a real-numbered term.
         /// </summary>
         /// <remarks>
-        /// Produces a term that represents the conversion of the floating-poiunt term t into a
+        /// Produces a term that represents the conversion of the floating-point term t into a
         /// real number. Note that this type of conversion will often result in non-linear
         /// constraints over real terms.
         /// </remarks>
@@ -4696,7 +4696,7 @@ namespace Microsoft.Z3
         /// <remarks>
         /// The size of the resulting bit-vector is automatically determined. Note that
         /// IEEE 754-2008 allows multiple different representations of NaN. This conversion
-        /// knows only one NaN and it will always produce the same bit-vector represenatation of
+        /// knows only one NaN and it will always produce the same bit-vector representation of
         /// that NaN.
         /// </remarks>
         /// <param name="t">FloatingPoint term.</param>
diff --git a/src/api/java/Context.java b/src/api/java/Context.java
index ba96209b3..3c5caadee 100644
--- a/src/api/java/Context.java
+++ b/src/api/java/Context.java
@@ -1978,7 +1978,7 @@ public class Context implements AutoCloseable {
     }
     
     /**
-     * Concatentate sequences.
+     * Concatenate sequences.
      */
     public SeqExpr mkConcat(SeqExpr... t)
     {
@@ -2781,7 +2781,7 @@ public class Context implements AutoCloseable {
     }
 
     /**
-     * Create a tactic that fails if the goal is not triviall satisfiable (i.e.,
+     * Create a tactic that fails if the goal is not trivially satisfiable (i.e.,
      * empty) or trivially unsatisfiable (i.e., contains `false').
      **/
     public Tactic failIfNotDecided()
@@ -3769,7 +3769,7 @@ public class Context implements AutoCloseable {
      * @param sz Size of the resulting bit-vector.
      * @param signed Indicates whether the result is a signed or unsigned bit-vector.
      * Remarks:
-     * Produces a term that represents the conversion of the floating-poiunt term t into a
+     * Produces a term that represents the conversion of the floating-point term t into a
      * bit-vector term of size sz in 2's complement format (signed when signed==true). If necessary, 
      * the result will be rounded according to rounding mode rm.        
      * @throws Z3Exception 
@@ -3786,7 +3786,7 @@ public class Context implements AutoCloseable {
      * Conversion of a floating-point term into a real-numbered term.
      * @param t FloatingPoint term
      * Remarks:
-     * Produces a term that represents the conversion of the floating-poiunt term t into a
+     * Produces a term that represents the conversion of the floating-point term t into a
      * real number. Note that this type of conversion will often result in non-linear 
      * constraints over real terms.
      * @throws Z3Exception 
@@ -3802,7 +3802,7 @@ public class Context implements AutoCloseable {
      * Remarks:
      * The size of the resulting bit-vector is automatically determined. Note that 
      * IEEE 754-2008 allows multiple different representations of NaN. This conversion 
-     * knows only one NaN and it will always produce the same bit-vector represenatation of 
+     * knows only one NaN and it will always produce the same bit-vector representation of
      * that NaN. 
      * @throws Z3Exception 
      **/
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 1cfb10179..e68d7280d 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -2428,7 +2428,7 @@ def is_rational_value(a):
     return is_arith(a) and a.is_real() and _is_numeral(a.ctx, a.as_ast())
 
 def is_algebraic_value(a):
-    """Return `True` if `a` is an algerbraic value of sort Real.
+    """Return `True` if `a` is an algebraic value of sort Real.
 
     >>> is_algebraic_value(RealVal("3/5"))
     False
@@ -4437,7 +4437,7 @@ class Datatype:
         """Declare constructor named `name` with the given accessors `args`.
         Each accessor is a pair `(name, sort)`, where `name` is a string and `sort` a Z3 sort or a reference to the datatypes being declared.
 
-        In the followin example `List.declare('cons', ('car', IntSort()), ('cdr', List))`
+        In the following example `List.declare('cons', ('car', IntSort()), ('cdr', List))`
         declares the constructor named `cons` that builds a new List using an integer and a List.
         It also declares the accessors `car` and `cdr`. The accessor `car` extracts the integer of a `cons` cell,
         and `cdr` the list of a `cons` cell. After all constructors were declared, we use the method create() to create
@@ -4457,7 +4457,7 @@ class Datatype:
         return "Datatype(%s, %s)" % (self.name, self.constructors)
 
     def create(self):
-        """Create a Z3 datatype based on the constructors declared using the mehtod `declare()`.
+        """Create a Z3 datatype based on the constructors declared using the method `declare()`.
 
         The function `CreateDatatypes()` must be used to define mutually recursive datatypes.
 
@@ -8874,7 +8874,7 @@ class FPNumRef(FPRef):
     def isSubnormal(self):
         return Z3_fpa_is_numeral_subnormal(self.ctx.ref(), self.as_ast())
 
-    """Indicates whether the numeral is postitive."""
+    """Indicates whether the numeral is positive."""
     def isPositive(self):
         return Z3_fpa_is_numeral_positive(self.ctx.ref(), self.as_ast())
 
@@ -9670,7 +9670,7 @@ def fpToIEEEBV(x, ctx=None):
     The size of the resulting bit-vector is automatically determined.
 
     Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion
-    knows only one NaN and it will always produce the same bit-vector represenatation of
+    knows only one NaN and it will always produce the same bit-vector representation of
     that NaN.
 
     >>> x = FP('x', FPSort(8, 24))
@@ -9845,7 +9845,7 @@ def Empty(s):
     raise Z3Exception("Non-sequence, non-regular expression sort passed to Empty")
 
 def Full(s):
-    """Create the regular expression that accepts the universal langauge
+    """Create the regular expression that accepts the universal language
     >>> e = Full(ReSort(SeqSort(IntSort())))
     >>> print(e)
     re.all
diff --git a/src/api/z3_fpa.h b/src/api/z3_fpa.h
index 358a3c619..7d237c6e7 100644
--- a/src/api/z3_fpa.h
+++ b/src/api/z3_fpa.h
@@ -756,7 +756,7 @@ extern "C" {
     /**
         \brief Conversion of a floating-point term into an unsigned bit-vector.
 
-        Produces a term that represents the conversion of the floating-poiunt term t into a
+        Produces a term that represents the conversion of the floating-point term t into a
         bit-vector term of size sz in unsigned 2's complement format. If necessary, the result
         will be rounded according to rounding mode rm.
 
@@ -772,7 +772,7 @@ extern "C" {
     /**
         \brief Conversion of a floating-point term into a signed bit-vector.
 
-        Produces a term that represents the conversion of the floating-poiunt term t into a
+        Produces a term that represents the conversion of the floating-point term t into a
         bit-vector term of size sz in signed 2's complement format. If necessary, the result
         will be rounded according to rounding mode rm.
 
@@ -788,7 +788,7 @@ extern "C" {
     /**
         \brief Conversion of a floating-point term into a real-numbered term.
 
-        Produces a term that represents the conversion of the floating-poiunt term t into a
+        Produces a term that represents the conversion of the floating-point term t into a
         real number. Note that this type of conversion will often result in non-linear
         constraints over real terms.
 
@@ -1011,7 +1011,7 @@ extern "C" {
         determined.
 
         Note that IEEE 754-2008 allows multiple different representations of NaN. This conversion
-        knows only one NaN and it will always produce the same bit-vector represenatation of
+        knows only one NaN and it will always produce the same bit-vector representation of
         that NaN.
 
         def_API('Z3_mk_fpa_to_ieee_bv', AST, (_in(CONTEXT),_in(AST)))
diff --git a/src/api/z3_interp.h b/src/api/z3_interp.h
index bcee0e22d..2441d4339 100644
--- a/src/api/z3_interp.h
+++ b/src/api/z3_interp.h
@@ -98,7 +98,7 @@ extern "C" {
 
         Interpolant may not necessarily be computable from all
         proofs. To be sure an interpolant can be computed, the proof
-        must be generated by an SMT solver for which interpoaltion is
+        must be generated by an SMT solver for which interpolation is
         supported, and the premises must be expressed using only
         theories and operators for which interpolation is supported.
 
@@ -199,7 +199,7 @@ extern "C" {
        (implies (and c1 ... cn f) v)
 
        where c1 .. cn are the children of v (which must precede v in the file)
-       and f is the formula assiciated to node v. The last formula in the
+       and f is the formula associated to node v. The last formula in the
        file is the root vertex, and is represented by the predicate "false".
 
        A solution to a tree interpolation problem can be thought of as a
diff --git a/src/ast/proofs/proof_checker.cpp b/src/ast/proofs/proof_checker.cpp
index 9ba52a402..bd50e6c2a 100644
--- a/src/ast/proofs/proof_checker.cpp
+++ b/src/ast/proofs/proof_checker.cpp
@@ -922,7 +922,7 @@ void proof_checker::set_false(expr_ref& e, unsigned position, expr_ref& lit) {
     }
 }
 
-bool proof_checker::match_fact(proof* p, expr_ref& fact) {
+bool proof_checker::match_fact(proof const* p, expr_ref& fact) const {
     if (m.is_proof(p) &&
         m.has_fact(p)) {
         fact = m.get_fact(p);
@@ -938,13 +938,13 @@ void proof_checker::add_premise(proof* p) {
     }
 }
 
-bool proof_checker::match_proof(proof* p) {
+bool proof_checker::match_proof(proof const* p) const {
     return 
         m.is_proof(p) &&
         m.get_num_parents(p) == 0;
 }
 
-bool proof_checker::match_proof(proof* p, proof_ref& p0) {
+bool proof_checker::match_proof(proof const* p, proof_ref& p0) const {
     if (m.is_proof(p) &&
         m.get_num_parents(p) == 1) {
         p0 = m.get_parent(p, 0);
@@ -953,7 +953,7 @@ bool proof_checker::match_proof(proof* p, proof_ref& p0) {
     return false;
 }
  
-bool proof_checker::match_proof(proof* p, proof_ref& p0, proof_ref& p1) {
+bool proof_checker::match_proof(proof const* p, proof_ref& p0, proof_ref& p1) const {
     if (m.is_proof(p) &&
         m.get_num_parents(p) == 2) {
         p0 = m.get_parent(p, 0);
@@ -963,7 +963,7 @@ bool proof_checker::match_proof(proof* p, proof_ref& p0, proof_ref& p1) {
     return false;
 }
 
-bool proof_checker::match_proof(proof* p, proof_ref_vector& parents) {
+bool proof_checker::match_proof(proof const* p, proof_ref_vector& parents) const {
     if (m.is_proof(p)) {
         for (unsigned i = 0; i < m.get_num_parents(p); ++i) {
             parents.push_back(m.get_parent(p, i));
@@ -974,7 +974,7 @@ bool proof_checker::match_proof(proof* p, proof_ref_vector& parents) {
 }
 
 
-bool proof_checker::match_binary(expr* e, func_decl_ref& d, expr_ref& t1, expr_ref& t2) {
+bool proof_checker::match_binary(expr const* e, func_decl_ref& d, expr_ref& t1, expr_ref& t2) const {
     if (e->get_kind() == AST_APP &&
         to_app(e)->get_num_args() == 2) {
         d = to_app(e)->get_decl();
@@ -986,7 +986,7 @@ bool proof_checker::match_binary(expr* e, func_decl_ref& d, expr_ref& t1, expr_r
 }
 
 
-bool proof_checker::match_app(expr* e, func_decl_ref& d, expr_ref_vector& terms) {
+bool proof_checker::match_app(expr const* e, func_decl_ref& d, expr_ref_vector& terms) const {
     if (e->get_kind() == AST_APP) {
         d = to_app(e)->get_decl();
         for (unsigned i = 0; i < to_app(e)->get_num_args(); ++i) {
@@ -997,9 +997,9 @@ bool proof_checker::match_app(expr* e, func_decl_ref& d, expr_ref_vector& terms)
     return false;
 }
 
-bool proof_checker::match_quantifier(expr* e, bool& is_univ, sort_ref_vector& sorts, expr_ref& body) {
+bool proof_checker::match_quantifier(expr const* e, bool& is_univ, sort_ref_vector& sorts, expr_ref& body) const {
     if (is_quantifier(e)) {
-        quantifier* q = to_quantifier(e);
+        quantifier const* q = to_quantifier(e);
         is_univ = q->is_forall();
         body = q->get_expr();
         for (unsigned i = 0; i < q->get_num_decls(); ++i) {
@@ -1010,7 +1010,7 @@ bool proof_checker::match_quantifier(expr* e, bool& is_univ, sort_ref_vector& so
     return false;
 }
 
-bool proof_checker::match_op(expr* e, decl_kind k, expr_ref& t1, expr_ref& t2) {
+bool proof_checker::match_op(expr const* e, decl_kind k, expr_ref& t1, expr_ref& t2) const {
     if (e->get_kind() == AST_APP &&
         to_app(e)->get_family_id() == m.get_basic_family_id() &&
         to_app(e)->get_decl_kind() == k &&
@@ -1022,7 +1022,7 @@ bool proof_checker::match_op(expr* e, decl_kind k, expr_ref& t1, expr_ref& t2) {
     return false;
 }
 
-bool proof_checker::match_op(expr* e, decl_kind k, expr_ref_vector& terms) {
+bool proof_checker::match_op(expr const* e, decl_kind k, expr_ref_vector& terms) const {
     if (e->get_kind() == AST_APP &&
         to_app(e)->get_family_id() == m.get_basic_family_id() &&
         to_app(e)->get_decl_kind() == k) {
@@ -1035,7 +1035,7 @@ bool proof_checker::match_op(expr* e, decl_kind k, expr_ref_vector& terms) {
 }
 
 
-bool proof_checker::match_op(expr* e, decl_kind k, expr_ref& t) {
+bool proof_checker::match_op(expr const* e, decl_kind k, expr_ref& t) const {
     if (e->get_kind() == AST_APP &&
         to_app(e)->get_family_id() == m.get_basic_family_id() &&
         to_app(e)->get_decl_kind() == k &&
@@ -1046,39 +1046,39 @@ bool proof_checker::match_op(expr* e, decl_kind k, expr_ref& t) {
     return false;
 }
 
-bool proof_checker::match_not(expr* e, expr_ref& t) {
+bool proof_checker::match_not(expr const* e, expr_ref& t) const {
     return match_op(e, OP_NOT, t);
 }
 
-bool proof_checker::match_or(expr* e, expr_ref_vector& terms) {
+bool proof_checker::match_or(expr const* e, expr_ref_vector& terms) const {
     return match_op(e, OP_OR, terms);
 }
 
-bool proof_checker::match_and(expr* e, expr_ref_vector& terms) {
+bool proof_checker::match_and(expr const* e, expr_ref_vector& terms) const {
     return match_op(e, OP_AND, terms);
 }
 
-bool proof_checker::match_iff(expr* e, expr_ref& t1, expr_ref& t2) {
+bool proof_checker::match_iff(expr const* e, expr_ref& t1, expr_ref& t2) const {
     return match_op(e, OP_IFF, t1, t2);
 }
 
-bool proof_checker::match_equiv(expr* e, expr_ref& t1, expr_ref& t2) {
+bool proof_checker::match_equiv(expr const* e, expr_ref& t1, expr_ref& t2) const {
     return match_oeq(e, t1, t2) || match_eq(e, t1, t2);
 }
 
-bool proof_checker::match_implies(expr* e, expr_ref& t1, expr_ref& t2) {
+bool proof_checker::match_implies(expr const* e, expr_ref& t1, expr_ref& t2) const {
     return match_op(e, OP_IMPLIES, t1, t2);
 }
 
-bool proof_checker::match_eq(expr* e, expr_ref& t1, expr_ref& t2) {
+bool proof_checker::match_eq(expr const* e, expr_ref& t1, expr_ref& t2) const {
     return match_op(e, OP_EQ, t1, t2) || match_iff(e, t1, t2);
 }
 
-bool proof_checker::match_oeq(expr* e, expr_ref& t1, expr_ref& t2) {
+bool proof_checker::match_oeq(expr const* e, expr_ref& t1, expr_ref& t2) const {
     return match_op(e, OP_OEQ, t1, t2);
 }
 
-bool proof_checker::match_negated(expr* a, expr* b) {
+bool proof_checker::match_negated(expr const* a, expr* b) const {
     expr_ref t(m);
     return 
         (match_not(a, t) && t.get() == b) ||
@@ -1186,14 +1186,14 @@ void proof_checker::get_hypotheses(proof* p, expr_ref_vector& ante) {
 
 }
 
-bool proof_checker::match_nil(expr* e) const {
+bool proof_checker::match_nil(expr const* e) const {
     return 
         is_app(e) &&
         to_app(e)->get_family_id() == m_hyp_fid &&
         to_app(e)->get_decl_kind() == OP_NIL;
 }
 
-bool proof_checker::match_cons(expr* e, expr_ref& a, expr_ref& b) const {
+bool proof_checker::match_cons(expr const* e, expr_ref& a, expr_ref& b) const {
     if (is_app(e) &&
         to_app(e)->get_family_id() == m_hyp_fid &&
         to_app(e)->get_decl_kind() == OP_CONS) {
@@ -1205,7 +1205,7 @@ bool proof_checker::match_cons(expr* e, expr_ref& a, expr_ref& b) const {
 }
 
 
-bool proof_checker::match_atom(expr* e, expr_ref& a) const {
+bool proof_checker::match_atom(expr const* e, expr_ref& a) const {
     if (is_app(e) &&
         to_app(e)->get_family_id() == m_hyp_fid &&
         to_app(e)->get_decl_kind() == OP_ATOM) {
@@ -1227,7 +1227,7 @@ expr* proof_checker::mk_nil() {
     return m_nil.get();
 }
 
-bool proof_checker::is_hypothesis(proof* p) const {
+bool proof_checker::is_hypothesis(proof const* p) const {
     return 
         m.is_proof(p) &&
         p->get_decl_kind() == PR_HYPOTHESIS;
@@ -1253,7 +1253,7 @@ expr* proof_checker::mk_hyp(unsigned num_hyps, expr * const * hyps) {
     } 
 }
 
-void proof_checker::dump_proof(proof * pr) {
+void proof_checker::dump_proof(proof const* pr) {
     if (!m_dump_lemmas)
         return;
     SASSERT(m.has_fact(pr));
diff --git a/src/ast/proofs/proof_checker.h b/src/ast/proofs/proof_checker.h
index ccb815c61..ac0e31dbd 100644
--- a/src/ast/proofs/proof_checker.h
+++ b/src/ast/proofs/proof_checker.h
@@ -77,39 +77,39 @@ private:
     bool check1_spc(proof* p, expr_ref_vector& side_conditions);
     bool check_arith_proof(proof* p);
     bool check_arith_literal(bool is_pos, app* lit, rational const& coeff, expr_ref& sum, bool& is_strict);
-    bool match_fact(proof* p, expr_ref& fact);
+    bool match_fact(proof const* p, expr_ref& fact) const;
     void add_premise(proof* p);
-    bool match_proof(proof* p);
-    bool match_proof(proof* p, proof_ref& p0);
-    bool match_proof(proof* p, proof_ref& p0, proof_ref& p1);
-    bool match_proof(proof* p, proof_ref_vector& parents);
-    bool match_binary(expr* e, func_decl_ref& d, expr_ref& t1, expr_ref& t2);
-    bool match_op(expr* e, decl_kind k, expr_ref& t1, expr_ref& t2);
-    bool match_op(expr* e, decl_kind k, expr_ref& t);
-    bool match_op(expr* e, decl_kind k, expr_ref_vector& terms);
-    bool match_iff(expr* e, expr_ref& t1, expr_ref& t2);
-    bool match_implies(expr* e, expr_ref& t1, expr_ref& t2);
-    bool match_eq(expr* e, expr_ref& t1, expr_ref& t2);
-    bool match_oeq(expr* e, expr_ref& t1, expr_ref& t2);
-    bool match_not(expr* e, expr_ref& t);
-    bool match_or(expr* e, expr_ref_vector& terms);
-    bool match_and(expr* e, expr_ref_vector& terms);
-    bool match_app(expr* e, func_decl_ref& d, expr_ref_vector& terms);
-    bool match_quantifier(expr*, bool& is_univ, sort_ref_vector&, expr_ref& body);
-    bool match_negated(expr* a, expr* b);
-    bool match_equiv(expr* a, expr_ref& t1, expr_ref& t2);
+    bool match_proof(proof const* p) const;
+    bool match_proof(proof const* p, proof_ref& p0) const;
+    bool match_proof(proof const* p, proof_ref& p0, proof_ref& p1) const;
+    bool match_proof(proof const* p, proof_ref_vector& parents) const;
+    bool match_binary(expr const* e, func_decl_ref& d, expr_ref& t1, expr_ref& t2) const;
+    bool match_op(expr const* e, decl_kind k, expr_ref& t1, expr_ref& t2) const;
+    bool match_op(expr const* e, decl_kind k, expr_ref& t) const;
+    bool match_op(expr const* e, decl_kind k, expr_ref_vector& terms) const;
+    bool match_iff(expr const* e, expr_ref& t1, expr_ref& t2) const;
+    bool match_implies(expr const* e, expr_ref& t1, expr_ref& t2) const;
+    bool match_eq(expr const* e, expr_ref& t1, expr_ref& t2) const;
+    bool match_oeq(expr const* e, expr_ref& t1, expr_ref& t2) const;
+    bool match_not(expr const* e, expr_ref& t) const;
+    bool match_or(expr const* e, expr_ref_vector& terms) const;
+    bool match_and(expr const* e, expr_ref_vector& terms) const;
+    bool match_app(expr const* e, func_decl_ref& d, expr_ref_vector& terms) const;
+    bool match_quantifier(expr const*, bool& is_univ, sort_ref_vector&, expr_ref& body) const;
+    bool match_negated(expr const* a, expr* b) const;
+    bool match_equiv(expr const* a, expr_ref& t1, expr_ref& t2) const;
     void get_ors(expr* e, expr_ref_vector& ors);
     void get_hypotheses(proof* p, expr_ref_vector& ante);
 
-    bool match_nil(expr* e) const;
-    bool match_cons(expr* e, expr_ref& a, expr_ref& b) const;
-    bool match_atom(expr* e, expr_ref& a) const;
+    bool match_nil(expr const* e) const;
+    bool match_cons(expr const* e, expr_ref& a, expr_ref& b) const;
+    bool match_atom(expr const* e, expr_ref& a) const;
     expr* mk_nil();
     expr* mk_cons(expr* a, expr* b);
     expr* mk_atom(expr* e);
-    bool is_hypothesis(proof* p) const;
+    bool is_hypothesis(proof const* p) const;
     expr* mk_hyp(unsigned num_hyps, expr * const * hyps);
-    void dump_proof(proof * pr);
+    void dump_proof(proof const* pr);
     void dump_proof(unsigned num_antecedents, expr * const * antecedents, expr * consequent);
 
     void set_false(expr_ref& e, unsigned idx, expr_ref& lit);
diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h
index 658fb2e05..878f4ef4c 100644
--- a/src/ast/rewriter/rewriter_def.h
+++ b/src/ast/rewriter/rewriter_def.h
@@ -358,7 +358,7 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
                 if (ProofGen) {
                     NOT_IMPLEMENTED_YET();
                     // We do not support the use of bindings in proof generation mode.
-                    // Thus we have to apply the subsitution here, and
+                    // Thus we have to apply the substitution here, and
                     // beta_reducer subst(m());
                     // subst.set_bindings(new_num_args, new_args);
                     // expr_ref r2(m());
diff --git a/src/interp/iz3checker.cpp b/src/interp/iz3checker.cpp
index cfea511ad..511342819 100644
--- a/src/interp/iz3checker.cpp
+++ b/src/interp/iz3checker.cpp
@@ -43,7 +43,7 @@ struct iz3checker : iz3base {
     /* HACK: for tree interpolants, we assume that uninterpreted functions
        are global. This is because in the current state of the tree interpolation
        code, symbols that appear in sibling sub-trees have to be global, and
-       we have no way to eliminate such function symbols. When tree interpoaltion is
+       we have no way to eliminate such function symbols. When tree interpolation is
        fixed, we can tree function symbols the same as constant symbols. */
 
     bool is_tree;
diff --git a/src/muz/base/fixedpoint_params.pyg b/src/muz/base/fixedpoint_params.pyg
index 0c2f03460..753a45e06 100644
--- a/src/muz/base/fixedpoint_params.pyg
+++ b/src/muz/base/fixedpoint_params.pyg
@@ -33,7 +33,7 @@ def_module_params('fixedpoint',
                            "updated relation was modified or not"),
                           ('datalog.compile_with_widening', BOOL, False, 
                            "widening will be used to compile recursive rules"),
-                          ('datalog.default_table_checked', BOOL, False, "if true, the detault " +
+                          ('datalog.default_table_checked', BOOL, False, "if true, the default " +
                            'table will be default_table inside a wrapper that checks that its results ' +
                            'are the same as of default_table_checker table'),
                           ('datalog.default_table_checker', SYMBOL, 'null', "see default_table_checked"),
@@ -59,7 +59,7 @@ def_module_params('fixedpoint',
                           ('duality.full_expand', BOOL, False, 'Fully expand derivation trees'),
                           ('duality.no_conj', BOOL, False, 'No forced covering (conjectures)'),
                           ('duality.feasible_edges', BOOL, True, 
-                           'Don\'t expand definitley infeasible edges'),
+                           'Don\'t expand definitely infeasible edges'),
                           ('duality.use_underapprox', BOOL, False, 'Use underapproximations'),
                           ('duality.stratified_inlining', BOOL, False, 'Use stratified inlining'),
                           ('duality.recursion_bound', UINT, UINT_MAX, 
@@ -130,7 +130,7 @@ def_module_params('fixedpoint',
                           ('xform.magic', BOOL, False, 
                            "perform symbolic magic set transformation"),
                           ('xform.scale', BOOL, False, 
-                           "add scaling variable to linear real arithemtic clauses"),
+                           "add scaling variable to linear real arithmetic clauses"),
                           ('xform.inline_linear', BOOL, True, "try linear inlining method"),
                           ('xform.inline_eager', BOOL, True, "try eager inlining of rules"),
                           ('xform.inline_linear_branch', BOOL, False, 
@@ -176,7 +176,7 @@ def_module_params('fixedpoint',
                           ('spacer.elim_aux', BOOL, True, "Eliminate auxiliary variables in reachability facts"),
                           ('spacer.reach_as_init', BOOL, True, "Extend initial rules with computed reachability facts"),
                           ('spacer.blast_term_ite', BOOL, True, "Expand non-Boolean ite-terms"),
-                          ('spacer.nondet_tie_break', BOOL, False, "Break ties in obligation queue non-deterministicly"),
+                          ('spacer.nondet_tie_break', BOOL, False, "Break ties in obligation queue non-deterministically"),
                           ('spacer.reach_dnf', BOOL, True, "Restrict reachability facts to DNF"),
                           ('bmc.linear_unrolling_depth', UINT, UINT_MAX, "Maximal level to explore"),
                           ('spacer.split_farkas_literals', BOOL, False, "Split Farkas literals"),
diff --git a/src/muz/transforms/dl_mk_array_instantiation.h b/src/muz/transforms/dl_mk_array_instantiation.h
index cd5715a4f..b2e80ab84 100644
--- a/src/muz/transforms/dl_mk_array_instantiation.h
+++ b/src/muz/transforms/dl_mk_array_instantiation.h
@@ -26,7 +26,7 @@ Implementation:
 
     1) Dealing with multiple quantifiers -> The options fixedpoint.xform.instantiate_arrays.nb_quantifier gives the number of quantifiers per array.
 
-    2) Inforcing the instantiation -> We suggest an option (enforce_instantiation) to enforce this abstraction. This transforms
+    2) Enforcing the instantiation -> We suggest an option (enforce_instantiation) to enforce this abstraction. This transforms
        P(a) into P(i, a[i]). This enforces the solver to limit the space search at the cost of imprecise results. This option
        corresponds to fixedpoint.xform.instantiate_arrays.enforce
 
diff --git a/src/muz/transforms/dl_mk_interp_tail_simplifier.h b/src/muz/transforms/dl_mk_interp_tail_simplifier.h
index 713827588..0d4c65d11 100644
--- a/src/muz/transforms/dl_mk_interp_tail_simplifier.h
+++ b/src/muz/transforms/dl_mk_interp_tail_simplifier.h
@@ -53,7 +53,7 @@ namespace datalog {
             */
             void reset(rule * r);
 
-            /** Reset subtitution and unify tail tgt_idx of the target rule and the head of the src rule */
+            /** Reset substitution and unify tail tgt_idx of the target rule and the head of the src rule */
             bool unify(expr * e1, expr * e2);
 
             void get_result(rule_ref & res);
diff --git a/src/muz/transforms/dl_mk_rule_inliner.h b/src/muz/transforms/dl_mk_rule_inliner.h
index 27b6dd418..9146343fa 100644
--- a/src/muz/transforms/dl_mk_rule_inliner.h
+++ b/src/muz/transforms/dl_mk_rule_inliner.h
@@ -45,7 +45,7 @@ namespace datalog {
             : m(ctx.get_manager()), m_rm(ctx.get_rule_manager()), m_context(ctx), 
             m_interp_simplifier(ctx), m_subst(m), m_unif(m), m_ready(false), m_normalize(true) {}
             
-        /** Reset subtitution and unify tail tgt_idx of the target rule and the head of the src rule */
+        /** Reset substitution and unify tail tgt_idx of the target rule and the head of the src rule */
         bool unify_rules(rule const& tgt, unsigned tgt_idx, rule const& src);
 
         /**
diff --git a/src/muz/transforms/dl_mk_scale.h b/src/muz/transforms/dl_mk_scale.h
index c171a1d06..94090ec93 100644
--- a/src/muz/transforms/dl_mk_scale.h
+++ b/src/muz/transforms/dl_mk_scale.h
@@ -7,7 +7,7 @@ Module Name:
 
 Abstract:
 
-    Add scale factor to linear (Real) arithemetic Horn clauses.
+    Add scale factor to linear (Real) arithmetic Horn clauses.
     The transformation replaces occurrences of isolated constants by
     a scale multiplied to each constant. 
 
diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 8567c6b30..9dfd0475b 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -641,7 +641,6 @@ namespace smt {
     }
 
     app * theory_str::mk_indexof(expr * haystack, expr * needle) {
-        // TODO check meaning of the third argument here
         app * indexof = u.str.mk_index(haystack, needle, mk_int(0));
         m_trail.push_back(indexof);
         // immediately force internalization so that axiom setup does not fail
@@ -844,14 +843,7 @@ namespace smt {
                     instantiate_axiom_Contains(e);
                 } else if (u.str.is_index(a)) {
                     instantiate_axiom_Indexof(e);
-                    /* TODO NEXT: Indexof2/Lastindexof rewrite?
-                       } else if (is_Indexof2(e)) {
-                       instantiate_axiom_Indexof2(e);
-                       } else if (is_LastIndexof(e)) {
-                       instantiate_axiom_LastIndexof(e);
-                    */
                 } else if (u.str.is_extract(a)) {
-                    // TODO check semantics of substr vs. extract
                     instantiate_axiom_Substr(e);
                 } else if (u.str.is_replace(a)) {
                     instantiate_axiom_Replace(e);
@@ -1232,27 +1224,37 @@ namespace smt {
         context & ctx = get_context();
         ast_manager & m = get_manager();
 
-        app * expr = e->get_owner();
-        if (axiomatized_terms.contains(expr)) {
-            TRACE("str", tout << "already set up Indexof axiom for " << mk_pp(expr, m) << std::endl;);
+        app * ex = e->get_owner();
+        if (axiomatized_terms.contains(ex)) {
+            TRACE("str", tout << "already set up str.indexof axiom for " << mk_pp(ex, m) << std::endl;);
             return;
         }
-        axiomatized_terms.insert(expr);
+        SASSERT(ex->get_num_args() == 3);
+        // if the third argument is exactly the integer 0, we can use this "simple" indexof;
+        // otherwise, we call the "extended" version
+        expr * startingPosition = ex->get_arg(2);
+        rational startingInteger;
+        if (!m_autil.is_numeral(startingPosition, startingInteger) || !startingInteger.is_zero()) {
+            // "extended" indexof term with prefix
+            instantiate_axiom_Indexof_extended(e);
+            return;
+        }
+        axiomatized_terms.insert(ex);
 
-        TRACE("str", tout << "instantiate Indexof axiom for " << mk_pp(expr, m) << std::endl;);
+        TRACE("str", tout << "instantiate str.indexof axiom for " << mk_pp(ex, m) << std::endl;);
 
         expr_ref x1(mk_str_var("x1"), m);
         expr_ref x2(mk_str_var("x2"), m);
         expr_ref indexAst(mk_int_var("index"), m);
 
-        expr_ref condAst(mk_contains(expr->get_arg(0), expr->get_arg(1)), m);
+        expr_ref condAst(mk_contains(ex->get_arg(0), ex->get_arg(1)), m);
         SASSERT(condAst);
 
         // -----------------------
         // true branch
         expr_ref_vector thenItems(m);
         //  args[0] = x1 . args[1] . x2
-        thenItems.push_back(ctx.mk_eq_atom(expr->get_arg(0), mk_concat(x1, mk_concat(expr->get_arg(1), x2))));
+        thenItems.push_back(ctx.mk_eq_atom(ex->get_arg(0), mk_concat(x1, mk_concat(ex->get_arg(1), x2))));
         //  indexAst = |x1|
         thenItems.push_back(ctx.mk_eq_atom(indexAst, mk_strlen(x1)));
         //     args[0]  = x3 . x4
@@ -1260,11 +1262,11 @@ namespace smt {
         //  /\ ! contains(x3, args[1])
         expr_ref x3(mk_str_var("x3"), m);
         expr_ref x4(mk_str_var("x4"), m);
-        expr_ref tmpLen(m_autil.mk_add(indexAst, mk_strlen(expr->get_arg(1)), mk_int(-1)), m);
+        expr_ref tmpLen(m_autil.mk_add(indexAst, mk_strlen(ex->get_arg(1)), mk_int(-1)), m);
         SASSERT(tmpLen);
-        thenItems.push_back(ctx.mk_eq_atom(expr->get_arg(0), mk_concat(x3, x4)));
+        thenItems.push_back(ctx.mk_eq_atom(ex->get_arg(0), mk_concat(x3, x4)));
         thenItems.push_back(ctx.mk_eq_atom(mk_strlen(x3), tmpLen));
-        thenItems.push_back(mk_not(m, mk_contains(x3, expr->get_arg(1))));
+        thenItems.push_back(mk_not(m, mk_contains(x3, ex->get_arg(1))));
         expr_ref thenBranch(m.mk_and(thenItems.size(), thenItems.c_ptr()), m);
         SASSERT(thenBranch);
 
@@ -1276,26 +1278,42 @@ namespace smt {
         expr_ref breakdownAssert(m.mk_ite(condAst, thenBranch, elseBranch), m);
         SASSERT(breakdownAssert);
 
-        expr_ref reduceToIndex(ctx.mk_eq_atom(expr, indexAst), m);
+        expr_ref reduceToIndex(ctx.mk_eq_atom(ex, indexAst), m);
         SASSERT(reduceToIndex);
 
         expr_ref finalAxiom(m.mk_and(breakdownAssert, reduceToIndex), m);
         SASSERT(finalAxiom);
         assert_axiom(finalAxiom);
+
+        {
+            // heuristic: integrate with str.contains information
+            // (but don't introduce it if it isn't already in the instance)
+            expr_ref haystack(ex->get_arg(0), m), needle(ex->get_arg(1), m), startIdx(ex->get_arg(2), m);
+            expr_ref zeroAst(mk_int(0), m);
+            // (H contains N) <==> (H indexof N, i) >= 0
+            expr_ref premise(u.str.mk_contains(haystack, needle), m);
+            ctx.internalize(premise, false);
+            expr_ref conclusion(m_autil.mk_ge(ex, zeroAst), m);
+            expr_ref containsAxiom(ctx.mk_eq_atom(premise, conclusion), m);
+            SASSERT(containsAxiom);
+            // we can't assert this during init_search as it breaks an invariant if the instance becomes inconsistent
+            m_delayed_axiom_setup_terms.push_back(containsAxiom);
+        }
     }
 
-    void theory_str::instantiate_axiom_Indexof2(enode * e) {
+    void theory_str::instantiate_axiom_Indexof_extended(enode * e) {
         context & ctx = get_context();
         ast_manager & m = get_manager();
 
         app * expr = e->get_owner();
         if (axiomatized_terms.contains(expr)) {
-            TRACE("str", tout << "already set up Indexof2 axiom for " << mk_pp(expr, m) << std::endl;);
+            TRACE("str", tout << "already set up extended str.indexof axiom for " << mk_pp(expr, m) << std::endl;);
             return;
         }
+        SASSERT(expr->get_num_args() == 3);
         axiomatized_terms.insert(expr);
 
-        TRACE("str", tout << "instantiate Indexof2 axiom for " << mk_pp(expr, m) << std::endl;);
+        TRACE("str", tout << "instantiate extended str.indexof axiom for " << mk_pp(expr, m) << std::endl;);
 
         // -------------------------------------------------------------------------------
         //   if (arg[2] >= length(arg[0]))                          // ite2
@@ -1327,7 +1345,7 @@ namespace smt {
         ite2ElseItems.push_back(ctx.mk_eq_atom(indexAst, mk_indexof(suffix, expr->get_arg(1))));
         ite2ElseItems.push_back(ctx.mk_eq_atom(expr->get_arg(2), prefixLen));
         ite2ElseItems.push_back(ite3);
-        expr_ref ite2Else(m.mk_and(ite2ElseItems.size(), ite2ElseItems.c_ptr()), m);
+        expr_ref ite2Else(mk_and(ite2ElseItems), m);
         SASSERT(ite2Else);
 
         expr_ref ite2(m.mk_ite(
@@ -1350,6 +1368,20 @@ namespace smt {
         expr_ref reduceTerm(ctx.mk_eq_atom(expr, resAst), m);
         SASSERT(reduceTerm);
         assert_axiom(reduceTerm);
+
+        {
+            // heuristic: integrate with str.contains information
+            // (but don't introduce it if it isn't already in the instance)
+            expr_ref haystack(expr->get_arg(0), m), needle(expr->get_arg(1), m), startIdx(expr->get_arg(2), m);
+            // (H contains N) <==> (H indexof N, i) >= 0
+            expr_ref premise(u.str.mk_contains(haystack, needle), m);
+            ctx.internalize(premise, false);
+            expr_ref conclusion(m_autil.mk_ge(expr, zeroAst), m);
+            expr_ref containsAxiom(ctx.mk_eq_atom(premise, conclusion), m);
+            SASSERT(containsAxiom);
+            // we can't assert this during init_search as it breaks an invariant if the instance becomes inconsistent
+            m_delayed_axiom_setup_terms.push_back(containsAxiom);
+        }
     }
 
     void theory_str::instantiate_axiom_LastIndexof(enode * e) {
@@ -8731,8 +8763,8 @@ namespace smt {
         context & ctx = get_context();
         ast_manager & m = get_manager();
 
-        expr_ref_vector assignments(m);
-        ctx.get_assignments(assignments);
+        //expr_ref_vector assignments(m);
+        //ctx.get_assignments(assignments);
 
         if (opt_VerifyFinalCheckProgress) {
             finalCheckProgressIndicator = false;
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index 3b71a2282..9288bac7c 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -447,7 +447,7 @@ protected:
     void instantiate_axiom_suffixof(enode * e);
     void instantiate_axiom_Contains(enode * e);
     void instantiate_axiom_Indexof(enode * e);
-    void instantiate_axiom_Indexof2(enode * e);
+    void instantiate_axiom_Indexof_extended(enode * e);
     void instantiate_axiom_LastIndexof(enode * e);
     void instantiate_axiom_Substr(enode * e);
     void instantiate_axiom_Replace(enode * e);
diff --git a/src/tactic/aig/aig.cpp b/src/tactic/aig/aig.cpp
index 40c68f72a..6afac32b8 100644
--- a/src/tactic/aig/aig.cpp
+++ b/src/tactic/aig/aig.cpp
@@ -267,7 +267,7 @@ struct aig_manager::imp {
             }
             if  (b == r) {
                 if (sign1) {
-                    // subsitution
+                    // substitution
                     // not (a and b) and r --> (not a) and r   IF b == r
                     l = a;
                     l.invert();
diff --git a/src/tactic/tactic_exception.h b/src/tactic/tactic_exception.h
index 177524726..bdf2636a9 100644
--- a/src/tactic/tactic_exception.h
+++ b/src/tactic/tactic_exception.h
@@ -7,7 +7,7 @@ Module Name:
 
 Abstract:
 
-    Tactic expection object.
+    Tactic exception object.
 
 Author:
 
diff --git a/src/tactic/tactical.h b/src/tactic/tactical.h
index 169566f39..9ec2f901f 100644
--- a/src/tactic/tactical.h
+++ b/src/tactic/tactical.h
@@ -47,7 +47,7 @@ tactic * or_else(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5
 
 tactic * repeat(tactic * t, unsigned max = UINT_MAX); 
 /**
-   \brief Fails if \c t produeces more than \c threshold subgoals.
+   \brief Fails if \c t produces more than \c threshold subgoals.
    Otherwise, it behaves like \c t.
 */
 tactic * fail_if_branching(tactic * t, unsigned threshold = 1);