summaryrefslogtreecommitdiff
path: root/src/theory/bv/bitblaster_template.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/bv/bitblaster_template.h')
-rw-r--r--src/theory/bv/bitblaster_template.h8
1 files changed, 4 insertions, 4 deletions
diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h
index 4d953b03c..d42c4a8c9 100644
--- a/src/theory/bv/bitblaster_template.h
+++ b/src/theory/bv/bitblaster_template.h
@@ -135,8 +135,8 @@ class TLazyBitblaster : public TBitblaster<Node> {
{}
bool notify(prop::SatLiteral lit);
void notify(prop::SatClause& clause);
- void spendResource(uint64_t ammount);
- void safePoint(uint64_t ammount);
+ void spendResource(unsigned ammount);
+ void safePoint(unsigned ammount);
};
TheoryBV *d_bv;
@@ -240,10 +240,10 @@ public:
MinisatEmptyNotify() {}
bool notify(prop::SatLiteral lit) { return true; }
void notify(prop::SatClause& clause) { }
- void spendResource(uint64_t ammount) {
+ void spendResource(unsigned ammount) {
NodeManager::currentResourceManager()->spendResource(ammount);
}
- void safePoint(uint64_t ammount) {}
+ void safePoint(unsigned ammount) {}
};
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback