summaryrefslogtreecommitdiff
path: root/src/theory/bv/bitblast/lazy_bitblaster.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/bv/bitblast/lazy_bitblaster.h')
-rw-r--r--src/theory/bv/bitblast/lazy_bitblaster.h1
1 files changed, 0 insertions, 1 deletions
diff --git a/src/theory/bv/bitblast/lazy_bitblaster.h b/src/theory/bv/bitblast/lazy_bitblaster.h
index 9af74d8db..8dbf7807d 100644
--- a/src/theory/bv/bitblast/lazy_bitblaster.h
+++ b/src/theory/bv/bitblast/lazy_bitblaster.h
@@ -77,7 +77,6 @@ class TLazyBitblaster : public TBitblaster<Node>
* constants to equivalence classes that don't already have them
*/
bool collectModelInfo(TheoryModel* m, bool fullModel);
- void setProofLog(proof::BitVectorProof* bvp);
typedef TNodeSet::const_iterator vars_iterator;
vars_iterator beginVars() { return d_variables.begin(); }
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback