summaryrefslogtreecommitdiff
path: root/src/options/uf_options
diff options
context:
space:
mode:
Diffstat (limited to 'src/options/uf_options')
-rw-r--r--src/options/uf_options5
1 files changed, 5 insertions, 0 deletions
diff --git a/src/options/uf_options b/src/options/uf_options
index cbac04b18..7e1cbdb17 100644
--- a/src/options/uf_options
+++ b/src/options/uf_options
@@ -41,4 +41,9 @@ option ufssFairness --uf-ss-fair bool :default true
option ufssFairnessMonotone --uf-ss-fair-monotone bool :read-write :default false
group monotone sorts when enforcing fairness for finite model finding
+option ufHo --uf-ho bool :read-write :default false
+ enable support for higher-order reasoning
+option ufHoExt --uf-ho-ext bool :read-write :default true
+ apply extensionality on function symbols
+
endmodule
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback