summaryrefslogtreecommitdiff
path: root/src/smt/smt_engine.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt/smt_engine.h')
-rw-r--r--src/smt/smt_engine.h6
1 files changed, 3 insertions, 3 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 8266bb1ed..1b5af415f 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -189,9 +189,9 @@ class CVC4_PUBLIC SmtEngine {
bool d_fullyInited;
/**
- * Whether or not we have added any assertions/declarations/definitions
- * since the last checkSat/query (and therefore we're not responsible
- * for an assignment).
+ * Whether or not we have added any assertions/declarations/definitions,
+ * or done push/pop, since the last checkSat/query, and therefore we're
+ * not responsible for models or proofs.
*/
bool d_problemExtended;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback