summaryrefslogtreecommitdiff
path: root/src/util/options.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/util/options.h')
-rw-r--r--src/util/options.h6
1 files changed, 5 insertions, 1 deletions
diff --git a/src/util/options.h b/src/util/options.h
index 60c8f2a1a..1eca0d499 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -126,6 +126,9 @@ struct CVC4_PUBLIC Options {
/** Whether we do typechecking at Expr creation time. */
bool earlyTypeChecking;
+ /** Whether incemental solving (push/pop) */
+ bool incrementalSolving;
+
Options() :
binary_name(),
statistics(false),
@@ -147,7 +150,8 @@ struct CVC4_PUBLIC Options {
produceModels(false),
produceAssignments(false),
typeChecking(DO_SEMANTIC_CHECKS_BY_DEFAULT),
- earlyTypeChecking(USE_EARLY_TYPE_CHECKING_BY_DEFAULT) {
+ earlyTypeChecking(USE_EARLY_TYPE_CHECKING_BY_DEFAULT),
+ incrementalSolving(false) {
}
/**
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback