summaryrefslogtreecommitdiff
path: root/cmdline.ml
diff options
context:
space:
mode:
Diffstat (limited to 'cmdline.ml')
-rw-r--r--cmdline.ml5
1 files changed, 5 insertions, 0 deletions
diff --git a/cmdline.ml b/cmdline.ml
index b8f8ea8..c82b35b 100644
--- a/cmdline.ml
+++ b/cmdline.ml
@@ -2,7 +2,12 @@ open Ast
type cmdline_opt = {
widen_delay : int;
+
disjunct : (id -> bool);
+
verbose_ci : bool;
vverbose_ci : bool;
+
+ max_dp_width : int;
+ max_dp_depth : int;
}