From: Tim King <taking@cs.nyu.edu>
Date: Fri, 30 Nov 2012 18:16:59 +0000 (+0000)
Subject: Adding smtname level options for tlimit, rlimit, etc. Fix to the internal documentati... 
X-Git-Tag: cvc5-1.0.0~7519
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8ebb053b1c8a43df8b8df21e31ed5a94cf0a53be;p=cvc5.git

Adding smtname level options for tlimit, rlimit, etc. Fix to the internal documentation in base_options.
---

diff --git a/src/options/base_options b/src/options/base_options
index d19c3b812..b4cc473eb 100644
--- 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 a3038cd4e..fc5ccf4c4 100644
--- 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