diff options
author | Cristian Cadar <c.cadar@imperial.ac.uk> | 2016-04-14 19:35:02 +0100 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2016-04-14 19:35:02 +0100 |
commit | 9efe135e3072c115af92c3f163c9d3e12ca57fb1 (patch) | |
tree | 1f3f9cfff116edf12e36a3b9c05756db0c3a84fb /lib/Basic | |
parent | 7616398de27ac2aabfc707ba11fce33ef6032627 (diff) | |
download | klee-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/Basic')
-rw-r--r-- | lib/Basic/CmdLineOptions.cpp | 4 |
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 |