From 0d12fcbb5f1c047f951a69aa6ef4ae127f499312 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sat, 21 Jul 2018 09:19:31 -0500 Subject: Optimizations and fixes for computing whether a type is finite (#2179) --- src/options/quantifiers_options.toml | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'src/options') diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index 8e954ddc0..8c7414fa7 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -637,6 +637,15 @@ header = "options/quantifiers_options.h" read_only = true help = "mode for which types of bounds to minimize via first decision heuristics" +[[option]] + name = "fmfTypeCompletionThresh" + category = "regular" + long = "fmf-type-completion-thresh=N" + type = "int" + default = "1000" + read_only = true + help = "the maximum cardinality of an interpreted type for which exhaustive enumeration in finite model finding is attempted" + [[option]] name = "quantConflictFind" category = "regular" -- cgit v1.2.3