diff --git a/src/solvers/qbf/qbf_bdd_core.cpp b/src/solvers/qbf/qbf_bdd_core.cpp
index 4d4f17da6be..57b47b90d54 100644
--- a/src/solvers/qbf/qbf_bdd_core.cpp
+++ b/src/solvers/qbf/qbf_bdd_core.cpp
@@ -14,16 +14,28 @@ Author: CM Wintersteiger
 
 #include <langapi/language_util.h>
 
+#include <solvers/prop/literal.h>
+
 #include <cuddObj.hh> // CUDD Library
 
 /*! \cond */
 // FIX FOR THE CUDD LIBRARY
 
-inline DdNode *
-DD::getNode() const
+/*******************************************************************\
+
+Function: DD::getNode
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+inline DdNode *DD::getNode() const
 {
     return node;
-
 } // DD::getNode
 /*! \endcond */
 
@@ -44,7 +56,7 @@ Function: qbf_bdd_certificatet::qbf_bdd_certificatet
 
 qbf_bdd_certificatet::qbf_bdd_certificatet(void) : qdimacs_coret()
 {
-  bdd_manager=new Cudd(0,0);
+  bdd_manager=new Cudd(0, 0);
 }
 
 /*******************************************************************\
@@ -61,11 +73,10 @@ Function: qbf_bdd_certificatet::~qbf_bdd_certificatet
 
 qbf_bdd_certificatet::~qbf_bdd_certificatet(void)
 {
-  for(model_bddst::iterator it=model_bdds.begin();
-      it!=model_bdds.end();
-      it++)
+  for(const BDD* model : model_bdds)
   {
-    if(*it!=NULL) { delete(*it); *it=NULL; }
+    if(model)
+      delete model;
   }
   model_bdds.clear();
 
@@ -127,16 +138,18 @@ Function: qbf_bdd_coret::~qbf_bdd_coret
 
 qbf_bdd_coret::~qbf_bdd_coret()
 {
-  for(bdd_variable_mapt::iterator it=bdd_variable_map.begin();
-      it!=bdd_variable_map.end();
-      it++)
+  for(const BDD* variable : bdd_variable_map)
   {
-    if (*it) { delete(*it); *it=NULL; }
+    if(variable)
+      delete variable;
   }
   bdd_variable_map.clear();
 
-  if(matrix) delete(matrix);
-  matrix=NULL;
+  if(matrix)
+  {
+    delete(matrix);
+    matrix=NULL;
+  }
 }
 
 /*******************************************************************\
@@ -189,17 +202,15 @@ Function: qbf_bdd_coret::prop_solve
 propt::resultt qbf_bdd_coret::prop_solve()
 {
   {
-    std::string msg=
-      solver_text() + ": "+
-      std::to_string(no_variables())+" variables, "+
-      std::to_string(matrix->nodeCount())+" nodes";
-    messaget::status() << msg << messaget::eom;
+    status() << solver_text() << ": "
+             << std::to_string(no_variables()) << " variables, "
+             << std::to_string(matrix->nodeCount()) << " nodes" << eom;
   }
 
   model_bdds.resize(no_variables()+1, NULL);
 
   // Eliminate variables
-  for(quantifierst::const_reverse_iterator it=quantifiers.rbegin();
+  for(auto it=quantifiers.rbegin();
       it!=quantifiers.rend();
       it++)
   {
@@ -212,13 +223,14 @@ propt::resultt qbf_bdd_coret::prop_solve()
         matrix->nodeCount() << " nodes" << std::endl;
       #endif
 
-      BDD* model = new BDD();
+      BDD *model=new BDD();
       const BDD &varbdd=*bdd_variable_map[var];
-      *model = matrix->AndAbstract(varbdd.Xnor(bdd_manager->bddOne()),
-                                   varbdd);
+      *model=matrix->AndAbstract(
+        varbdd.Xnor(bdd_manager->bddOne()),
+        varbdd);
       model_bdds[var]=model;
 
-      *matrix = matrix->ExistAbstract(*bdd_variable_map[var]);
+      *matrix=matrix->ExistAbstract(*bdd_variable_map[var]);
     }
     else if(it->type==quantifiert::UNIVERSAL)
     {
@@ -227,10 +239,10 @@ propt::resultt qbf_bdd_coret::prop_solve()
         matrix->nodeCount() << " nodes" << std::endl;
       #endif
 
-      *matrix = matrix->UnivAbstract(*bdd_variable_map[var]);
+      *matrix=matrix->UnivAbstract(*bdd_variable_map[var]);
     }
     else
-      throw ("Unquantified variable");
+      throw "unquantified variable";
   }
 
   if(*matrix==bdd_manager->bddOne())
@@ -261,7 +273,7 @@ Function: qbf_bdd_coret::is_in_core
 
 bool qbf_bdd_coret::is_in_core(literalt l) const
 {
-  throw ("NYI");
+  throw "nyi";
 }
 
 /*******************************************************************\
@@ -278,7 +290,7 @@ Function: qbf_bdd_coret::m_get
 
 qdimacs_coret::modeltypet qbf_bdd_coret::m_get(literalt a) const
 {
-  throw ("NYI");
+  throw "nyi";
 }
 
 /*******************************************************************\
@@ -299,7 +311,7 @@ literalt qbf_bdd_coret::new_variable()
 
   bdd_variable_map.resize(res.var_no()+1, NULL);
   BDD &var=*(new BDD());
-  var = bdd_manager->bddVar();
+  var=bdd_manager->bddVar();
   bdd_variable_map[res.var_no()]=&var;
 
   return res;
@@ -326,17 +338,17 @@ void qbf_bdd_coret::lcnf(const bvt &bv)
 
   BDD clause(bdd_manager->bddZero());
 
-  for(unsigned long i=0; i<new_bv.size(); i++)
+  for(const literalt &l : new_bv)
   {
-    literalt l=new_bv[i];
     BDD v(*bdd_variable_map[l.var_no()]);
 
-    if(l.sign()) v = ~v;
+    if(l.sign())
+      v=~v;
 
-    clause |= v;
+    clause|=v;
   }
 
-  *matrix &= clause;
+  *matrix&=clause;
 }
 
 /*******************************************************************\
@@ -353,15 +365,17 @@ Function: qbf_bdd_coret::lor
 
 literalt qbf_bdd_coret::lor(literalt a, literalt b)
 {
-  literalt nl = new_variable();
+  literalt nl=new_variable();
 
   BDD abdd(*bdd_variable_map[a.var_no()]);
   BDD bbdd(*bdd_variable_map[b.var_no()]);
 
-  if(a.sign()) abdd = ~abdd;
-  if(b.sign()) bbdd = ~bbdd;
+  if(a.sign())
+    abdd=~abdd;
+  if(b.sign())
+    bbdd=~bbdd;
 
-  *bdd_variable_map[nl.var_no()] |= abdd | bbdd;
+  *bdd_variable_map[nl.var_no()]|=abdd | bbdd;
 
   return nl;
 }
@@ -380,25 +394,26 @@ Function: qbf_bdd_coret::lor
 
 literalt qbf_bdd_coret::lor(const bvt &bv)
 {
-  forall_literals(it, bv)
-    if(*it==const_literal(true))
-      return const_literal(true);
+  for(const literalt &literal : bv)
+  {
+    if(literal==const_literal(true))
+      return literal;
+  }
 
-  literalt nl = new_variable();
+  literalt nl=new_variable();
 
-  BDD &orbdd = *bdd_variable_map[nl.var_no()];
+  BDD &orbdd=*bdd_variable_map[nl.var_no()];
 
-  forall_literals(it, bv)
+  for(const literalt &literal : bv)
   {
-    literalt l=*it;
-
-    if(l==const_literal(false))
+    if(literal==const_literal(false))
       continue;
 
-    BDD v(*bdd_variable_map[l.var_no()]);
-    if(l.sign()) v = ~v;
+    BDD v(*bdd_variable_map[literal.var_no()]);
+    if(literal.sign())
+      v=~v;
 
-    orbdd |= v;
+    orbdd|=v;
   }
 
   return nl;
@@ -420,23 +435,19 @@ void qbf_bdd_coret::compress_certificate(void)
 {
   status() << "Compressing Certificate" << eom;
 
-  for(quantifierst::const_iterator it=quantifiers.begin();
-      it!=quantifiers.end();
-      it++)
+  for(const quantifiert& quantifier : quantifiers)
   {
-    if(it->type==quantifiert::EXISTENTIAL)
+    if(quantifier.type==quantifiert::EXISTENTIAL)
     {
-      const BDD &var=*bdd_variable_map[it->var_no];
-      const BDD &model=*model_bdds[it->var_no];
+      const BDD &var=*bdd_variable_map[quantifier.var_no];
+      const BDD &model=*model_bdds[quantifier.var_no];
 
       if(model==bdd_manager->bddOne() ||
          model==bdd_manager->bddZero())
       {
-        for(quantifierst::const_iterator it2=it;
-            it2!=quantifiers.end();
-            it2++)
+        for(const quantifiert &quantifier2 : quantifier)
         {
-          BDD &model2=*model_bdds[it2->var_no];
+          BDD &model2=*model_bdds[quantifier2.var_no];
 
           if(model==bdd_manager->bddZero())
             model2=model2.AndAbstract(~var, var);
@@ -464,7 +475,7 @@ const exprt qbf_bdd_certificatet::f_get(literalt l)
 {
   quantifiert q;
   if(!find_quantifier(l, q))
-    throw ("No model for unquantified variable");
+    throw "no model for unquantified variable";
 
   // universal?
   if(q.type==quantifiert::UNIVERSAL)
@@ -473,7 +484,7 @@ const exprt qbf_bdd_certificatet::f_get(literalt l)
     variable_mapt::const_iterator it=variable_map.find(l.var_no());
 
     if(it==variable_map.end())
-      throw "Variable map error";
+      throw "variable map error";
 
     const exprt &sym=it->second.first;
     unsigned index=it->second.second;
@@ -485,7 +496,8 @@ const exprt qbf_bdd_certificatet::f_get(literalt l)
     uint_type.set(ID_width, 32);
     extract_expr.copy_to_operands(from_integer(index, uint_type));
 
-    if(l.sign()) extract_expr.negate();
+    if(l.sign())
+      extract_expr.negate();
 
     return extract_expr;
   }
@@ -517,17 +529,17 @@ const exprt qbf_bdd_certificatet::f_get(literalt l)
     model.PrintMinterm();
     #endif
 
-    int* cube;
+    int *cube;
     DdGen *generator;
-//    CUDD_VALUE_TYPE value;
 
     exprt result=or_exprt();
 
-    Cudd_ForeachPrime(bdd_manager->getManager(),
-                      model.getNode(), model.getNode(),
-                      generator,
-                      cube)
-//    Cudd_ForeachCube(bdd_manager->getManager(), model.getNode(), generator, cube, value)
+    Cudd_ForeachPrime(
+      bdd_manager->getManager(),
+      model.getNode(),
+      model.getNode(),
+      generator,
+      cube)
     {
       exprt prime=and_exprt();
 
@@ -540,7 +552,8 @@ const exprt qbf_bdd_certificatet::f_get(literalt l)
 
       for(signed i=0; i<bdd_manager->ReadSize(); i++)
       {
-        if(quantifiers[i].var_no==l.var_no()) break; // is this sound?
+        if(quantifiers[i].var_no==l.var_no())
+          break; // is this sound?
 
         if(cube[i]!=2)
         {
@@ -567,9 +580,10 @@ const exprt qbf_bdd_certificatet::f_get(literalt l)
       final=false_exprt();
     else if(result.operands().size()==1)
       final=result.op0();
-    else final=result;
+    else
+      final=result;
 
-    function_cache[l.var_no()] = final;
+    function_cache[l.var_no()]=final;
 
     if(l.sign())
       return not_exprt(final);
diff --git a/src/solvers/qbf/qbf_bdd_core.h b/src/solvers/qbf/qbf_bdd_core.h
index 4fc8fd1abaa..4c9d3e6fd2d 100644
--- a/src/solvers/qbf/qbf_bdd_core.h
+++ b/src/solvers/qbf/qbf_bdd_core.h
@@ -14,13 +14,13 @@ Author: CM Wintersteiger
 
 #include "qdimacs_core.h"
 
-class Cudd;
-class BDD;
+class Cudd; // NOLINT(*)
+class BDD; // NOLINT(*)
 
-class qbf_bdd_certificatet : public qdimacs_coret
+class qbf_bdd_certificatet:public qdimacs_coret
 {
 protected:
-  Cudd* bdd_manager;
+  Cudd *bdd_manager;
 
   typedef std::vector<BDD*> model_bddst;
   model_bddst model_bdds;
diff --git a/src/solvers/qbf/qbf_quantor.cpp b/src/solvers/qbf/qbf_quantor.cpp
index 8106b29e986..27ecdf95920 100644
--- a/src/solvers/qbf/qbf_quantor.cpp
+++ b/src/solvers/qbf/qbf_quantor.cpp
@@ -110,14 +110,10 @@ propt::resultt qbf_quantort::prop_solve()
     write_qdimacs_cnf(out);
   }
 
-  //std::string options=" --equivalences=0";
-  std::string options="";
-
   // solve it
-  int res=system(("quantor "+qbf_tmp_file+
-         options+
-         " -o "+result_tmp_file).c_str());
-  assert(0 == res);
+  int res=system((
+    "quantor "+qbf_tmp_file+" -o "+result_tmp_file).c_str());
+  assert(0==res);
 
   bool result=false;
 
diff --git a/src/solvers/qbf/qbf_qube.cpp b/src/solvers/qbf/qbf_qube.cpp
index 4bf79ad8cf6..f32d77d3370 100644
--- a/src/solvers/qbf/qbf_qube.cpp
+++ b/src/solvers/qbf/qbf_qube.cpp
@@ -116,14 +116,12 @@ propt::resultt qbf_qubet::prop_solve()
     write_qdimacs_cnf(out);
   }
 
-  //std::string options=" --equivalences=0";
   std::string options="";
 
   // solve it
-  int res=system(("QuBE "+qbf_tmp_file+
-         options+
-         " > "+result_tmp_file).c_str());
-  assert(0 == res);
+  int res=system(
+    ("QuBE "+qbf_tmp_file+options+" > "+result_tmp_file).c_str());
+  assert(0==res);
 
   bool result=false;
 
diff --git a/src/solvers/qbf/qbf_qube_core.cpp b/src/solvers/qbf/qbf_qube_core.cpp
index 53b6e0d6182..e9593a1702e 100644
--- a/src/solvers/qbf/qbf_qube_core.cpp
+++ b/src/solvers/qbf/qbf_qube_core.cpp
@@ -83,10 +83,9 @@ propt::resultt qbf_qube_coret::prop_solve()
     return P_SATISFIABLE;
 
   {
-    messaget::status() <<
-      "QuBE: " <<
-      no_variables() << " variables, " <<
-      no_clauses() << " clauses" << eom;
+    messaget::status() << "QuBE: "
+      << no_variables() << " variables, "
+      << no_clauses() << " clauses" << eom;
   }
 
   std::string result_tmp_file="qube.out";
@@ -102,9 +101,9 @@ propt::resultt qbf_qube_coret::prop_solve()
   std::string options="";
 
   // solve it
-  int res=system(("QuBE " + options + " " + qbf_tmp_file +
-          " > "+result_tmp_file).c_str());
-  assert(0 == res);
+  int res=system((
+    "QuBE "+options+" "+qbf_tmp_file+" > "+result_tmp_file).c_str());
+  assert(0==res);
 
   bool result=false;
 
@@ -126,9 +125,9 @@ propt::resultt qbf_qube_coret::prop_solve()
       {
         mp_integer b(line.substr(2).c_str());
         if(b<0)
-          assignment[integer2unsigned(b.negate())] = false;
+          assignment[integer2unsigned(b.negate())]=false;
         else
-          assignment[integer2unsigned(b)] = true;
+          assignment[integer2unsigned(b)]=true;
       }
       else if(line=="s cnf 1")
       {
@@ -180,7 +179,7 @@ Function: qbf_qube_coret::is_in_core
 
 bool qbf_qube_coret::is_in_core(literalt l) const
 {
-  throw ("Not supported");
+  throw "not supported";
 }
 
 /*******************************************************************\
@@ -197,5 +196,5 @@ Function: qbf_qube_coret::m_get
 
 qdimacs_coret::modeltypet qbf_qube_coret::m_get(literalt a) const
 {
-  throw ("not supported");
+  throw "not supported";
 }
diff --git a/src/solvers/qbf/qbf_qube_core.h b/src/solvers/qbf/qbf_qube_core.h
index 55dd915296c..348d9492015 100644
--- a/src/solvers/qbf/qbf_qube_core.h
+++ b/src/solvers/qbf/qbf_qube_core.h
@@ -11,7 +11,7 @@ Author: CM Wintersteiger
 
 #include "qdimacs_core.h"
 
-class qbf_qube_coret : public qdimacs_coret
+class qbf_qube_coret:public qdimacs_coret
 {
 protected:
   std::string qbf_tmp_file;
@@ -32,7 +32,7 @@ class qbf_qube_coret : public qdimacs_coret
   {
     unsigned v=a.var_no();
 
-    assignmentt::const_iterator fit = assignment.find(v);
+    assignmentt::const_iterator fit=assignment.find(v);
 
     if(fit!=assignment.end())
       return a.sign()?tvt(!fit->second) : tvt(fit->second);
@@ -50,7 +50,7 @@ class qbf_qube_coret : public qdimacs_coret
 
   virtual const exprt f_get(literalt l)
   {
-    throw "Qube does not support full certificates.";
+    throw "qube does not support full certificates.";
   }
 };
 
diff --git a/src/solvers/qbf/qbf_skizzo.cpp b/src/solvers/qbf/qbf_skizzo.cpp
index 678d070f7ac..27837ef57b8 100644
--- a/src/solvers/qbf/qbf_skizzo.cpp
+++ b/src/solvers/qbf/qbf_skizzo.cpp
@@ -116,14 +116,12 @@ propt::resultt qbf_skizzot::prop_solve()
     write_qdimacs_cnf(out);
   }
 
-  //std::string options=" --equivalences=0";
   std::string options="";
 
   // solve it
-  int res=system(("sKizzo "+qbf_tmp_file+
-         options+
-         " > "+result_tmp_file).c_str());
-  assert(0 == res);
+  int res=system((
+    "sKizzo "+qbf_tmp_file+options+" > "+result_tmp_file).c_str());
+  assert(0==res);
 
   bool result=false;
 
diff --git a/src/solvers/qbf/qbf_skizzo_core.cpp b/src/solvers/qbf/qbf_skizzo_core.cpp
index 127f4a9e42e..0b79ca216a6 100644
--- a/src/solvers/qbf/qbf_skizzo_core.cpp
+++ b/src/solvers/qbf/qbf_skizzo_core.cpp
@@ -16,11 +16,21 @@ Author: CM Wintersteiger
 /*! \cond */
 // FIX FOR THE CUDD LIBRARY
 
-inline DdNode *
-DD::getNode() const
+/*******************************************************************\
+
+Function: DD::getNode
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+inline DdNode *DD::getNode() const
 {
     return node;
-
 } // DD::getNode
 /*! \endcond */
 
@@ -40,7 +50,8 @@ Function: qbf_skizzo_coret::qbf_skizzo_coret
 
 \*******************************************************************/
 
-qbf_skizzo_coret::qbf_skizzo_coret() : qbf_bdd_certificatet()
+qbf_skizzo_coret::qbf_skizzo_coret():
+  qbf_bdd_certificatet()
 {
   // skizzo crashes on broken lines
   break_lines=false;
@@ -119,9 +130,8 @@ propt::resultt qbf_skizzo_coret::prop_solve()
   std::string options="";
 
   // solve it
-  system(("sKizzo -log "+qbf_tmp_file+
-         options+
-         " > "+result_tmp_file).c_str());
+  system((
+    "sKizzo -log "+qbf_tmp_file+options+" > "+result_tmp_file).c_str());
 
   bool result=false;
 
@@ -193,7 +203,7 @@ Function: qbf_skizzo_coret::is_in_core
 
 bool qbf_skizzo_coret::is_in_core(literalt l) const
 {
-  throw ("NYI");
+  throw "nyi";
 }
 
 /*******************************************************************\
@@ -210,7 +220,7 @@ Function: qbf_skizzo_coret::m_get
 
 qdimacs_coret::modeltypet qbf_skizzo_coret::m_get(literalt a) const
 {
-  throw ("NYI");
+  throw "nyi";
 }
 
 /*******************************************************************\
@@ -229,10 +239,10 @@ bool qbf_skizzo_coret::get_certificate(void)
 {
   std::string result_tmp_file="ozziKs.out";
   std::string options="-dump qbm=bdd";
-  std::string log_file = qbf_tmp_file + ".sKizzo.log";
+  std::string log_file=qbf_tmp_file+".sKizzo.log";
 
-  system(("ozziKs " + options + " " + log_file +
-          " > "+result_tmp_file).c_str());
+  system((
+    "ozziKs "+options+" "+log_file+" > "+result_tmp_file).c_str());
 
   // read result
   bool result=false;
@@ -313,18 +323,20 @@ bool qbf_skizzo_coret::get_certificate(void)
       assert(cur!=0);
 
       e_list[i]=cur;
-      if(cur>e_max) e_max=cur;
+      if(cur>e_max)
+        e_max=cur;
 
-      e_lists = e_lists.substr(space+1);
+      e_lists=e_lists.substr(space+1);
     }
 
     if(!result)
-      throw ("Existential mapping from sKizzo missing");
+      throw "existential mapping from sKizzo missing";
 
     in.close();
 
     // workaround for long comments
-    system(("sed -e \"s/^#.*$/# no comment/\" -i "+qbf_tmp_file+".qbm").c_str());
+    system((
+      "sed -e \"s/^#.*$/# no comment/\" -i "+qbf_tmp_file+".qbm").c_str());
   }
 
 
@@ -333,19 +345,25 @@ bool qbf_skizzo_coret::get_certificate(void)
     std::string bdd_file=qbf_tmp_file+".qbm";
 
     // dddmp insists on a non-const string here...
-    char filename[bdd_file.size()+1];
-    strcpy(filename, bdd_file.c_str());
+    // The linter insists on compile time constant for arrays
+    char filename[bdd_file.size()+1]; // NOLINT(*)
+    snprintf(filename, bdd_file.size()+1, bdd_file.c_str());
 
     bdd_manager->AutodynEnable(CUDD_REORDER_SIFT);
 
-    int nroots =
-    Dddmp_cuddBddArrayLoad(bdd_manager->getManager(),
-                           DDDMP_ROOT_MATCHLIST, NULL,
-                           DDDMP_VAR_MATCHIDS, NULL, NULL, NULL,
-                           DDDMP_MODE_DEFAULT,
-                           filename,
-                           NULL,
-                           &bdds);
+    int nroots=
+      Dddmp_cuddBddArrayLoad(
+        bdd_manager->getManager(),
+        DDDMP_ROOT_MATCHLIST,
+        NULL,
+        DDDMP_VAR_MATCHIDS,
+        NULL,
+        NULL,
+        NULL,
+        DDDMP_MODE_DEFAULT,
+        filename,
+        NULL,
+        &bdds);
 
     assert(nroots=2*n_e); // ozziKs documentation guarantees that.
 
@@ -354,10 +372,10 @@ bool qbf_skizzo_coret::get_certificate(void)
     for(unsigned i=0; i<e_list.size(); i++)
     {
       int cur=e_list[i];
-      DdNode *posNode = bdds[2*i];
-      DdNode *negNode = bdds[2*i+1];
+      DdNode *posNode=bdds[2*i];
+      DdNode *negNode=bdds[2*i+1];
 
-      if(Cudd_DagSize(posNode) <= Cudd_DagSize(negNode))
+      if(Cudd_DagSize(posNode)<=Cudd_DagSize(negNode))
         model_bdds[cur]=new BDD(*bdd_manager, posNode);
       else
         model_bdds[cur]=new BDD(*bdd_manager, Cudd_Not(negNode));
diff --git a/src/solvers/qbf/qbf_skizzo_core.h b/src/solvers/qbf/qbf_skizzo_core.h
index 376936de4e5..6ffa06c9c84 100644
--- a/src/solvers/qbf/qbf_skizzo_core.h
+++ b/src/solvers/qbf/qbf_skizzo_core.h
@@ -11,8 +11,8 @@ Author: CM Wintersteiger
 
 #include "qbf_bdd_core.h"
 
-class qbf_skizzo_coret :
-  public qbf_bdd_certificatet // a qdimacs_coret with f_get from BDDs
+// a qdimacs_coret with f_get from BDDs
+class qbf_skizzo_coret:public qbf_bdd_certificatet
 {
 public:
   qbf_skizzo_coret();
diff --git a/src/solvers/qbf/qbf_squolem.cpp b/src/solvers/qbf/qbf_squolem.cpp
index f6fa86278ab..a869603a737 100644
--- a/src/solvers/qbf/qbf_squolem.cpp
+++ b/src/solvers/qbf/qbf_squolem.cpp
@@ -21,7 +21,8 @@ Function: qbf_squolemt::qbf_squolemt
 
 \*******************************************************************/
 
-qbf_squolemt::qbf_squolemt() : early_decision(false)
+qbf_squolemt::qbf_squolemt():
+  early_decision(false)
 {
 }
 
@@ -98,7 +99,8 @@ propt::resultt qbf_squolemt::prop_solve()
     messaget::status() << msg << messaget::eom;
   }
 
-  if(early_decision) return P_UNSATISFIABLE;
+  if(early_decision)
+    return P_UNSATISFIABLE;
 
 //  squolem.options.set_showStatus(true);
   squolem.options.set_freeOnExit(true);
@@ -108,7 +110,7 @@ propt::resultt qbf_squolemt::prop_solve()
   squolem.options.set_saveDebugFile(true);
 
   squolem.endOfOriginals();
-  bool result = squolem.decide();
+  bool result=squolem.decide();
 
   if(result)
   {
@@ -138,7 +140,8 @@ Function: qbf_squolemt::lcnf
 
 void qbf_squolemt::lcnf(const bvt &bv)
 {
-  if(early_decision) return; // we don't need no more...
+  if(early_decision)
+    return; // we don't need no more...
 
   bvt new_bv;
 
@@ -158,7 +161,7 @@ void qbf_squolemt::lcnf(const bvt &bv)
     buffer[i]=new_bv[i].dimacs();
     i++;
   }
-  while (i<new_bv.size());
+  while(i<new_bv.size());
 
   if(!squolem.addClause(buffer))
     early_decision=true;
@@ -178,8 +181,9 @@ Function: qbf_squolemt::add_quantifier
 
 void qbf_squolemt::add_quantifier(const quantifiert &quantifier)
 {
-  squolem.quantifyVariableInner(quantifier.var_no,
-                                quantifier.type==quantifiert::UNIVERSAL);
+  squolem.quantifyVariableInner(
+    quantifier.var_no,
+    quantifier.type==quantifiert::UNIVERSAL);
 
   qdimacs_cnft::add_quantifier(quantifier); // necessary?
 }
diff --git a/src/solvers/qbf/qbf_squolem_core.cpp b/src/solvers/qbf/qbf_squolem_core.cpp
index e076e9341a2..00229cd8fee 100644
--- a/src/solvers/qbf/qbf_squolem_core.cpp
+++ b/src/solvers/qbf/qbf_squolem_core.cpp
@@ -171,7 +171,7 @@ propt::resultt qbf_squolem_coret::prop_solve()
   }
 
   squolem->endOfOriginals();
-  bool result = squolem->decide();
+  bool result=squolem->decide();
 
   if(result)
   {
@@ -206,7 +206,7 @@ bool qbf_squolem_coret::is_in_core(literalt l) const
 
 /*******************************************************************\
 
-Function: qbf_squolem_coret::l_get
+Function: qbf_squolem_coret::m_get
 
   Inputs:
 
@@ -242,7 +242,8 @@ Function: qbf_squolem_coret::lcnf
 
 void qbf_squolem_coret::lcnf(const bvt &bv)
 {
-  if(early_decision) return; // we don't need no more...
+  if(early_decision)
+    return; // we don't need no more...
 
   bvt new_bv;
 
@@ -262,7 +263,7 @@ void qbf_squolem_coret::lcnf(const bvt &bv)
     buffer[i]=new_bv[i].dimacs();
     i++;
   }
-  while (i<new_bv.size());
+  while(i<new_bv.size());
 
   if(!squolem->addClause(buffer))
     early_decision=true;
@@ -282,8 +283,9 @@ Function: qbf_squolem_coret::add_quantifier
 
 void qbf_squolem_coret::add_quantifier(const quantifiert &quantifier)
 {
-  squolem->quantifyVariableInner(quantifier.var_no,
-                                quantifier.type==quantifiert::UNIVERSAL);
+  squolem->quantifyVariableInner(
+    quantifier.var_no,
+    quantifier.type==quantifiert::UNIVERSAL);
 
   qdimacs_cnft::add_quantifier(quantifier); // necessary?
 }
@@ -380,7 +382,7 @@ const exprt qbf_squolem_coret::f_get(literalt l)
     variable_mapt::const_iterator it=variable_map.find(l.var_no());
 
     if(it==variable_map.end())
-      throw "Variable map error";
+      throw "variable map error";
 
     const exprt &sym=it->second.first;
     unsigned index=it->second.second;
@@ -391,7 +393,8 @@ const exprt qbf_squolem_coret::f_get(literalt l)
     uint_type.set(ID_width, 32);
     extract_expr.copy_to_operands(from_integer(index, uint_type));
 
-    if(l.sign()) extract_expr.negate();
+    if(l.sign())
+      extract_expr.negate();
 
     return extract_expr;
   }
@@ -410,7 +413,7 @@ const exprt qbf_squolem_coret::f_get(literalt l)
   }
   else
   {
-    WitnessStack *wsp = squolem->getModelFunction(Literal(l.dimacs()));
+    WitnessStack *wsp=squolem->getModelFunction(Literal(l.dimacs()));
     exprt res;
 
     if(wsp==NULL || wsp->empty())
@@ -423,7 +426,7 @@ const exprt qbf_squolem_coret::f_get(literalt l)
     else
       res=f_get_dnf(wsp);
 
-    function_cache[l.var_no()] = res;
+    function_cache[l.var_no()]=res;
 
     if(l.sign())
       return not_exprt(res);
@@ -448,7 +451,8 @@ const exprt qbf_squolem_coret::f_get_cnf(WitnessStack *wsp)
 {
   Clause *p=wsp->negWits;
 
-  if(!p) return exprt(ID_true, typet(ID_bool));
+  if(!p)
+    return exprt(ID_true, typet(ID_bool));
 
   exprt::operandst operands;
 
@@ -459,7 +463,7 @@ const exprt qbf_squolem_coret::f_get_cnf(WitnessStack *wsp)
     for(unsigned i=0; i<p->size; i++)
     {
       const Literal &lit=p->literals[i];
-      exprt subf = f_get(literalt(var(lit), isPositive(lit))); // negated!
+      exprt subf=f_get(literalt(var(lit), isPositive(lit))); // negated!
       if(find(clause.operands().begin(), clause.operands().end(), subf)==
          clause.operands().end())
         clause.move_to_operands(subf);
@@ -501,7 +505,8 @@ const exprt qbf_squolem_coret::f_get_dnf(WitnessStack *wsp)
 {
   Clause *p=wsp->posWits;
 
-  if(!p) return exprt(ID_false, typet(ID_bool));
+  if(!p)
+    return exprt(ID_false, typet(ID_bool));
 
   exprt::operandst operands;
 
@@ -512,7 +517,7 @@ const exprt qbf_squolem_coret::f_get_dnf(WitnessStack *wsp)
     for(unsigned i=0; i<p->size; i++)
     {
       const Literal &lit=p->literals[i];
-      exprt subf = f_get(literalt(var(lit), !isPositive(lit)));
+      exprt subf=f_get(literalt(var(lit), !isPositive(lit)));
       if(find(cube.operands().begin(), cube.operands().end(), subf)==
          cube.operands().end())
         cube.move_to_operands(subf);
diff --git a/src/solvers/qbf/qbf_squolem_core.h b/src/solvers/qbf/qbf_squolem_core.h
index c09f7d69713..3c6e96252b4 100644
--- a/src/solvers/qbf/qbf_squolem_core.h
+++ b/src/solvers/qbf/qbf_squolem_core.h
@@ -16,7 +16,7 @@ Author: CM Wintersteiger
 class qbf_squolem_coret:public qdimacs_coret
 {
 protected:
-  Squolem2* squolem;
+  Squolem2 *squolem;
   bool early_decision;
 
 public:
diff --git a/src/solvers/qbf/qdimacs_core.cpp b/src/solvers/qbf/qdimacs_core.cpp
index 979174d22a9..3ffb8ec6db2 100644
--- a/src/solvers/qbf/qdimacs_core.cpp
+++ b/src/solvers/qbf/qdimacs_core.cpp
@@ -9,8 +9,6 @@ Author: CM Wintersteiger
 #include <util/arith_tools.h>
 #include <util/std_expr.h>
 
-//#include <solvers/flattening/boolbv_width.h>
-
 #include "qdimacs_core.h"
 
 /*******************************************************************\
@@ -56,7 +54,7 @@ void qdimacs_coret::simplify_extractbits(exprt &expr) const
       std::string value_string;
       value_string.resize(width, '0');
 
-      if(it->second.size() == width) // all bits extracted from this one!
+      if(it->second.size()==width) // all bits extracted from this one!
       {
         const irep_idt &ident=it->first.get(ID_identifier);
         const exprt::operandst &old_operands=expr.operands();
@@ -74,10 +72,10 @@ void qdimacs_coret::simplify_extractbits(exprt &expr) const
               const exprt &val_expr=oit->op1();
               mp_integer value;
               to_integer(val_expr, value);
-              value_string[value.to_ulong()] = '1';
+              value_string[value.to_ulong()]='1';
 
               #if 0
-              std::cout << "[" << value << "] = 1" << std::endl;
+              std::cout << "[" << value << "]=1" << std::endl;
               #endif
 
               continue;
@@ -105,7 +103,7 @@ void qdimacs_coret::simplify_extractbits(exprt &expr) const
         std::cout << "FINAL: " << value_string << std::endl;
         #endif
 
-        expr.operands() = new_operands;
+        expr.operands()=new_operands;
       }
       #endif
     }