about summary refs log tree commit diff homepage
path: root/lib
diff options
context:
space:
mode:
authorCristian Cadar <c.cadar@imperial.ac.uk>2016-04-14 19:35:02 +0100
committerCristian Cadar <c.cadar@imperial.ac.uk>2016-04-14 19:35:02 +0100
commit9efe135e3072c115af92c3f163c9d3e12ca57fb1 (patch)
tree1f3f9cfff116edf12e36a3b9c05756db0c3a84fb /lib
parent7616398de27ac2aabfc707ba11fce33ef6032627 (diff)
downloadklee-9efe135e3072c115af92c3f163c9d3e12ca57fb1.tar.gz
Disabling --solver-optimize-divides by default, as the optimization is currently buggy, and we keep hitting this bug... See https://github.com/klee/klee/issues/334 for details.
Diffstat (limited to 'lib')
-rw-r--r--lib/Basic/CmdLineOptions.cpp4
1 files changed, 2 insertions, 2 deletions
diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp
index 1724ea06..a0fbda03 100644
--- a/lib/Basic/CmdLineOptions.cpp
+++ b/lib/Basic/CmdLineOptions.cpp
@@ -61,8 +61,8 @@ UseForkedCoreSolver("use-forked-solver",
 
 llvm::cl::opt<bool>
 CoreSolverOptimizeDivides("solver-optimize-divides", 
-                 llvm::cl::desc("Optimize constant divides into add/shift/multiplies before passing to core SMT solver (default=on)"),
-                 llvm::cl::init(true));
+                 llvm::cl::desc("Optimize constant divides into add/shift/multiplies before passing to core SMT solver (default=off)"),
+                 llvm::cl::init(false));
 
 
 /* Using cl::list<> instead of cl::bits<> results in quite a bit of ugliness when it comes to checking