summaryrefslogtreecommitdiff
path: root/src/theory/bv/options
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/bv/options')
-rw-r--r--src/theory/bv/options17
1 files changed, 17 insertions, 0 deletions
diff --git a/src/theory/bv/options b/src/theory/bv/options
new file mode 100644
index 000000000..72db63c09
--- /dev/null
+++ b/src/theory/bv/options
@@ -0,0 +1,17 @@
+#
+# Option specification file for CVC4
+# See src/options/base_options for a description of this file format
+#
+
+module BV "theory/bv/options.h" Bitvector theory
+
+option bitvectorEagerBitblast --bitblast-eager bool
+ eagerly bitblast the bitvectors to the main SAT solver
+
+option bitvectorShareLemmas --bitblast-share-lemmas bool
+ share lemmas from the bitblasting solver with the main solver
+
+option bitvectorEagerFullcheck --bitblast-eager-fullcheck bool
+ check the bitblasting eagerly
+
+endmodule
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback