summaryrefslogtreecommitdiff
path: root/src/theory/bv/options
diff options
context:
space:
mode:
authorlianah <lianahady@gmail.com>2013-03-26 22:14:24 -0400
committerlianah <lianahady@gmail.com>2013-03-26 22:14:24 -0400
commit2bed73156740d7e93e303b02319c407a1d587109 (patch)
tree99876e3263f20b0c507caac27c147a991fc759dd /src/theory/bv/options
parent33a5c0897bdbfb8367dfa90342471615908df1bc (diff)
parent70d1a0171840cd62b5c1d89b875ffb50da216793 (diff)
added model generation for bv subtheories and bv-inequality solver option
Diffstat (limited to 'src/theory/bv/options')
-rw-r--r--src/theory/bv/options2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/bv/options b/src/theory/bv/options
index 72db63c09..8e01c6572 100644
--- a/src/theory/bv/options
+++ b/src/theory/bv/options
@@ -14,4 +14,6 @@ option bitvectorShareLemmas --bitblast-share-lemmas bool
option bitvectorEagerFullcheck --bitblast-eager-fullcheck bool
check the bitblasting eagerly
+option bitvectorInequalitySolver --bv-inequality-solver bool
+ turn on the inequality solver for the bit-vector theory
endmodule
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback