diff --git a/src/ast/csp_decl_plugin.cpp b/src/ast/csp_decl_plugin.cpp
index 21cd798b2..154bbfbc3 100644
--- a/src/ast/csp_decl_plugin.cpp
+++ b/src/ast/csp_decl_plugin.cpp
@@ -104,7 +104,7 @@ func_decl * csp_decl_plugin::mk_func_decl(
         if (domain[2] != m_int_sort) m_manager->raise_exception("3rd argument of add-job-resource expects should be an integer");
         if (domain[3] != m_int_sort) m_manager->raise_exception("4th argument of add-job-resource expects should be an integer");
         if (domain[4] != m_int_sort) m_manager->raise_exception("5th argument of add-job-resource expects should be an integer");
-        if (domain[5] != m_alist_sort) m_manager->raise_exception("6th argument of add-job-resource should be an a list of properties");
+        if (domain[5] != m_alist_sort) m_manager->raise_exception("6th argument of add-job-resource should be a list of properties");
         name = symbol("add-job-resource");
         rng = m_alist_sort;
         break;
@@ -115,7 +115,7 @@ func_decl * csp_decl_plugin::mk_func_decl(
         if (domain[2] != m_int_sort) m_manager->raise_exception("3rd argument of add-resource-available expects should be an integer");
         if (domain[3] != m_int_sort) m_manager->raise_exception("4th argument of add-resource-available expects should be an integer");
         if (domain[4] != m_int_sort) m_manager->raise_exception("5th argument of add-resource-available expects should be an integer");
-        if (domain[5] != m_alist_sort) m_manager->raise_exception("6th argument of add-resource-available should be an a list of properties");
+        if (domain[5] != m_alist_sort) m_manager->raise_exception("6th argument of add-resource-available should be a list of properties");
         name = symbol("add-resource-available");
         rng = m_alist_sort;
         break;
diff --git a/src/muz/rel/dl_relation_manager.h b/src/muz/rel/dl_relation_manager.h
index 5fb468ef5..f81785332 100644
--- a/src/muz/rel/dl_relation_manager.h
+++ b/src/muz/rel/dl_relation_manager.h
@@ -263,7 +263,7 @@ namespace datalog {
         }
 
         /**
-            \brief Return an operation that is a composition of a join an a project operation.
+            \brief Return an operation that is a composition of a join and a project operation.
         */
         relation_join_fn * mk_join_project_fn(const relation_base & t1, const relation_base & t2,
                 unsigned joined_col_cnt, const unsigned * cols1, const unsigned * cols2, 
@@ -433,7 +433,7 @@ namespace datalog {
         }
 
         /**
-            \brief Return an operation that is a composition of a join an a project operation.
+            \brief Return an operation that is a composition of a join and a project operation.
 
             This operation is equivalent to the two operations performed separately, unless functional 
             columns are involved.
diff --git a/src/smt/theory_jobscheduler.cpp b/src/smt/theory_jobscheduler.cpp
index 847ea7f5e..3b218f56d 100644
--- a/src/smt/theory_jobscheduler.cpp
+++ b/src/smt/theory_jobscheduler.cpp
@@ -315,7 +315,7 @@ namespace smt {
 
     /**
      *  For time interval [t0, t1] the end-time can be computed as a function 
-     *  of start time based on reource load availability.
+     *  of start time based on resource load availability.
      * 
      *  r = resource(j) & t1 >= start(j) >= t0 => end(j) = start(j) + ect(j, r, t0) - t0
      */
@@ -672,7 +672,7 @@ namespace smt {
     }
 
     /*
-     * Initialze the state based on the set of jobs and resources added.
+     * Initialize the state based on the set of jobs and resources added.
      * Ensure that the availability slots for each resource is sorted by time.
      *
      * For each resource j: