diff options
author | Guy <katz911@gmail.com> | 2016-06-20 14:20:15 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-06-20 14:20:15 -0700 |
commit | a592e0137504c5788084cb8e150f46f109f566d7 (patch) | |
tree | 0816b285c639e0121a1d0a63033ad29bf25b5e35 /src/proof/theory_proof.cpp | |
parent | 4b8972fec229012812bb7edc9e315c2e54f7c059 (diff) |
Addressed a bug that occurs when proof production is triggered via text flags in the input.
Separated some initialization into two phases:
1. Those that can be done when the proof compiliation flag is set
2. Those that can be done only when the --proof option is set.
For #2, deferred their execution until the text flags in the input have been processed
Diffstat (limited to 'src/proof/theory_proof.cpp')
-rw-r--r-- | src/proof/theory_proof.cpp | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index 7fa11cc5f..634b2b738 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -79,7 +79,6 @@ void TheoryProofEngine::registerTheory(theory::Theory* th) { if (id == theory::THEORY_BV) { BitVectorProof * bvp = new LFSCBitVectorProof((theory::bv::TheoryBV*)th, this); d_theoryProofTable[id] = bvp; - ((theory::bv::TheoryBV*)th)->setProofLog( bvp ); return; } @@ -98,6 +97,19 @@ void TheoryProofEngine::registerTheory(theory::Theory* th) { } } +void TheoryProofEngine::finishRegisterTheory(theory::Theory* th) { + if (th) { + theory::TheoryId id = th->getId(); + if (id == theory::THEORY_BV) { + Assert(d_theoryProofTable.find(id) != d_theoryProofTable.end()); + + BitVectorProof *bvp = (BitVectorProof *)d_theoryProofTable[id]; + ((theory::bv::TheoryBV*)th)->setProofLog( bvp ); + return; + } + } +} + TheoryProof* TheoryProofEngine::getTheoryProof(theory::TheoryId id) { // The UF theory handles queries for the Builtin theory. if (id == theory::THEORY_BUILTIN) { |