summaryrefslogtreecommitdiff
path: root/src/prop/theory_proxy.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop/theory_proxy.h')
-rw-r--r--src/prop/theory_proxy.h3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index 3bb15aa4e..61c556f34 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -34,6 +34,7 @@
#include "smt_util/lemma_input_channel.h"
#include "smt_util/lemma_output_channel.h"
#include "theory/theory.h"
+#include "util/resource_manager.h"
#include "util/statistics_registry.h"
namespace CVC4 {
@@ -92,7 +93,7 @@ public:
void logDecision(SatLiteral lit);
- void spendResource(unsigned amount);
+ void spendResource(ResourceManager::Resource r);
bool isDecisionEngineDone();
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback