summaryrefslogtreecommitdiff
path: root/src/options
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2016-04-14 11:38:51 -0500
committerajreynol <andrew.j.reynolds@gmail.com>2016-04-14 11:38:51 -0500
commit4ce7a09a02bdcdf456d2028b3b4365c981a031f2 (patch)
tree1dce3580517f717d263ab8969b95a351ffe497c1 /src/options
parenta08f9d1f33c110ded40ee395d328de1fac087463 (diff)
Add option --snorm-infer-eq to infer equalities based on normalization in ArithCongruenceManager at standard effort (disabled by default).
Diffstat (limited to 'src/options')
-rw-r--r--src/options/arith_options3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/options/arith_options b/src/options/arith_options
index 9f4003004..f38e377ba 100644
--- a/src/options/arith_options
+++ b/src/options/arith_options
@@ -162,4 +162,7 @@ option pbRewrites --pb-rewrites bool :default false
option pbRewriteThreshold --pb-rewrite-threshold int :default 256
threshold of number of pseudoboolean variables to have before doing rewrites
+option sNormInferEq --snorm-infer-eq bool :default false
+ infer equalities based on Shostak normalization
+
endmodule
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback