Resource-limiting work.

Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>

1 files changed, 1 insertions, 6 deletions

diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index adf6dfd07..b71844590 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -62,12 +62,6 @@ public:
   /** Check the satisfiability of the added clauses */
   virtual SatValue solve(long unsigned int&) = 0;
 
-  /**
-   * Instruct the solver that it should bump its consumed resource count.
-   * Returns true if resources are exhausted.
-   */
-  virtual bool spendResource() = 0;
-
   /** Interrupt the solver */
   virtual void interrupt() = 0;
 
@@ -102,6 +96,7 @@ public:
      * Notify about a learnt clause.
      */
     virtual void notify(SatClause& clause) = 0;
+    virtual void spendResource() = 0;
     virtual void safePoint() = 0;
     
   };/* class BVSatSolverInterface::Notify */