From f614c70737a5a53188e19cfb5e9bbaa2ade1f533 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Sun, 3 Feb 2019 22:34:01 +0000
Subject: [PATCH 1/3] Use override

---
 src/solvers/sat/cnf_clause_list.h     | 18 ++++++++-----
 src/solvers/sat/dimacs_cnf.h          | 10 ++++----
 src/solvers/sat/pbs_dimacs_cnf.h      |  6 ++---
 src/solvers/sat/satcheck_booleforce.h |  8 +++---
 src/solvers/sat/satcheck_cadical.h    | 28 ++++++++++++--------
 src/solvers/sat/satcheck_glucose.h    | 28 ++++++++++++--------
 src/solvers/sat/satcheck_ipasir.h     | 28 ++++++++++++--------
 src/solvers/sat/satcheck_lingeling.h  | 30 +++++++++++++---------
 src/solvers/sat/satcheck_minisat.h    | 37 +++++++++++++++++----------
 src/solvers/sat/satcheck_minisat2.h   | 28 ++++++++++++--------
 src/solvers/sat/satcheck_picosat.h    | 28 ++++++++++++--------
 src/solvers/sat/satcheck_zchaff.h     |  8 +++---
 src/solvers/sat/satcheck_zcore.h      |  6 ++---
 src/solvers/smt2/smt2_dec.h           |  9 ++++---
 14 files changed, 163 insertions(+), 109 deletions(-)

diff --git a/src/solvers/sat/cnf_clause_list.h b/src/solvers/sat/cnf_clause_list.h
index 22d89d15aeb..8f5b296932d 100644
--- a/src/solvers/sat/cnf_clause_list.h
+++ b/src/solvers/sat/cnf_clause_list.h
@@ -29,19 +29,25 @@ 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; }
+  resultt prop_solve() override
+  {
+    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;
 
@@ -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..7b38b3e5157 100644
--- a/src/solvers/sat/dimacs_cnf.h
+++ b/src/solvers/sat/dimacs_cnf.h
@@ -45,24 +45,24 @@ 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);
+  void lcnf(const bvt &bv) override;
 
-  virtual resultt prop_solve()
+  resultt prop_solve() override
   {
     return resultt::P_ERROR;
   }
 
-  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;
   }
diff --git a/src/solvers/sat/pbs_dimacs_cnf.h b/src/solvers/sat/pbs_dimacs_cnf.h
index 1d331dc71ba..88048a60c62 100644
--- a/src/solvers/sat/pbs_dimacs_cnf.h
+++ b/src/solvers/sat/pbs_dimacs_cnf.h
@@ -48,13 +48,13 @@ class pbs_dimacs_cnft:public dimacs_cnft
 
   bool pbs_solve();
 
-  virtual resultt prop_solve();
+  resultt prop_solve() override;
 
-  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";
   }
diff --git a/src/solvers/sat/satcheck_booleforce.h b/src/solvers/sat/satcheck_booleforce.h
index e52dc1b0883..6197a1e804a 100644
--- a/src/solvers/sat/satcheck_booleforce.h
+++ b/src/solvers/sat/satcheck_booleforce.h
@@ -20,11 +20,11 @@ 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;
+  resultt prop_solve() override;
+  tvt l_get(literalt a) const override;
 
-  virtual void lcnf(const bvt &bv);
+  void lcnf(const bvt &bv) override;
 };
 
 class satcheck_booleforcet:public satcheck_booleforce_baset
diff --git a/src/solvers/sat/satcheck_cadical.h b/src/solvers/sat/satcheck_cadical.h
index 763b2e3f150..c6865a778b7 100644
--- a/src/solvers/sat/satcheck_cadical.h
+++ b/src/solvers/sat/satcheck_cadical.h
@@ -23,17 +23,23 @@ 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;
+  resultt prop_solve() 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:
   // NOLINTNEXTLINE(readability/identifiers)
diff --git a/src/solvers/sat/satcheck_glucose.h b/src/solvers/sat/satcheck_glucose.h
index 9b6c22e08bb..08a26f92d1b 100644
--- a/src/solvers/sat/satcheck_glucose.h
+++ b/src/solvers/sat/satcheck_glucose.h
@@ -30,21 +30,27 @@ 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;
+  resultt prop_solve() override;
+  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:
   T *solver;
@@ -58,7 +64,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 +72,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.h b/src/solvers/sat/satcheck_ipasir.h
index 58ffb12d08a..cd6fa31032d 100644
--- a/src/solvers/sat/satcheck_ipasir.h
+++ b/src/solvers/sat/satcheck_ipasir.h
@@ -22,23 +22,29 @@ 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;
+  const std::string solver_text() override;
 
-  virtual resultt prop_solve() override;
+  resultt prop_solve() 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;
-
-  virtual 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; }
+  void set_assignment(literalt a, bool value) override;
+
+  void set_assumptions(const bvt &_assumptions) override;
+
+  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:
   void *solver;
diff --git a/src/solvers/sat/satcheck_lingeling.h b/src/solvers/sat/satcheck_lingeling.h
index ddc9388407c..1c782e9c760 100644
--- a/src/solvers/sat/satcheck_lingeling.h
+++ b/src/solvers/sat/satcheck_lingeling.h
@@ -21,18 +21,24 @@ 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;
+  resultt prop_solve() 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:
   // NOLINTNEXTLINE(readability/identifiers)
diff --git a/src/solvers/sat/satcheck_minisat.h b/src/solvers/sat/satcheck_minisat.h
index 64954dee626..022a508c35e 100644
--- a/src/solvers/sat/satcheck_minisat.h
+++ b/src/solvers/sat/satcheck_minisat.h
@@ -24,22 +24,28 @@ 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;
+  resultt prop_solve() 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:
   // NOLINTNEXTLINE(readability/identifiers)
@@ -61,7 +67,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 +83,15 @@ 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;
+  resultt prop_solve() 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()];
diff --git a/src/solvers/sat/satcheck_minisat2.h b/src/solvers/sat/satcheck_minisat2.h
index 6a53ff468d7..f4afe3829a1 100644
--- a/src/solvers/sat/satcheck_minisat2.h
+++ b/src/solvers/sat/satcheck_minisat2.h
@@ -30,14 +30,14 @@ 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;
+  resultt prop_solve() override;
+  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 +48,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
   {
@@ -70,7 +76,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 +84,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.h b/src/solvers/sat/satcheck_picosat.h
index 5380c186ee9..7db1dd30064 100644
--- a/src/solvers/sat/satcheck_picosat.h
+++ b/src/solvers/sat/satcheck_picosat.h
@@ -21,17 +21,23 @@ 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;
+  resultt prop_solve() 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:
   bvt assumptions;
diff --git a/src/solvers/sat/satcheck_zchaff.h b/src/solvers/sat/satcheck_zchaff.h
index a25846fecff..c392cdd19d4 100644
--- a/src/solvers/sat/satcheck_zchaff.h
+++ b/src/solvers/sat/satcheck_zchaff.h
@@ -24,10 +24,10 @@ 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;
+  resultt prop_solve() override;
+  tvt l_get(literalt a) const override;
+  void set_assignment(literalt a, bool value) override;
   virtual void copy_cnf();
 
   CSolver *zchaff_solver()
diff --git a/src/solvers/sat/satcheck_zcore.h b/src/solvers/sat/satcheck_zcore.h
index e643f86e67f..60355bf7b53 100644
--- a/src/solvers/sat/satcheck_zcore.h
+++ b/src/solvers/sat/satcheck_zcore.h
@@ -20,9 +20,9 @@ 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;
+  resultt prop_solve() override;
+  tvt l_get(literalt a) const override;
 
   bool is_in_core(literalt l) const
   {
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);

From 7cb1056b45a02bba6429455f226795815f686c07 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Sun, 3 Feb 2019 22:42:28 +0000
Subject: [PATCH 2/3] Add protected do_prop_solve for overriding

This will allow us to count solver invocations
without repeating the code in each propt implementation.
---
 src/solvers/prop/prop.cpp               |  5 +++++
 src/solvers/prop/prop.h                 |  4 +++-
 src/solvers/sat/cnf_clause_list.h       | 10 +++++-----
 src/solvers/sat/dimacs_cnf.h            | 10 +++++-----
 src/solvers/sat/pbs_dimacs_cnf.cpp      |  2 +-
 src/solvers/sat/pbs_dimacs_cnf.h        |  4 ++--
 src/solvers/sat/satcheck_booleforce.cpp |  2 +-
 src/solvers/sat/satcheck_booleforce.h   |  4 +++-
 src/solvers/sat/satcheck_cadical.cpp    |  2 +-
 src/solvers/sat/satcheck_cadical.h      |  3 ++-
 src/solvers/sat/satcheck_glucose.cpp    |  4 ++--
 src/solvers/sat/satcheck_glucose.h      |  3 ++-
 src/solvers/sat/satcheck_ipasir.cpp     |  2 +-
 src/solvers/sat/satcheck_ipasir.h       |  4 ++--
 src/solvers/sat/satcheck_lingeling.cpp  |  2 +-
 src/solvers/sat/satcheck_lingeling.h    |  3 ++-
 src/solvers/sat/satcheck_minisat.cpp    |  6 +++---
 src/solvers/sat/satcheck_minisat.h      |  6 ++++--
 src/solvers/sat/satcheck_minisat2.cpp   |  4 ++--
 src/solvers/sat/satcheck_minisat2.h     |  3 ++-
 src/solvers/sat/satcheck_picosat.cpp    |  2 +-
 src/solvers/sat/satcheck_picosat.h      |  3 ++-
 src/solvers/sat/satcheck_zchaff.cpp     |  2 +-
 src/solvers/sat/satcheck_zchaff.h       |  3 ++-
 src/solvers/sat/satcheck_zcore.cpp      |  2 +-
 src/solvers/sat/satcheck_zcore.h        |  3 ++-
 unit/solvers/bdd/miniBDD/miniBDD.cpp    |  2 +-
 27 files changed, 59 insertions(+), 41 deletions(-)

diff --git a/src/solvers/prop/prop.cpp b/src/solvers/prop/prop.cpp
index 62cb972297c..d3dbdf2e420 100644
--- a/src/solvers/prop/prop.cpp
+++ b/src/solvers/prop/prop.cpp
@@ -25,3 +25,8 @@ bvt propt::new_variables(std::size_t width)
     result[i]=new_variable();
   return result;
 }
+
+propt::resultt propt::prop_solve()
+{
+  return do_prop_solve();
+}
diff --git a/src/solvers/prop/prop.h b/src/solvers/prop/prop.h
index e5078979e4e..8eefdb53569 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;
@@ -120,6 +120,8 @@ class propt
   }
 
 protected:
+  virtual resultt do_prop_solve() = 0;
+
   // to avoid a temporary for lcnf(...)
   bvt lcnf_bv;
 
diff --git a/src/solvers/sat/cnf_clause_list.h b/src/solvers/sat/cnf_clause_list.h
index 8f5b296932d..480c95a50dd 100644
--- a/src/solvers/sat/cnf_clause_list.h
+++ b/src/solvers/sat/cnf_clause_list.h
@@ -39,11 +39,6 @@ class cnf_clause_listt:public cnft
     return tvt::unknown();
   }
 
-  resultt prop_solve() override
-  {
-    return resultt::P_ERROR;
-  }
-
   size_t no_clauses() const override
   {
     return clauses.size();
@@ -82,6 +77,11 @@ class cnf_clause_listt:public cnft
   }
 
 protected:
+  resultt do_prop_solve() override
+  {
+    return resultt::P_ERROR;
+  }
+
   clausest clauses;
 };
 
diff --git a/src/solvers/sat/dimacs_cnf.h b/src/solvers/sat/dimacs_cnf.h
index 7b38b3e5157..f552229e3c2 100644
--- a/src/solvers/sat/dimacs_cnf.h
+++ b/src/solvers/sat/dimacs_cnf.h
@@ -52,11 +52,6 @@ class dimacs_cnf_dumpt:public cnft
 
   void lcnf(const bvt &bv) override;
 
-  resultt prop_solve() override
-  {
-    return resultt::P_ERROR;
-  }
-
   tvt l_get(literalt) const override
   {
     return tvt::unknown();
@@ -68,6 +63,11 @@ class dimacs_cnf_dumpt:public cnft
   }
 
 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 88048a60c62..1d6cc821109 100644
--- a/src/solvers/sat/pbs_dimacs_cnf.h
+++ b/src/solvers/sat/pbs_dimacs_cnf.h
@@ -48,8 +48,6 @@ class pbs_dimacs_cnft:public dimacs_cnft
 
   bool pbs_solve();
 
-  resultt prop_solve() override;
-
   tvt l_get(literalt a) const override;
 
   // dummy functions
@@ -60,6 +58,8 @@ class pbs_dimacs_cnft:public dimacs_cnft
   }
 
 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 6197a1e804a..99bbae4fe1e 100644
--- a/src/solvers/sat/satcheck_booleforce.h
+++ b/src/solvers/sat/satcheck_booleforce.h
@@ -21,10 +21,12 @@ class satcheck_booleforce_baset:public cnf_solvert
   virtual ~satcheck_booleforce_baset();
 
   const std::string solver_text() override;
-  resultt prop_solve() override;
   tvt l_get(literalt a) const override;
 
   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 c6865a778b7..caaf99c0417 100644
--- a/src/solvers/sat/satcheck_cadical.h
+++ b/src/solvers/sat/satcheck_cadical.h
@@ -24,7 +24,6 @@ class satcheck_cadicalt:public cnf_solvert
   virtual ~satcheck_cadicalt();
 
   const std::string solver_text() override;
-  resultt prop_solve() override;
   tvt l_get(literalt a) const override;
 
   void lcnf(const bvt &bv) override;
@@ -42,6 +41,8 @@ class satcheck_cadicalt:public cnf_solvert
   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 08a26f92d1b..157bdabf692 100644
--- a/src/solvers/sat/satcheck_glucose.h
+++ b/src/solvers/sat/satcheck_glucose.h
@@ -30,7 +30,6 @@ class satcheck_glucose_baset:public cnf_solvert
   satcheck_glucose_baset(T *, message_handlert &message_handler);
   virtual ~satcheck_glucose_baset();
 
-  resultt prop_solve() override;
   tvt l_get(literalt a) const override;
 
   void lcnf(const bvt &bv) override;
@@ -53,6 +52,8 @@ class satcheck_glucose_baset:public cnf_solvert
   }
 
 protected:
+  resultt do_prop_solve() override;
+
   T *solver;
 
   void add_variables();
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 cd6fa31032d..107620cfafc 100644
--- a/src/solvers/sat/satcheck_ipasir.h
+++ b/src/solvers/sat/satcheck_ipasir.h
@@ -24,8 +24,6 @@ class satcheck_ipasirt:public cnf_solvert
   /// This method returns the description produced by the linked SAT solver
   const std::string solver_text() override;
 
-  resultt prop_solve() override;
-
   /// This method returns the truth value for a literal of the current SAT model
   tvt l_get(literalt a) const override final;
 
@@ -47,6 +45,8 @@ class satcheck_ipasirt:public cnf_solvert
   }
 
 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 1c782e9c760..06c1bbda700 100644
--- a/src/solvers/sat/satcheck_lingeling.h
+++ b/src/solvers/sat/satcheck_lingeling.h
@@ -22,7 +22,6 @@ class satcheck_lingelingt:public cnf_solvert
   virtual ~satcheck_lingelingt();
 
   const std::string solver_text() override;
-  resultt prop_solve() override;
   tvt l_get(literalt a) const override;
 
   void lcnf(const bvt &bv) override;
@@ -41,6 +40,8 @@ class satcheck_lingelingt:public cnf_solvert
   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 022a508c35e..9a34d062136 100644
--- a/src/solvers/sat/satcheck_minisat.h
+++ b/src/solvers/sat/satcheck_minisat.h
@@ -25,7 +25,6 @@ class satcheck_minisat1_baset:public cnf_solvert
   virtual ~satcheck_minisat1_baset();
 
   const std::string solver_text() override;
-  resultt prop_solve() override;
   tvt l_get(literalt a) const override;
 
   void lcnf(const bvt &bv) final;
@@ -48,6 +47,8 @@ class satcheck_minisat1_baset:public cnf_solvert
   bool is_in_conflict(literalt l) const override;
 
 protected:
+  resultt do_prop_solve() override;
+
   // NOLINTNEXTLINE(readability/identifiers)
   class Solver *solver;
   void add_variables();
@@ -84,7 +85,6 @@ class satcheck_minisat1_coret:public satcheck_minisat1_prooft
   ~satcheck_minisat1_coret();
 
   const std::string solver_text() override;
-  resultt prop_solve() override;
 
   bool has_in_core() const
   {
@@ -99,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 f4afe3829a1..d8f2c1afdeb 100644
--- a/src/solvers/sat/satcheck_minisat2.h
+++ b/src/solvers/sat/satcheck_minisat2.h
@@ -30,7 +30,6 @@ class satcheck_minisat2_baset:public cnf_solvert
   satcheck_minisat2_baset(T *, message_handlert &message_handler);
   virtual ~satcheck_minisat2_baset();
 
-  resultt prop_solve() override;
   tvt l_get(literalt a) const override final;
 
   void lcnf(const bvt &bv) override final;
@@ -64,6 +63,8 @@ class satcheck_minisat2_baset:public cnf_solvert
   }
 
 protected:
+  resultt do_prop_solve() override;
+
   T *solver;
   uint32_t time_limit_seconds;
 
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 7db1dd30064..8589cc5d819 100644
--- a/src/solvers/sat/satcheck_picosat.h
+++ b/src/solvers/sat/satcheck_picosat.h
@@ -22,7 +22,6 @@ class satcheck_picosatt:public cnf_solvert
   ~satcheck_picosatt();
 
   const std::string solver_text() override;
-  resultt prop_solve() override;
   tvt l_get(literalt a) const override;
 
   void lcnf(const bvt &bv) override;
@@ -40,6 +39,8 @@ class satcheck_picosatt:public cnf_solvert
   }
 
 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 c392cdd19d4..e60b67604ca 100644
--- a/src/solvers/sat/satcheck_zchaff.h
+++ b/src/solvers/sat/satcheck_zchaff.h
@@ -25,7 +25,6 @@ class satcheck_zchaff_baset:public cnf_clause_listt
   virtual ~satcheck_zchaff_baset();
 
   const std::string solver_text() override;
-  resultt prop_solve() override;
   tvt l_get(literalt a) const override;
   void set_assignment(literalt a, bool value) override;
   virtual void copy_cnf();
@@ -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 60355bf7b53..e54cb9f90fa 100644
--- a/src/solvers/sat/satcheck_zcore.h
+++ b/src/solvers/sat/satcheck_zcore.h
@@ -21,7 +21,6 @@ class satcheck_zcoret:public dimacs_cnft
   virtual ~satcheck_zcoret();
 
   const std::string solver_text() override;
-  resultt prop_solve() 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/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 {};

From 36feaddd0f7b1e3588fc54daf59037515f20b822 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Sun, 3 Feb 2019 22:42:28 +0000
Subject: [PATCH 3/3] Count number of solver calls in propt and prop_convt

Useful for logging statistics
---
 src/solvers/prop/prop.cpp      | 6 ++++++
 src/solvers/prop/prop.h        | 3 +++
 src/solvers/prop/prop_conv.cpp | 5 +++++
 src/solvers/prop/prop_conv.h   | 5 +++++
 src/solvers/smt2/smt2_conv.cpp | 5 +++++
 src/solvers/smt2/smt2_conv.h   | 4 ++++
 src/solvers/smt2/smt2_dec.cpp  | 2 ++
 7 files changed, 30 insertions(+)

diff --git a/src/solvers/prop/prop.cpp b/src/solvers/prop/prop.cpp
index d3dbdf2e420..2f2a03f78e2 100644
--- a/src/solvers/prop/prop.cpp
+++ b/src/solvers/prop/prop.cpp
@@ -28,5 +28,11 @@ bvt propt::new_variables(std::size_t width)
 
 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 8eefdb53569..2a861b8e6c2 100644
--- a/src/solvers/prop/prop.h
+++ b/src/solvers/prop/prop.h
@@ -119,6 +119,8 @@ 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;
 
@@ -126,6 +128,7 @@ class propt
   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/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_", "");