Fix several spelling errors

diff --git a/proofs/signatures/th_bv_bitblast.plf b/proofs/signatures/th_bv_bitblast.plf
index 2b2fe086888d41834a0512ae7c99ea54a49189a5..254be92a005d69e67af572c7d2f538b1f8654618 100644 (file)
--- a/proofs/signatures/th_bv_bitblast.plf
+++ b/proofs/signatures/th_bv_bitblast.plf
@@ -425,7 +425,7 @@
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 ; bit blast  x = y
-; for x,y of size n, it will return a conjuction (x.0 = y.0 ^ ( ... ^ (x.{n-1} = y.{n-1})))
+; for x,y of size n, it will return a conjunction (x.0 = y.0 ^ ( ... ^ (x.{n-1} = y.{n-1})))
 ; f is the accumulator formula that builds the equality in the right order
 (program bblast_eq_rec ((x bblt) (y bblt) (f formula)) formula
   (match x

diff --git a/src/options/arith_options b/src/options/arith_options
index 6f76758e31cbb953496719650a233b4c4b6aa978..6452aafb0f6f84083a3c83f061583005a69f4f14 100644 (file)
--- a/src/options/arith_options
+++ b/src/options/arith_options
@@ -135,7 +135,7 @@ option replayRejectCutSize --replay-reject-cut unsigned :default 25500
  maximum complexity of any coefficient while replaying cuts
 
 option lemmaRejectCutSize --replay-lemma-reject-cut unsigned :default 25500
- maximum complexity of any coefficient while outputing replaying cut lemmas
+ maximum complexity of any coefficient while outputting replaying cut lemmas
 
 option soiApproxMajorFailure --replay-soi-major-threshold double :default .01
  threshold for a major tolerance failure by the approximate solver

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 94bf15540dec5393032b2c3154e07d61afec9757..d24558a00b9a81465a499179c248b540a352d4f3 100644 (file)
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -958,7 +958,7 @@ const std::string OptionsHandler::s_bitblastingModeHelp = "\
 Bit-blasting modes currently supported by the --bitblast option:\n\
 \n\
 lazy (default)\n\
-+ Separate boolean structure and term reasoning betwen the core\n\
++ Separate boolean structure and term reasoning between the core\n\
   SAT solver and the bv SAT solver\n\
 \n\
 eager\n\

diff --git a/src/options/smt_options b/src/options/smt_options
index 8f681e57d50ac932083f0d8c53a223d99af7b0af..394e2382a778b5a382d7d570019c4cdedef09add 100644 (file)
--- a/src/options/smt_options
+++ b/src/options/smt_options
@@ -108,40 +108,40 @@ common-option cpuTime cpu-time --cpu-time bool :default false
 
 # Resource spending options for SPARK
 expert-option rewriteStep rewrite-step --rewrite-step unsigned :default 1
- ammount of resources spent for each rewrite step
+ amount of resources spent for each rewrite step
 
 expert-option theoryCheckStep theory-check-step --theory-check-step unsigned :default 1
- ammount of resources spent for each theory check call
+ amount of resources spent for each theory check call
 
 expert-option decisionStep decision-step --decision-step unsigned :default 1
- ammount of getNext decision calls in the decision engine
+ amount of getNext decision calls in the decision engine
  
 expert-option bitblastStep bitblast-step --bitblast-step unsigned :default 1
- ammount of resources spent for each bitblast step
+ amount of resources spent for each bitblast step
  
 expert-option parseStep parse-step --parse-step unsigned :default 1
- ammount of resources spent for each command/expression parsing
+ amount of resources spent for each command/expression parsing
  
 expert-option lemmaStep lemma-step --lemma-step unsigned :default 1
- ammount of resources spent when adding lemmas
+ amount of resources spent when adding lemmas
  
 expert-option restartStep restart-step --restart-step unsigned :default 1
- ammount of resources spent for each theory restart
+ amount of resources spent for each theory restart
  
 expert-option cnfStep cnf-step --cnf-step unsigned :default 1
- ammount of resources spent for each call to cnf conversion
+ amount of resources spent for each call to cnf conversion
  
 expert-option preprocessStep preprocess-step --preprocess-step unsigned :default 1
- ammount of resources spent for each preprocessing step in SmtEngine
+ amount of resources spent for each preprocessing step in SmtEngine
  
 expert-option quantifierStep quantifier-step --quantifier-step unsigned :default 1
- ammount of resources spent for quantifier instantiations
+ amount of resources spent for quantifier instantiations
  
 expert-option satConflictStep sat-conflict-step --sat-conflict-step unsigned :default 1
- ammount of resources spent for each sat conflict (main sat solver)
+ amount of resources spent for each sat conflict (main sat solver)
  
 expert-option bvSatConflictStep bv-sat-conflict-step --bv-sat-conflict-step unsigned :default 1
- ammount of resources spent for each sat conflict (bitvectors)
+ amount of resources spent for each sat conflict (bitvectors)
  
  
 expert-option rewriteApplyToConst rewrite-apply-to-const --rewrite-apply-to-const bool :default false

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 6087ab70f72c1352f6bdfb5c42911f9ee5b41ae7..4d7e9deefc8d6671046961841ee8c615318fcc37 100644 (file)
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -212,7 +212,7 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){
         // Todo improve the exception thrown
         std::stringstream ss;
         ss << "The POW(^) operator can only be used with a natural number ";
-        ss << "in the exponent.  Exception occured in:" << std::endl;
+        ss << "in the exponent.  Exception occurred in:" << std::endl;
         ss << "  " << t;
         throw LogicException(ss.str());
       }

diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index c0f955861a6cd4cffe263e35e6488388adf2ca2d..0ebebf1dd8c49b7a1ebd7e72060e73ac2bf87e18 100644 (file)
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -302,7 +302,7 @@ operator SEXPR 0: "a symbolic expression (any arity)"
 
 operator LAMBDA 2 "a lambda expression; first parameter is a BOUND_VAR_LIST, second is lambda body"
 
-parameterized CHAIN CHAIN_OP 2: "chained operator (N-ary), turned into a conjuction of binary applications of the operator on adjoining parameters; first parameter is a CHAIN_OP representing a binary operator, rest are arguments to that operator"
+parameterized CHAIN CHAIN_OP 2: "chained operator (N-ary), turned into a conjunction of binary applications of the operator on adjoining parameters; first parameter is a CHAIN_OP representing a binary operator, rest are arguments to that operator"
 constant CHAIN_OP \
     ::CVC4::Chain \
     ::CVC4::ChainHashFunction \

diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h
index eae993545db0e573e106cac759dcf87e00a44e92..6dc207b6ba0511e122e396a30b4891f4fcfffd95 100644 (file)
--- a/src/theory/strings/theory_strings_type_rules.h
+++ b/src/theory/strings/theory_strings_type_rules.h
@@ -98,7 +98,7 @@ public:
     if( check ) {
       TypeNode t = n[0].getType(check);
       if (!t.isString()) {
-        throw TypeCheckingExceptionPrivate(n, "expecting an orginal string term in string contain");
+        throw TypeCheckingExceptionPrivate(n, "expecting an original string term in string contain");
       }
       t = n[1].getType(check);
       if (!t.isString()) {

diff --git a/test/regress/regress0/arith/bug716.1.cvc b/test/regress/regress0/arith/bug716.1.cvc
index 3c0e9879a1d0eba74c5a3d67f019a3ba4f3d0978..d9330c7277267cdaf479e2d6a6c7da87286bffb1 100644 (file)
--- a/test/regress/regress0/arith/bug716.1.cvc
+++ b/test/regress/regress0/arith/bug716.1.cvc
@@ -1,4 +1,4 @@
-% EXPECT: The POW(^) operator can only be used with a natural number in the exponent.  Exception occured in:
+% EXPECT: The POW(^) operator can only be used with a natural number in the exponent.  Exception occurred in:
 % EXPECT:   2 ^ x
 % EXIT: 1
 x: INT;