Adding smtname level options for tlimit, rlimit, etc. Fix to the internal documentati...

diff --git a/src/options/base_options b/src/options/base_options
index d19c3b812eecb2f343ef0782aab2f7767cff033a..b4cc473ebb09206fe1ef5649a89d7cb1c425f18d 100644 (file)
--- a/src/options/base_options
+++ b/src/options/base_options
@@ -31,7 +31,7 @@
 #
 #     SPECIFICATIONs take this form:
 #
-#       SPECIFICATION ::= (internal-name | -) [-short-option/-alternate-short-option] [--long-option/--alternate-long-option] [smt-option-name] C++-type [ATTRIBUTEs...]
+#       SPECIFICATION ::= (internal-name | -) [smt-option-name] [-short-option/-alternate-short-option] [--long-option/--alternate-long-option] C++-type [ATTRIBUTEs...]
 #       ATTRIBUTE ::=   :include include-files..
 #                     | :default C++-expression
 #                     | :handler custom-option-handlers..

diff --git a/src/smt/options b/src/smt/options
index a3038cd4ea86c75c9cd2d070014894b4e71e1e72..fc5ccf4c4c01ee91cdb05bb9e8d8a5c643f069ff 100644 (file)
--- a/src/smt/options
+++ b/src/smt/options
@@ -60,13 +60,13 @@ option - regular-output-channel argument :handler CVC4::smt::setRegularOutputCha
 option - diagnostic-output-channel argument :handler CVC4::smt::setDiagnosticOutputChannel :handler-include "smt/options_handlers.h"
  set the diagnostic output channel of the solver
 
-common-option cumulativeMillisecondLimit --tlimit=MS "unsigned long"
+common-option cumulativeMillisecondLimit tlimit --tlimit=MS "unsigned long"
  enable time limiting (give milliseconds)
-common-option perCallMillisecondLimit --tlimit-per=MS "unsigned long"
+common-option perCallMillisecondLimit  tlimit-per --tlimit-per=MS "unsigned long"
  enable time limiting per query (give milliseconds)
-common-option cumulativeResourceLimit --rlimit=N "unsigned long"
+common-option cumulativeResourceLimit rlimit --rlimit=N "unsigned long"
  enable resource limiting
-common-option perCallResourceLimit --rlimit-per=N "unsigned long"
+common-option perCallResourceLimit rlimit-per --rlimit-per=N "unsigned long"
  enable resource limiting per query
 
 # --replay is currently broken; don't document it for 1.0