diff options
Diffstat (limited to 'src/theory/theory_inference_manager.cpp')
| -rw-r--r-- | src/theory/theory_inference_manager.cpp | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp index 3bc7351fe..ad988e534 100644 --- a/src/theory/theory_inference_manager.cpp +++ b/src/theory/theory_inference_manager.cpp @@ -15,6 +15,7 @@ #include "theory/theory_inference_manager.h" +#include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" #include "theory/output_channel.h" #include "theory/rewriter.h" @@ -118,6 +119,7 @@ void TheoryInferenceManager::conflict(TNode conf, InferenceId id) void TheoryInferenceManager::trustedConflict(TrustNode tconf, InferenceId id) { d_conflictIdStats << id; + smt::currentResourceManager()->spendResource(id); Trace("im") << "(conflict " << id << " " << tconf.getProven() << ")" << std::endl; d_theoryState.notifyInConflict(); @@ -250,6 +252,7 @@ bool TheoryInferenceManager::trustedLemma(const TrustNode& tlem, } } d_lemmaIdStats << id; + smt::currentResourceManager()->spendResource(id); Trace("im") << "(lemma " << id << " " << tlem.getProven() << ")" << std::endl; d_numCurrentLemmas++; d_out.trustedLemma(tlem, p); @@ -370,6 +373,7 @@ bool TheoryInferenceManager::processInternalFact(TNode atom, ProofGenerator* pg) { d_factIdStats << iid; + smt::currentResourceManager()->spendResource(iid); Trace("im") << "(fact " << iid << " " << (pol ? Node(atom) : atom.notNode()) << ")" << std::endl; // make the node corresponding to the explanation |