diff options
Diffstat (limited to 'src/smt/smt_engine.h')
| -rw-r--r-- | src/smt/smt_engine.h | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 1424352ef..61f8b7540 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -859,6 +859,9 @@ class CVC4_PUBLIC SmtEngine SmtEngine(const SmtEngine&) = delete; SmtEngine& operator=(const SmtEngine&) = delete; + /** Get a pointer to the PropEngine owned by this SmtEngine. */ + prop::PropEngine* getPropEngine() { return d_propEngine.get(); } + /** * Check that a generated proof (via getProof()) checks. */ @@ -1063,7 +1066,7 @@ class CVC4_PUBLIC SmtEngine /** The theory engine */ TheoryEngine* d_theoryEngine; /** The propositional engine */ - prop::PropEngine* d_propEngine; + std::unique_ptr<prop::PropEngine> d_propEngine; /** The proof manager */ ProofManager* d_proofManager; |