diff --git a/src/solvers/prop/prop.cpp b/src/solvers/prop/prop.cpp
index 62cb972297c..2f2a03f78e2 100644
--- a/src/solvers/prop/prop.cpp
+++ b/src/solvers/prop/prop.cpp
@@ -25,3 +25,14 @@ bvt propt::new_variables(std::size_t width)
     result[i]=new_variable();
   return result;
 }
+
+propt::resultt propt::prop_solve()
+{
+  ++number_of_solver_calls;
+  return do_prop_solve();
+}
+
+std::size_t propt::get_number_of_solver_calls() const
+{
+  return number_of_solver_calls;
+}
diff --git a/src/solvers/prop/prop.h b/src/solvers/prop/prop.h
index e5078979e4e..2a861b8e6c2 100644
--- a/src/solvers/prop/prop.h
+++ b/src/solvers/prop/prop.h
@@ -97,7 +97,7 @@ class propt
   // solving
   virtual const std::string solver_text()=0;
   enum class resultt { P_SATISFIABLE, P_UNSATISFIABLE, P_ERROR };
-  virtual resultt prop_solve()=0;
+  resultt prop_solve();
 
   // satisfying assignment
   virtual tvt l_get(literalt a) const=0;
@@ -119,11 +119,16 @@ class propt
     log.warning() << "CPU limit ignored (not implemented)" << messaget::eom;
   }
 
+  std::size_t get_number_of_solver_calls() const;
+
 protected:
+  virtual resultt do_prop_solve() = 0;
+
   // to avoid a temporary for lcnf(...)
   bvt lcnf_bv;
 
   messaget log;
+  std::size_t number_of_solver_calls = 0;
 };
 
 #endif // CPROVER_SOLVERS_PROP_PROP_H
diff --git a/src/solvers/prop/prop_conv.cpp b/src/solvers/prop/prop_conv.cpp
index 0c9f20884f4..3dbb0a1bc6f 100644
--- a/src/solvers/prop/prop_conv.cpp
+++ b/src/solvers/prop/prop_conv.cpp
@@ -512,3 +512,8 @@ void prop_conv_solvert::print_assignment(std::ostream &out) const
   for(const auto &symbol : symbols)
     out << symbol.first << " = " << prop.l_get(symbol.second) << '\n';
 }
+
+std::size_t prop_conv_solvert::get_number_of_solver_calls() const
+{
+  return prop.get_number_of_solver_calls();
+}
diff --git a/src/solvers/prop/prop_conv.h b/src/solvers/prop/prop_conv.h
index a1914148217..365c339548b 100644
--- a/src/solvers/prop/prop_conv.h
+++ b/src/solvers/prop/prop_conv.h
@@ -55,6 +55,9 @@ class prop_convt:public decision_proceduret
 
   // Resource limits:
   virtual void set_time_limit_seconds(uint32_t) {}
+
+  /// Returns the number of incremental solver calls
+  virtual std::size_t get_number_of_solver_calls() const = 0;
 };
 
 //
@@ -122,6 +125,8 @@ class prop_conv_solvert:public prop_convt
     prop.set_time_limit_seconds(lim);
   }
 
+  std::size_t get_number_of_solver_calls() const override;
+
 protected:
   virtual void post_process();
 
diff --git a/src/solvers/sat/cnf_clause_list.h b/src/solvers/sat/cnf_clause_list.h
index 22d89d15aeb..480c95a50dd 100644
--- a/src/solvers/sat/cnf_clause_list.h
+++ b/src/solvers/sat/cnf_clause_list.h
@@ -29,19 +29,20 @@ class cnf_clause_listt:public cnft
   }
   virtual ~cnf_clause_listt() { }
 
-  virtual void lcnf(const bvt &bv);
+  void lcnf(const bvt &bv) override;
 
-  virtual const std::string solver_text()
+  const std::string solver_text() override
   { return "CNF clause list"; }
 
-  virtual tvt l_get(literalt) const
+  tvt l_get(literalt) const override
   {
     return tvt::unknown();
   }
 
-  virtual resultt prop_solve() { return resultt::P_ERROR; }
-
-  virtual size_t no_clauses() const { return clauses.size(); }
+  size_t no_clauses() const override
+  {
+    return clauses.size();
+  }
 
   typedef std::list<bvt> clausest;
 
@@ -76,6 +77,11 @@ class cnf_clause_listt:public cnft
   }
 
 protected:
+  resultt do_prop_solve() override
+  {
+    return resultt::P_ERROR;
+  }
+
   clausest clauses;
 };
 
@@ -97,7 +103,7 @@ class cnf_clause_list_assignmentt:public cnf_clause_listt
     return assignment;
   }
 
-  virtual tvt l_get(literalt literal) const
+  tvt l_get(literalt literal) const override
   {
     if(literal.is_true())
       return tvt(true);
diff --git a/src/solvers/sat/dimacs_cnf.h b/src/solvers/sat/dimacs_cnf.h
index 0677f8ffd2c..f552229e3c2 100644
--- a/src/solvers/sat/dimacs_cnf.h
+++ b/src/solvers/sat/dimacs_cnf.h
@@ -45,29 +45,29 @@ class dimacs_cnf_dumpt:public cnft
   dimacs_cnf_dumpt(std::ostream &_out, message_handlert &message_handler);
   virtual ~dimacs_cnf_dumpt() { }
 
-  virtual const std::string solver_text()
+  const std::string solver_text() override
   {
     return "DIMACS CNF Dumper";
   }
 
-  virtual void lcnf(const bvt &bv);
-
-  virtual resultt prop_solve()
-  {
-    return resultt::P_ERROR;
-  }
+  void lcnf(const bvt &bv) override;
 
-  virtual tvt l_get(literalt) const
+  tvt l_get(literalt) const override
   {
     return tvt::unknown();
   }
 
-  virtual size_t no_clauses() const
+  size_t no_clauses() const override
   {
     return 0;
   }
 
 protected:
+  resultt do_prop_solve() override
+  {
+    return resultt::P_ERROR;
+  }
+
   std::ostream &out;
 };
 
diff --git a/src/solvers/sat/pbs_dimacs_cnf.cpp b/src/solvers/sat/pbs_dimacs_cnf.cpp
index 0cb7829c9b1..8bf33eee15d 100644
--- a/src/solvers/sat/pbs_dimacs_cnf.cpp
+++ b/src/solvers/sat/pbs_dimacs_cnf.cpp
@@ -205,7 +205,7 @@ bool pbs_dimacs_cnft::pbs_solve()
   return satisfied;
 }
 
-propt::resultt pbs_dimacs_cnft::prop_solve()
+propt::resultt pbs_dimacs_cnft::do_prop_solve()
 {
   std::ofstream file("temp.cnf");
 
diff --git a/src/solvers/sat/pbs_dimacs_cnf.h b/src/solvers/sat/pbs_dimacs_cnf.h
index 1d331dc71ba..1d6cc821109 100644
--- a/src/solvers/sat/pbs_dimacs_cnf.h
+++ b/src/solvers/sat/pbs_dimacs_cnf.h
@@ -48,18 +48,18 @@ class pbs_dimacs_cnft:public dimacs_cnft
 
   bool pbs_solve();
 
-  virtual resultt prop_solve();
-
-  virtual tvt l_get(literalt a) const;
+  tvt l_get(literalt a) const override;
 
   // dummy functions
 
-  virtual const std::string solver_text()
+  const std::string solver_text() override
   {
     return "PBS - Pseudo Boolean/CNF Solver and Optimizer";
   }
 
 protected:
+  resultt do_prop_solve() override;
+
   std::set<int> assigned;
 };
 
diff --git a/src/solvers/sat/satcheck_booleforce.cpp b/src/solvers/sat/satcheck_booleforce.cpp
index eedc206695b..bdb4f59fee8 100644
--- a/src/solvers/sat/satcheck_booleforce.cpp
+++ b/src/solvers/sat/satcheck_booleforce.cpp
@@ -79,7 +79,7 @@ void satcheck_booleforce_baset::lcnf(const bvt &bv)
   clause_counter++;
 }
 
-propt::resultt satcheck_booleforce_baset::prop_solve()
+propt::resultt satcheck_booleforce_baset::do_prop_solve()
 {
   PRECONDITION(status == SAT || status == INIT);
 
diff --git a/src/solvers/sat/satcheck_booleforce.h b/src/solvers/sat/satcheck_booleforce.h
index e52dc1b0883..99bbae4fe1e 100644
--- a/src/solvers/sat/satcheck_booleforce.h
+++ b/src/solvers/sat/satcheck_booleforce.h
@@ -20,11 +20,13 @@ class satcheck_booleforce_baset:public cnf_solvert
 public:
   virtual ~satcheck_booleforce_baset();
 
-  virtual const std::string solver_text();
-  virtual resultt prop_solve();
-  virtual tvt l_get(literalt a) const;
+  const std::string solver_text() override;
+  tvt l_get(literalt a) const override;
 
-  virtual void lcnf(const bvt &bv);
+  void lcnf(const bvt &bv) override;
+
+protected:
+  resultt do_prop_solve() override;
 };
 
 class satcheck_booleforcet:public satcheck_booleforce_baset
diff --git a/src/solvers/sat/satcheck_cadical.cpp b/src/solvers/sat/satcheck_cadical.cpp
index 42938c3829a..6c78e3e5693 100644
--- a/src/solvers/sat/satcheck_cadical.cpp
+++ b/src/solvers/sat/satcheck_cadical.cpp
@@ -65,7 +65,7 @@ void satcheck_cadicalt::lcnf(const bvt &bv)
   clause_counter++;
 }
 
-propt::resultt satcheck_cadicalt::prop_solve()
+propt::resultt satcheck_cadicalt::do_prop_solve()
 {
   INVARIANT(status != statust::ERROR, "there cannot be an error");
 
diff --git a/src/solvers/sat/satcheck_cadical.h b/src/solvers/sat/satcheck_cadical.h
index 763b2e3f150..caaf99c0417 100644
--- a/src/solvers/sat/satcheck_cadical.h
+++ b/src/solvers/sat/satcheck_cadical.h
@@ -23,19 +23,26 @@ class satcheck_cadicalt:public cnf_solvert
   satcheck_cadicalt();
   virtual ~satcheck_cadicalt();
 
-  virtual const std::string solver_text() override;
-  virtual resultt prop_solve() override;
-  virtual tvt l_get(literalt a) const override;
-
-  virtual void lcnf(const bvt &bv) override;
-  virtual void set_assignment(literalt a, bool value) override;
-
-  virtual void set_assumptions(const bvt &_assumptions) override;
-  virtual bool has_set_assumptions() const override { return false; }
-  virtual bool has_is_in_conflict() const override { return false; }
-  virtual bool is_in_conflict(literalt a) const override;
+  const std::string solver_text() override;
+  tvt l_get(literalt a) const override;
+
+  void lcnf(const bvt &bv) override;
+  void set_assignment(literalt a, bool value) override;
+
+  void set_assumptions(const bvt &_assumptions) override;
+  bool has_set_assumptions() const override
+  {
+    return false;
+  }
+  bool has_is_in_conflict() const override
+  {
+    return false;
+  }
+  bool is_in_conflict(literalt a) const override;
 
 protected:
+  resultt do_prop_solve() override;
+
   // NOLINTNEXTLINE(readability/identifiers)
   CaDiCaL::Solver * solver;
 };
diff --git a/src/solvers/sat/satcheck_glucose.cpp b/src/solvers/sat/satcheck_glucose.cpp
index 0b7439c9553..14a555f08a9 100644
--- a/src/solvers/sat/satcheck_glucose.cpp
+++ b/src/solvers/sat/satcheck_glucose.cpp
@@ -131,8 +131,8 @@ void satcheck_glucose_baset<T>::lcnf(const bvt &bv)
   }
 }
 
-template<typename T>
-propt::resultt satcheck_glucose_baset<T>::prop_solve()
+template <typename T>
+propt::resultt satcheck_glucose_baset<T>::do_prop_solve()
 {
   PRECONDITION(status != statust::ERROR);
 
diff --git a/src/solvers/sat/satcheck_glucose.h b/src/solvers/sat/satcheck_glucose.h
index 9b6c22e08bb..157bdabf692 100644
--- a/src/solvers/sat/satcheck_glucose.h
+++ b/src/solvers/sat/satcheck_glucose.h
@@ -30,23 +30,30 @@ class satcheck_glucose_baset:public cnf_solvert
   satcheck_glucose_baset(T *, message_handlert &message_handler);
   virtual ~satcheck_glucose_baset();
 
-  virtual resultt prop_solve();
-  virtual tvt l_get(literalt a) const;
+  tvt l_get(literalt a) const override;
 
-  virtual void lcnf(const bvt &bv);
-  virtual void set_assignment(literalt a, bool value);
+  void lcnf(const bvt &bv) override;
+  void set_assignment(literalt a, bool value) override;
 
   // extra MiniSat feature: solve with assumptions
-  virtual void set_assumptions(const bvt &_assumptions);
+  void set_assumptions(const bvt &_assumptions) override;
 
   // extra MiniSat feature: default branching decision
   void set_polarity(literalt a, bool value);
 
-  virtual bool is_in_conflict(literalt a) const;
-  virtual bool has_set_assumptions() const { return true; }
-  virtual bool has_is_in_conflict() const { return true; }
+  bool is_in_conflict(literalt a) const override;
+  bool has_set_assumptions() const override
+  {
+    return true;
+  }
+  bool has_is_in_conflict() const override
+  {
+    return true;
+  }
 
 protected:
+  resultt do_prop_solve() override;
+
   T *solver;
 
   void add_variables();
@@ -58,7 +65,7 @@ class satcheck_glucose_no_simplifiert:
 {
 public:
   explicit satcheck_glucose_no_simplifiert(message_handlert &message_handler);
-  virtual const std::string solver_text();
+  const std::string solver_text() override;
 };
 
 class satcheck_glucose_simplifiert:
@@ -66,8 +73,8 @@ class satcheck_glucose_simplifiert:
 {
 public:
   explicit satcheck_glucose_simplifiert(message_handlert &message_handler);
-  virtual const std::string solver_text();
-  virtual void set_frozen(literalt a);
+  const std::string solver_text() override;
+  void set_frozen(literalt a) override;
   bool is_eliminated(literalt a) const;
 };
 
diff --git a/src/solvers/sat/satcheck_ipasir.cpp b/src/solvers/sat/satcheck_ipasir.cpp
index a8e1840dff0..7063a458009 100644
--- a/src/solvers/sat/satcheck_ipasir.cpp
+++ b/src/solvers/sat/satcheck_ipasir.cpp
@@ -93,7 +93,7 @@ void satcheck_ipasirt::lcnf(const bvt &bv)
   clause_counter++;
 }
 
-propt::resultt satcheck_ipasirt::prop_solve()
+propt::resultt satcheck_ipasirt::do_prop_solve()
 {
   INVARIANT(status!=statust::ERROR, "there cannot be an error");
 
diff --git a/src/solvers/sat/satcheck_ipasir.h b/src/solvers/sat/satcheck_ipasir.h
index 58ffb12d08a..107620cfafc 100644
--- a/src/solvers/sat/satcheck_ipasir.h
+++ b/src/solvers/sat/satcheck_ipasir.h
@@ -22,25 +22,31 @@ class satcheck_ipasirt:public cnf_solvert
   virtual ~satcheck_ipasirt() override;
 
   /// This method returns the description produced by the linked SAT solver
-  virtual const std::string solver_text() override;
-
-  virtual resultt prop_solve() override;
+  const std::string solver_text() override;
 
   /// This method returns the truth value for a literal of the current SAT model
-  virtual tvt l_get(literalt a) const override final;
+  tvt l_get(literalt a) const override final;
 
-  virtual void lcnf(const bvt &bv) override final;
+  void lcnf(const bvt &bv) override final;
 
   /* This method is not supported, and currently not called anywhere in CBMC */
-  virtual void set_assignment(literalt a, bool value) override;
+  void set_assignment(literalt a, bool value) override;
 
-  virtual void set_assumptions(const bvt &_assumptions) override;
+  void set_assumptions(const bvt &_assumptions) override;
 
-  virtual bool is_in_conflict(literalt a) const override;
-  virtual bool has_set_assumptions() const override final { return true; }
-  virtual bool has_is_in_conflict() const override final { return true; }
+  bool is_in_conflict(literalt a) const override;
+  bool has_set_assumptions() const override final
+  {
+    return true;
+  }
+  bool has_is_in_conflict() const override final
+  {
+    return true;
+  }
 
 protected:
+  resultt do_prop_solve() override;
+
   void *solver;
 
   bvt assumptions;
diff --git a/src/solvers/sat/satcheck_lingeling.cpp b/src/solvers/sat/satcheck_lingeling.cpp
index 2cc79855d6e..756754300e5 100644
--- a/src/solvers/sat/satcheck_lingeling.cpp
+++ b/src/solvers/sat/satcheck_lingeling.cpp
@@ -63,7 +63,7 @@ void satcheck_lingelingt::lcnf(const bvt &bv)
   clause_counter++;
 }
 
-propt::resultt satcheck_lingelingt::prop_solve()
+propt::resultt satcheck_lingelingt::do_prop_solve()
 {
   PRECONDITION(status != ERROR);
 
diff --git a/src/solvers/sat/satcheck_lingeling.h b/src/solvers/sat/satcheck_lingeling.h
index ddc9388407c..06c1bbda700 100644
--- a/src/solvers/sat/satcheck_lingeling.h
+++ b/src/solvers/sat/satcheck_lingeling.h
@@ -21,20 +21,27 @@ class satcheck_lingelingt:public cnf_solvert
   satcheck_lingelingt();
   virtual ~satcheck_lingelingt();
 
-  virtual const std::string solver_text();
-  virtual resultt prop_solve();
-  virtual tvt l_get(literalt a) const;
-
-  virtual void lcnf(const bvt &bv);
-  virtual void set_assignment(literalt a, bool value);
-
-  virtual void set_assumptions(const bvt &_assumptions);
-  virtual bool has_set_assumptions() const { return true; }
-  virtual bool has_is_in_conflict() const { return true; }
-  virtual bool is_in_conflict(literalt a) const;
-  virtual void set_frozen(literalt a);
+  const std::string solver_text() override;
+  tvt l_get(literalt a) const override;
+
+  void lcnf(const bvt &bv) override;
+  void set_assignment(literalt a, bool value) override;
+
+  void set_assumptions(const bvt &_assumptions) override;
+  bool has_set_assumptions() const override
+  {
+    return true;
+  }
+  bool has_is_in_conflict() const override
+  {
+    return true;
+  }
+  bool is_in_conflict(literalt a) const override;
+  void set_frozen(literalt a) override;
 
 protected:
+  resultt do_prop_solve() override;
+
   // NOLINTNEXTLINE(readability/identifiers)
   struct LGL * solver;
   bvt assumptions;
diff --git a/src/solvers/sat/satcheck_minisat.cpp b/src/solvers/sat/satcheck_minisat.cpp
index ab6114ac2eb..c944c471668 100644
--- a/src/solvers/sat/satcheck_minisat.cpp
+++ b/src/solvers/sat/satcheck_minisat.cpp
@@ -150,7 +150,7 @@ void satcheck_minisat1_baset::lcnf(const bvt &bv)
   clause_counter++;
 }
 
-propt::resultt satcheck_minisat1_baset::prop_solve()
+propt::resultt satcheck_minisat1_baset::do_prop_solve()
 {
   PRECONDITION(status != ERROR);
 
@@ -262,11 +262,11 @@ const std::string satcheck_minisat1_prooft::solver_text()
   return "MiniSAT + Proof";
 }
 
-propt::resultt satcheck_minisat1_coret::prop_solve()
+propt::resultt satcheck_minisat1_coret::do_prop_solve()
 {
   propt::resultt r;
 
-  r=satcheck_minisat1_prooft::prop_solve();
+  r = satcheck_minisat1_prooft::do_prop_solve();
 
   if(status==UNSAT)
   {
diff --git a/src/solvers/sat/satcheck_minisat.h b/src/solvers/sat/satcheck_minisat.h
index 64954dee626..9a34d062136 100644
--- a/src/solvers/sat/satcheck_minisat.h
+++ b/src/solvers/sat/satcheck_minisat.h
@@ -24,24 +24,31 @@ class satcheck_minisat1_baset:public cnf_solvert
 
   virtual ~satcheck_minisat1_baset();
 
-  virtual const std::string solver_text() override;
-  virtual resultt prop_solve() override;
-  virtual tvt l_get(literalt a) const override;
+  const std::string solver_text() override;
+  tvt l_get(literalt a) const override;
 
-  virtual void lcnf(const bvt &bv) final;
+  void lcnf(const bvt &bv) final;
 
-  virtual void set_assignment(literalt a, bool value) override;
+  void set_assignment(literalt a, bool value) override;
 
   // extra MiniSat feature: solve with assumptions
-  virtual void set_assumptions(const bvt &_assumptions) override;
+  void set_assumptions(const bvt &_assumptions) override;
 
   // features
-  virtual bool has_set_assumptions() const override { return true; }
-  virtual bool has_is_in_conflict() const override { return true; }
+  bool has_set_assumptions() const override
+  {
+    return true;
+  }
+  bool has_is_in_conflict() const override
+  {
+    return true;
+  }
 
-  virtual bool is_in_conflict(literalt l) const override;
+  bool is_in_conflict(literalt l) const override;
 
 protected:
+  resultt do_prop_solve() override;
+
   // NOLINTNEXTLINE(readability/identifiers)
   class Solver *solver;
   void add_variables();
@@ -61,7 +68,7 @@ class satcheck_minisat1_prooft:public satcheck_minisat1t
   satcheck_minisat1_prooft();
   ~satcheck_minisat1_prooft();
 
-  virtual const std::string solver_text() override;
+  const std::string solver_text() override;
   simple_prooft &get_resolution_proof();
   // void set_partition_id(unsigned p_id);
 
@@ -77,12 +84,14 @@ class satcheck_minisat1_coret:public satcheck_minisat1_prooft
   satcheck_minisat1_coret();
   ~satcheck_minisat1_coret();
 
-  virtual const std::string solver_text() override;
-  virtual resultt prop_solve() override;
+  const std::string solver_text() override;
 
-  virtual bool has_in_core() const { return true; }
+  bool has_in_core() const
+  {
+    return true;
+  }
 
-  virtual bool is_in_core(literalt l) const
+  bool is_in_core(literalt l) const
   {
     PRECONDITION(l.var_no() < in_core.size());
     return in_core[l.var_no()];
@@ -90,5 +99,7 @@ class satcheck_minisat1_coret:public satcheck_minisat1_prooft
 
 protected:
   std::vector<bool> in_core;
+
+  resultt do_prop_solve() override;
 };
 #endif // CPROVER_SOLVERS_SAT_SATCHECK_MINISAT_H
diff --git a/src/solvers/sat/satcheck_minisat2.cpp b/src/solvers/sat/satcheck_minisat2.cpp
index 7c5b25a707a..0a916e66e72 100644
--- a/src/solvers/sat/satcheck_minisat2.cpp
+++ b/src/solvers/sat/satcheck_minisat2.cpp
@@ -162,8 +162,8 @@ static void interrupt_solver(int signum)
 
 #endif
 
-template<typename T>
-propt::resultt satcheck_minisat2_baset<T>::prop_solve()
+template <typename T>
+propt::resultt satcheck_minisat2_baset<T>::do_prop_solve()
 {
   PRECONDITION(status != statust::ERROR);
 
diff --git a/src/solvers/sat/satcheck_minisat2.h b/src/solvers/sat/satcheck_minisat2.h
index 6a53ff468d7..d8f2c1afdeb 100644
--- a/src/solvers/sat/satcheck_minisat2.h
+++ b/src/solvers/sat/satcheck_minisat2.h
@@ -30,14 +30,13 @@ class satcheck_minisat2_baset:public cnf_solvert
   satcheck_minisat2_baset(T *, message_handlert &message_handler);
   virtual ~satcheck_minisat2_baset();
 
-  virtual resultt prop_solve() override;
-  virtual tvt l_get(literalt a) const final;
+  tvt l_get(literalt a) const override final;
 
-  virtual void lcnf(const bvt &bv) final;
-  virtual void set_assignment(literalt a, bool value) override;
+  void lcnf(const bvt &bv) override final;
+  void set_assignment(literalt a, bool value) override;
 
   // extra MiniSat feature: solve with assumptions
-  virtual void set_assumptions(const bvt &_assumptions) override;
+  void set_assumptions(const bvt &_assumptions) override;
 
   // extra MiniSat feature: default branching decision
   void set_polarity(literalt a, bool value);
@@ -48,9 +47,15 @@ class satcheck_minisat2_baset:public cnf_solvert
   // extra MiniSat feature: permit previously interrupted SAT query to continue
   void clear_interrupt();
 
-  virtual bool is_in_conflict(literalt a) const override;
-  virtual bool has_set_assumptions() const final { return true; }
-  virtual bool has_is_in_conflict() const final { return true; }
+  bool is_in_conflict(literalt a) const override;
+  bool has_set_assumptions() const override final
+  {
+    return true;
+  }
+  bool has_is_in_conflict() const override final
+  {
+    return true;
+  }
 
   void set_time_limit_seconds(uint32_t lim) override
   {
@@ -58,6 +63,8 @@ class satcheck_minisat2_baset:public cnf_solvert
   }
 
 protected:
+  resultt do_prop_solve() override;
+
   T *solver;
   uint32_t time_limit_seconds;
 
@@ -70,7 +77,7 @@ class satcheck_minisat_no_simplifiert:
 {
 public:
   explicit satcheck_minisat_no_simplifiert(message_handlert &message_handler);
-  virtual const std::string solver_text();
+  const std::string solver_text() override;
 };
 
 class satcheck_minisat_simplifiert:
@@ -78,8 +85,8 @@ class satcheck_minisat_simplifiert:
 {
 public:
   explicit satcheck_minisat_simplifiert(message_handlert &message_handler);
-  virtual const std::string solver_text() final;
-  virtual void set_frozen(literalt a) final;
+  const std::string solver_text() override final;
+  void set_frozen(literalt a) override final;
   bool is_eliminated(literalt a) const;
 };
 
diff --git a/src/solvers/sat/satcheck_picosat.cpp b/src/solvers/sat/satcheck_picosat.cpp
index 126e4572510..30ac32737e1 100644
--- a/src/solvers/sat/satcheck_picosat.cpp
+++ b/src/solvers/sat/satcheck_picosat.cpp
@@ -65,7 +65,7 @@ void satcheck_picosatt::lcnf(const bvt &bv)
   clause_counter++;
 }
 
-propt::resultt satcheck_picosatt::prop_solve()
+propt::resultt satcheck_picosatt::do_prop_solve()
 {
   PRECONDITION(status != ERROR);
 
diff --git a/src/solvers/sat/satcheck_picosat.h b/src/solvers/sat/satcheck_picosat.h
index 5380c186ee9..8589cc5d819 100644
--- a/src/solvers/sat/satcheck_picosat.h
+++ b/src/solvers/sat/satcheck_picosat.h
@@ -21,19 +21,26 @@ class satcheck_picosatt:public cnf_solvert
   satcheck_picosatt();
   ~satcheck_picosatt();
 
-  virtual const std::string solver_text();
-  virtual resultt prop_solve();
-  virtual tvt l_get(literalt a) const;
-
-  virtual void lcnf(const bvt &bv);
-  virtual void set_assignment(literalt a, bool value);
-
-  virtual bool is_in_conflict(literalt a) const;
-  virtual void set_assumptions(const bvt &_assumptions);
-  virtual bool has_set_assumptions() const { return true; }
-  virtual bool has_is_in_conflict() const { return true; }
+  const std::string solver_text() override;
+  tvt l_get(literalt a) const override;
+
+  void lcnf(const bvt &bv) override;
+  void set_assignment(literalt a, bool value) override;
+
+  bool is_in_conflict(literalt a) const override;
+  void set_assumptions(const bvt &_assumptions) override;
+  bool has_set_assumptions() const override
+  {
+    return true;
+  }
+  bool has_is_in_conflict() const override
+  {
+    return true;
+  }
 
 protected:
+  resultt do_prop_solve() override;
+
   bvt assumptions;
 
 private:
diff --git a/src/solvers/sat/satcheck_zchaff.cpp b/src/solvers/sat/satcheck_zchaff.cpp
index ba56a12919a..2fbeb2082dc 100644
--- a/src/solvers/sat/satcheck_zchaff.cpp
+++ b/src/solvers/sat/satcheck_zchaff.cpp
@@ -70,7 +70,7 @@ void satcheck_zchaff_baset::copy_cnf()
       reinterpret_cast<int*>(&((*it)[0])), it->size());
 }
 
-propt::resultt satcheck_zchaff_baset::prop_solve()
+propt::resultt satcheck_zchaff_baset::do_prop_solve()
 {
   // this is *not* incremental
   PRECONDITION(status == INIT);
diff --git a/src/solvers/sat/satcheck_zchaff.h b/src/solvers/sat/satcheck_zchaff.h
index a25846fecff..e60b67604ca 100644
--- a/src/solvers/sat/satcheck_zchaff.h
+++ b/src/solvers/sat/satcheck_zchaff.h
@@ -24,10 +24,9 @@ class satcheck_zchaff_baset:public cnf_clause_listt
   explicit satcheck_zchaff_baset(CSolver *_solver);
   virtual ~satcheck_zchaff_baset();
 
-  virtual const std::string solver_text();
-  virtual resultt prop_solve();
-  virtual tvt l_get(literalt a) const;
-  virtual void set_assignment(literalt a, bool value);
+  const std::string solver_text() override;
+  tvt l_get(literalt a) const override;
+  void set_assignment(literalt a, bool value) override;
   virtual void copy_cnf();
 
   CSolver *zchaff_solver()
@@ -36,6 +35,8 @@ class satcheck_zchaff_baset:public cnf_clause_listt
   }
 
 protected:
+  resultt do_prop_solve() override;
+
   CSolver *solver;
 
   enum statust { INIT, SAT, UNSAT, ERROR };
diff --git a/src/solvers/sat/satcheck_zcore.cpp b/src/solvers/sat/satcheck_zcore.cpp
index 707af33bcee..fed3fd8f314 100644
--- a/src/solvers/sat/satcheck_zcore.cpp
+++ b/src/solvers/sat/satcheck_zcore.cpp
@@ -34,7 +34,7 @@ const std::string satcheck_zcoret::solver_text()
   return "ZCore";
 }
 
-propt::resultt satcheck_zcoret::prop_solve()
+propt::resultt satcheck_zcoret::do_prop_solve()
 {
   // We start counting at 1, thus there is one variable fewer.
   {
diff --git a/src/solvers/sat/satcheck_zcore.h b/src/solvers/sat/satcheck_zcore.h
index e643f86e67f..e54cb9f90fa 100644
--- a/src/solvers/sat/satcheck_zcore.h
+++ b/src/solvers/sat/satcheck_zcore.h
@@ -20,9 +20,8 @@ class satcheck_zcoret:public dimacs_cnft
   satcheck_zcoret();
   virtual ~satcheck_zcoret();
 
-  virtual const std::string solver_text();
-  virtual resultt prop_solve();
-  virtual tvt l_get(literalt a) const;
+  const std::string solver_text() override;
+  tvt l_get(literalt a) const override;
 
   bool is_in_core(literalt l) const
   {
@@ -30,6 +29,8 @@ class satcheck_zcoret:public dimacs_cnft
   }
 
 protected:
+  resultt do_prop_solve() override;
+
   std::set<unsigned> in_core;
 };
 
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index fb6ba0fca79..9063595d499 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -4859,3 +4859,8 @@ exprt smt2_convt::substitute_let(
 
   return expr;
 }
+
+std::size_t smt2_convt::get_number_of_solver_calls() const
+{
+  return number_of_solver_calls;
+}
diff --git a/src/solvers/smt2/smt2_conv.h b/src/solvers/smt2/smt2_conv.h
index dbebd558c30..3d7f4e84532 100644
--- a/src/solvers/smt2/smt2_conv.h
+++ b/src/solvers/smt2/smt2_conv.h
@@ -133,6 +133,8 @@ class smt2_convt:public prop_convt
   void convert_type(const typet &);
   void convert_literal(const literalt);
 
+  std::size_t get_number_of_solver_calls() const override;
+
 protected:
   const namespacet &ns;
   std::ostream &out;
@@ -142,6 +144,8 @@ class smt2_convt:public prop_convt
   bvt assumptions;
   boolbv_widtht boolbv_width;
 
+  std::size_t number_of_solver_calls = 0;
+
   void write_header();
   void write_footer(std::ostream &);
 
diff --git a/src/solvers/smt2/smt2_dec.cpp b/src/solvers/smt2/smt2_dec.cpp
index 57f4752446d..0d818e441eb 100644
--- a/src/solvers/smt2/smt2_dec.cpp
+++ b/src/solvers/smt2/smt2_dec.cpp
@@ -36,6 +36,8 @@ std::string smt2_dect::decision_procedure_text() const
 
 decision_proceduret::resultt smt2_dect::dec_solve()
 {
+  ++number_of_solver_calls;
+
   temporary_filet temp_file_problem("smt2_dec_problem_", ""),
     temp_file_stdout("smt2_dec_stdout_", ""),
     temp_file_stderr("smt2_dec_stderr_", "");
diff --git a/src/solvers/smt2/smt2_dec.h b/src/solvers/smt2/smt2_dec.h
index 6dea910eed8..9b7354600e1 100644
--- a/src/solvers/smt2/smt2_dec.h
+++ b/src/solvers/smt2/smt2_dec.h
@@ -35,11 +35,14 @@ class smt2_dect:protected smt2_stringstreamt, public smt2_convt
   {
   }
 
-  virtual resultt dec_solve();
-  virtual std::string decision_procedure_text() const;
+  resultt dec_solve() override;
+  std::string decision_procedure_text() const override;
 
   // yes, we are incremental!
-  virtual bool has_set_assumptions() const { return true; }
+  bool has_set_assumptions() const override
+  {
+    return true;
+  }
 
 protected:
   resultt read_result(std::istream &in);
diff --git a/unit/solvers/bdd/miniBDD/miniBDD.cpp b/unit/solvers/bdd/miniBDD/miniBDD.cpp
index a096e22aa76..2eafa4deb96 100644
--- a/unit/solvers/bdd/miniBDD/miniBDD.cpp
+++ b/unit/solvers/bdd/miniBDD/miniBDD.cpp
@@ -149,7 +149,7 @@ class bdd_propt : public propt
     return "BDDs";
   }
 
-  resultt prop_solve() override
+  resultt do_prop_solve() override
   {
     UNREACHABLE;
     return {};