From d1592c6abf7fa3c9067e47eb40e6fa32d7dc0817 Mon Sep 17 00:00:00 2001
From: Alexander Traud <pabstraud@compuserve.com>
Date: Fri, 29 Oct 2021 15:34:28 +0200
Subject: [PATCH] fix misspelled \brief for doxygen (#5632)

---
 src/model/array_factory.cpp | 2 +-
 src/muz/spacer/spacer_mbc.h | 2 +-
 src/smt/seq_offset_eq.h     | 2 +-
 src/smt/smt_relevancy.h     | 4 ++--
 4 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/model/array_factory.cpp b/src/model/array_factory.cpp
index 6fab80661cf..d3ec56d3906 100644
--- a/src/model/array_factory.cpp
+++ b/src/model/array_factory.cpp
@@ -38,7 +38,7 @@ array_factory::array_factory(ast_manager & m, model_core & md):
 }
 
 /**
-   \brieft Return as-array[f] where f is a fresh function symbol with the right domain and range for the array sort s.
+   \brief Return as-array[f] where f is a fresh function symbol with the right domain and range for the array sort s.
    Store in fi the function interpretation for f.
 */
 expr * array_factory::mk_array_interp(sort * s, func_interp * & fi) {
diff --git a/src/muz/spacer/spacer_mbc.h b/src/muz/spacer/spacer_mbc.h
index 5c61f2d7b50..19bbe839d3a 100644
--- a/src/muz/spacer/spacer_mbc.h
+++ b/src/muz/spacer/spacer_mbc.h
@@ -34,7 +34,7 @@ class mbc {
     typedef obj_map<func_decl, unsigned> partition_map;
 
     /**
-       \Brief Model Based Cartesian projection of lits
+       \brief Model Based Cartesian projection of lits
      */
     void operator()(const partition_map &pmap, expr_ref_vector &lits, model &mdl,
                     vector<expr_ref_vector> &res);
diff --git a/src/smt/seq_offset_eq.h b/src/smt/seq_offset_eq.h
index e3c138f9e16..3535343fd74 100644
--- a/src/smt/seq_offset_eq.h
+++ b/src/smt/seq_offset_eq.h
@@ -42,7 +42,7 @@ namespace smt {
         seq_offset_eq(theory& th, ast_manager& m);
         bool empty() const { return m_offset_equalities.empty(); }
         /**
-           \breif determine if r1 = r2 + offset
+           \brief determine if r1 = r2 + offset
          */
         bool find(enode* r1, enode* r2, int& offset) const;
         bool contains(enode* r1, enode* r2) const { int offset = 0; return find(r1, r2, offset); }
diff --git a/src/smt/smt_relevancy.h b/src/smt/smt_relevancy.h
index 53bf4807d6c..87cc3847cd1 100644
--- a/src/smt/smt_relevancy.h
+++ b/src/smt/smt_relevancy.h
@@ -169,12 +169,12 @@ namespace smt {
         bool enabled() const;
 
         /**
-           \Brief Return the region allocator for the smt::context that owns this propagator.
+           \brief Return the region allocator for the smt::context that owns this propagator.
         */
         region & get_region() const;
 
         /**
-           \Brief Return the ast_manager for the smt::context that owns this propagator.
+           \brief Return the ast_manager for the smt::context that owns this propagator.
         */
         ast_manager & get_manager() const;