summaryrefslogtreecommitdiff
path: root/src/proof/bitvector_proof.h
diff options
context:
space:
mode:
authorguykatzz <katz911@gmail.com>2017-03-23 14:13:46 -0700
committerguykatzz <katz911@gmail.com>2017-03-23 14:13:46 -0700
commit16c0d86ae359fc16064e29ed7545db5896366c9b (patch)
tree71706cd01f2adde9fb94cfacab67ef284ef2c200 /src/proof/bitvector_proof.h
parent99ea8403a0f41387fef1a42abe45817fb191aa12 (diff)
support incremental unsat cores
Diffstat (limited to 'src/proof/bitvector_proof.h')
-rw-r--r--src/proof/bitvector_proof.h1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/proof/bitvector_proof.h b/src/proof/bitvector_proof.h
index 6b952e35c..fcd1d2584 100644
--- a/src/proof/bitvector_proof.h
+++ b/src/proof/bitvector_proof.h
@@ -85,6 +85,7 @@ protected:
std::map<Expr,std::string> d_constantLetMap;
bool d_useConstantLetification;
+ context::Context d_fakeContext;
public:
BitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback