Renaming solver-related command-line options in order to decouple them from STP. More specifically, command-line options max-stp-time, use-forked-stp and stp-optimize-divides renamed to max-solver-time, use-forked-solver and solver-optimize-divides, respectively.

Option of running the SMT solver in a separate process (i.e. forked) set to true by default.

Options of running SMT solver forked and with optimized divides made available to Kleaver as well.

1 files changed, 14 insertions, 3 deletions

diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp
index 6fe20b7e..ac0474fb 100644
--- a/lib/Basic/CmdLineOptions.cpp
+++ b/lib/Basic/CmdLineOptions.cpp
@@ -40,9 +40,20 @@ MinQueryTimeToLog("min-query-time-to-log",
                                  "Set this param to a negative value to log timeouts only."));
 
 llvm::cl::opt<double>
-MaxSTPTime("max-stp-time",
-           llvm::cl::desc("Maximum amount of time for a single query (default=0s (off)). Enables --use-forked-stp"),
-           llvm::cl::init(0.0));
+MaxCoreSolverTime("max-solver-time",
+           llvm::cl::desc("Maximum amount of time for a single SMT query (default=0s (off)). Enables --use-forked-solver"),
+           llvm::cl::init(0.0),
+           llvm::cl::value_desc("seconds"));
+
+llvm::cl::opt<bool>
+UseForkedCoreSolver("use-forked-solver",
+             llvm::cl::desc("Run the core SMT solver in a forked process (default=on)"),
+             llvm::cl::init(true));
+
+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));
 
 
 /* Using cl::list<> instead of cl::bits<> results in quite a bit of ugliness when it comes to checking