diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index a941f8e86..cdaae332b 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -475,7 +475,7 @@ namespace Microsoft.Z3
         /// Update a datatype field at expression t with value v.
         /// The function performs a record update at t. The field
         /// that is passed in as argument is updated with value v,
-        /// the remainig fields of t are unchanged.
+        /// the remaining fields of t are unchanged.
             /// </summary>
         public Expr MkUpdateField(FuncDecl field, Expr t, Expr v)
         {
diff --git a/src/api/dotnet/Optimize.cs b/src/api/dotnet/Optimize.cs
index 4713f414a..9a7bd3bd1 100644
--- a/src/api/dotnet/Optimize.cs
+++ b/src/api/dotnet/Optimize.cs
@@ -25,7 +25,7 @@ using System.Linq;
 namespace Microsoft.Z3
 {
     /// <summary>
-    /// Object for managing optimizization context
+    /// Object for managing optimization context
     /// </summary>
     public class Optimize : Z3Object
     {
diff --git a/src/api/dotnet/dotnet35/Readme.NET35 b/src/api/dotnet/dotnet35/Readme.NET35
index f8c2958ee..75210f8b6 100644
--- a/src/api/dotnet/dotnet35/Readme.NET35
+++ b/src/api/dotnet/dotnet35/Readme.NET35
@@ -4,7 +4,7 @@ instructions are as follows:
 
 In the project properties of Microsoft.Z3.csproj:
 - Under 'Application': Change Target framework to .NET Framework 3.5
-- Under 'Build': Add FRAMEWORK_LT_4 to the condidional compilation symbols
+- Under 'Build': Add FRAMEWORK_LT_4 to the conditional compilation symbols
 - Remove the reference to System.Numerics
 - Install the NuGet Package "Microsoft Code Contracts for Net3.5":
   In the Package Manager Console enter Install-Package Code.Contract
diff --git a/src/qe/qe.h b/src/qe/qe.h
index 1027f0b61..1eb7b7e4a 100644
--- a/src/qe/qe.h
+++ b/src/qe/qe.h
@@ -253,7 +253,7 @@ namespace qe {
     /**
        \brief Guarded definitions.
 
-       A realizer to a an existential quantified formula is a disjunction
+       A realizer to an existential quantified formula is a disjunction
        together with a substitution from the existentially quantified variables
        to terms such that:
        1. The original formula (exists (vars) fml) is equivalent to the disjunction of guards.
diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp
index 1be76728c..6ef94e880 100644
--- a/src/util/memory_manager.cpp
+++ b/src/util/memory_manager.cpp
@@ -18,7 +18,7 @@ Copyright (c) 2015 Microsoft Corporation
 //      ADD_INITIALIZER('rational::initialize();')
 //      ADD_FINALIZER('rational::finalize();')
 // Thus, any executable or shared object (DLL) that depends on rational.h
-// will have an automalically generated file mem_initializer.cpp containing
+// will have an automatically generated file mem_initializer.cpp containing
 //    mem_initialize() 
 //    mem_finalize()
 // and these functions will include the statements: