diff --git a/.clang-format b/.clang-format
index 220d113fa..09d7ac855 100644
--- a/.clang-format
+++ b/.clang-format
@@ -1,12 +1,17 @@
 ---
 Language: Cpp
-BasedOnStyle:  LLVM
+Standard: c++20
+BasedOnStyle: LLVM
 ColumnLimit: 120
 IndentWidth: 4
 AccessModifierOffset: -4
 PointerAlignment: Middle
+QualifierAlignment: Right
+AlignOperands: AlignAfterOperator
 AllowShortFunctionsOnASingleLine: Inline
 AllowShortBlocksOnASingleLine: Always
 AllowShortIfStatementsOnASingleLine: WithoutElse
 IndentCaseLabels: True
+NamespaceIndentation: All
+AlwaysBreakTemplateDeclarations: Yes
 SpaceAfterTemplateKeyword: False
diff --git a/src/cnfizers/TermMapper.cc b/src/cnfizers/TermMapper.cc
index a063a3cf9..ad8c3953d 100644
--- a/src/cnfizers/TermMapper.cc
+++ b/src/cnfizers/TermMapper.cc
@@ -84,7 +84,7 @@ Var TermMapper::getVar(PTRef r) const {
     return v;
 }
 
-const Lit TermMapper::getOrCreateLit(PTRef ptr) {
+Lit const TermMapper::getOrCreateLit(PTRef ptr) {
     PTRef p_tr;
     bool sgn;
     Var v = var_Undef;
diff --git a/src/cnfizers/TermMapper.h b/src/cnfizers/TermMapper.h
index 6819a4a6b..59967c3b5 100644
--- a/src/cnfizers/TermMapper.h
+++ b/src/cnfizers/TermMapper.h
@@ -68,7 +68,7 @@ class TermMapper {
      * Handles the sign of the term correctly, i.e., it returned negative literal for negative term and
      * positive literal for positive term.
      */
-    const Lit getOrCreateLit(PTRef ptr);
+    Lit const getOrCreateLit(PTRef ptr);
 
     // Returns the variable corresponding to the term. The connection must already exist.
     Var getVar(PTRef) const;
diff --git a/src/rewriters/Rewriter.h b/src/rewriters/Rewriter.h
index 10a850930..bc7ba0ccb 100644
--- a/src/rewriters/Rewriter.h
+++ b/src/rewriters/Rewriter.h
@@ -11,7 +11,8 @@
 
 #include "Logic.h"
 
-template<typename TConfig> class Rewriter {
+template<typename TConfig>
+class Rewriter {
 protected:
     Logic & logic;
     TConfig & cfg;
@@ -97,4 +98,4 @@ class NoOpRewriter : Rewriter<DefaultRewriterConfig> {
     NoOpRewriter(Logic & logic) : Rewriter<DefaultRewriterConfig>(logic, config) {}
 };
 
-#endif // OPENSMT_REWRITER_H
\ No newline at end of file
+#endif // OPENSMT_REWRITER_H
diff --git a/src/tsolvers/lasolver/Tableau.cc b/src/tsolvers/lasolver/Tableau.cc
index 7a5ed19d0..4ce8ebb57 100644
--- a/src/tsolvers/lasolver/Tableau.cc
+++ b/src/tsolvers/lasolver/Tableau.cc
@@ -15,9 +15,10 @@
 
 using namespace opensmt;
 namespace {
-template<class C, class E> inline bool contains(const C & container, const E & elem) {
-    return container.find(elem) != container.end();
-}
+    template<class C, class E>
+    inline bool contains(C const & container, E const & elem) {
+        return container.find(elem) != container.end();
+    }
 } // namespace
 
 void Tableau::nonbasicVar(LVRef v) {
@@ -50,17 +51,17 @@ std::size_t Tableau::getPolySize(LVRef basicVar) const {
     return rows[basicVar.x]->size();
 }
 
-const opensmt::Real & Tableau::getCoeff(LVRef basicVar, LVRef nonBasicVar) const {
+opensmt::Real const & Tableau::getCoeff(LVRef basicVar, LVRef nonBasicVar) const {
     assert(rows[basicVar.x]);
     return rows[basicVar.x]->getCoeff(nonBasicVar);
 }
 
-const Tableau::column_t & Tableau::getColumn(LVRef nonBasicVar) const {
+Tableau::column_t const & Tableau::getColumn(LVRef nonBasicVar) const {
     assert(cols[nonBasicVar.x]);
     return *cols[nonBasicVar.x];
 }
 
-const Tableau::Polynomial & Tableau::getRowPoly(LVRef basicVar) const {
+Tableau::Polynomial const & Tableau::getRowPoly(LVRef basicVar) const {
     assert(rows[basicVar.x]);
     return *rows[basicVar.x];
 }
@@ -70,7 +71,7 @@ Tableau::Polynomial & Tableau::getRowPoly(LVRef basicVar) {
     return *rows[basicVar.x];
 }
 
-const Tableau::rows_t & Tableau::getRows() const {
+Tableau::rows_t const & Tableau::getRows() const {
     return rows;
 }
 
@@ -124,7 +125,7 @@ void Tableau::pivot(LVRef bv, LVRef nv) {
     assert(!rows[nv.x]);
     {
         Polynomial & nvPoly = getRowPoly(bv);
-        const auto coeff = nvPoly.removeVar(nv);
+        auto const coeff = nvPoly.removeVar(nv);
         if (not coeff.isOne()) { nvPoly.divideBy(coeff); }
         nvPoly.negate();
         nvPoly.addTerm(bv, coeff.inverse());
@@ -149,7 +150,7 @@ void Tableau::pivot(LVRef bv, LVRef nv) {
         if (rowVar == nv || isQuasiBasic(rowVar)) { continue; }
         // update the polynomials
         auto & poly = getRowPoly(rowVar);
-        const auto nvCoeff = poly.removeVar(nv);
+        auto const nvCoeff = poly.removeVar(nv);
         poly.merge(
             nvPoly, nvCoeff, tmp_storage,
             // informAdded
@@ -193,7 +194,7 @@ void Tableau::print() const {
     for (unsigned i = 0; i != rows.size(); ++i) {
         if (!rows[i]) { continue; }
         std::cout << "Var of the row: " << i << ';';
-        for (const auto & term : this->getRowPoly(LVRef{i})) {
+        for (auto const & term : this->getRowPoly(LVRef{i})) {
             std::cout << "( " << term.coeff << " | " << term.var.x << " ) ";
         }
         std::cout << '\n';
diff --git a/src/tsolvers/lasolver/Tableau.h b/src/tsolvers/lasolver/Tableau.h
index 7d3796fbd..255aceb92 100644
--- a/src/tsolvers/lasolver/Tableau.h
+++ b/src/tsolvers/lasolver/Tableau.h
@@ -67,11 +67,11 @@ class Tableau {
     void newRow(LVRef v, std::unique_ptr<Polynomial> poly);
     std::size_t getNumOfCols() const;
     std::size_t getPolySize(LVRef basicVar) const;
-    const opensmt::Real & getCoeff(LVRef basicVar, LVRef nonBasicVar) const;
-    const column_t & getColumn(LVRef nonBasicVar) const;
-    const Polynomial & getRowPoly(LVRef basicVar) const;
+    opensmt::Real const & getCoeff(LVRef basicVar, LVRef nonBasicVar) const;
+    column_t const & getColumn(LVRef nonBasicVar) const;
+    Polynomial const & getRowPoly(LVRef basicVar) const;
     Polynomial & getRowPoly(LVRef basicVar);
-    const rows_t & getRows() const;
+    rows_t const & getRows() const;
 
     void clear();
     void pivot(LVRef bv, LVRef nv);