summaryrefslogtreecommitdiff
path: root/src/smt/smt_engine_scope.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt/smt_engine_scope.h')
-rw-r--r--src/smt/smt_engine_scope.h3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h
index fb5810fd5..701775c9c 100644
--- a/src/smt/smt_engine_scope.h
+++ b/src/smt/smt_engine_scope.h
@@ -38,6 +38,9 @@ inline SmtEngine* currentSmtEngine() {
Assert(s_smtEngine_current != NULL);
return s_smtEngine_current;
}
+inline bool smtEngineInScope() {
+ return s_smtEngine_current != NULL;
+}
inline ProofManager* currentProofManager() {
#ifdef CVC4_PROOF
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback