summaryrefslogtreecommitdiff
path: root/src/theory/bv/bv_subtheory.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/bv/bv_subtheory.h')
-rw-r--r--src/theory/bv/bv_subtheory.h4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h
index 31c542e0b..e2b649841 100644
--- a/src/theory/bv/bv_subtheory.h
+++ b/src/theory/bv/bv_subtheory.h
@@ -26,7 +26,7 @@
namespace CVC4 {
namespace proof {
-class ResolutionBitVectorProof;
+class BitVectorProof;
}
namespace theory {
@@ -93,7 +93,7 @@ class SubtheorySolver {
return res;
}
virtual void assertFact(TNode fact) { d_assertionQueue.push_back(fact); }
- virtual void setProofLog(proof::ResolutionBitVectorProof* bvp) {}
+ virtual void setProofLog(proof::BitVectorProof* bvp) {}
AssertionQueue::const_iterator assertionsBegin() {
return d_assertionQueue.begin();
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback