Documentation fixes, some code typo fixes, file perms, other minor things.

3 files changed, 12 insertions, 11 deletions

diff --git a/src/smt/options b/src/smt/options
index e5f9c2eaf..f39662c10 100644
--- a/src/smt/options
+++ b/src/smt/options
@@ -69,7 +69,7 @@ common-option cumulativeMillisecondLimit tlimit --tlimit=MS "unsigned long"
 common-option perCallMillisecondLimit  tlimit-per --tlimit-per=MS "unsigned long"
  enable time limiting per query (give milliseconds)
 common-option cumulativeResourceLimit rlimit --rlimit=N "unsigned long"
- enable resource limiting
+ enable resource limiting (currently, roughly the number of SAT conflicts)
 common-option perCallResourceLimit rlimit-per --rlimit-per=N "unsigned long"
  enable resource limiting per query
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 987220cc7..6e09408d9 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -684,7 +684,7 @@ void SmtEngine::finalOptionsAreSet() {
     return;
   }
 
-  if (options::bitvectorEagerBitblast()) {
+  if(options::bitvectorEagerBitblast()) {
     // Eager solver should use the internal decision strategy
     options::decisionMode.set(DECISION_STRATEGY_INTERNAL);
   }
@@ -1380,20 +1380,19 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
       // otherwise expand it
 
       NodeManager* nm = d_smt.d_nodeManager;
-      // FIXME: this theory specific code should be factored out of the SmtEngine, somehow
+      // FIXME: this theory-specific code should be factored out of the
+      // SmtEngine, somehow
       switch(k) {
       case kind::BITVECTOR_SDIV:
       case kind::BITVECTOR_SREM:
-      case kind::BITVECTOR_SMOD: {
+      case kind::BITVECTOR_SMOD:
         node = bv::TheoryBVRewriter::eliminateBVSDiv(node);
         break;
-      }
 
       case kind::BITVECTOR_UDIV:
-      case kind::BITVECTOR_UREM: {
+      case kind::BITVECTOR_UREM:
         node = expandBVDivByZero(node);
         break;
-      }
 
       case kind::DIVISION: {
         // partial function: division
@@ -2961,7 +2960,7 @@ void SmtEnginePrivate::processAssertions() {
           Rewriter::rewrite(Node(builder));
       }
       // For some reason this is needed for some benchmarks, such as
-      // http://church.cims.nyu.edu/benchmarks/smtlib2/QF_AUFBV/dwp_formulas/try5_small_difret_functions_dwp_tac.re_node_set_remove_at.il.dwp.smt2
+      // http://cvc4.cs.nyu.edu/benchmarks/smtlib2/QF_AUFBV/dwp_formulas/try5_small_difret_functions_dwp_tac.re_node_set_remove_at.il.dwp.smt2
       // Figure it out later
       removeITEs();
       //      Assert(iteRewriteAssertionsEnd == d_assertionsToCheck.size());
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 3531f92e7..9655297b3 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -507,9 +507,11 @@ public:
   /**
    * Set a resource limit for SmtEngine operations.  This is like a time
    * limit, but it's deterministic so that reproducible results can be
-   * obtained.  However, please note that it may not be deterministic
-   * between different versions of CVC4, or even the same version on
-   * different platforms.
+   * obtained.  Currently, it's based on the number of conflicts.
+   * However, please note that the definition may change between different
+   * versions of CVC4 (as may the number of conflicts required, anyway),
+   * and it might even be different between instances of the same version
+   * of CVC4 on different platforms.
    *
    * A cumulative and non-cumulative (per-call) resource limit can be
    * set at the same time.  A call to setResourceLimit() with